Homework (III)

Problem 1

Find logical formulae, each involving as many quantifiers as you wish, that logicizes each of the following statements. Make sure you explicitly define your predicates.

If someone is alone, they are not with someone else.
No mortal man can slay every dragon.
There is no greatest odd integer.
There is an integer that is divisible by every integer.
If an integer has a rational square root, then that root is an integer.
There is no smallest positive real number

The next three problems are from Chapter 1 of the Textbook with a slight modification: You can find the original versions as Problem 1.8., Problem 1.10. and Problem 1.18.

Problem 2

Find a statement in plain English, involving no variables at all, that is equivalent to the logical formula \[ \forall a \in \mathbb{Q} \; \forall b \in \mathbb{Q} \; (a < b \Rightarrow \exists c \in \mathbb{R} \; [a < c < b \land \neg (c \in \mathbb{Q})])\]
Prove this statement, using the structure of the logical formula as a guide.

Problem 3

Let $X$ be a set and let $P(x)$ be a predicate in one free variable $x$.

Find a logical formula representing the statement “there are exactly two elements $x : X$ such that $P(x)$ is true”.
Use the structure of this logical formula to describe how a proof of this statement should be structured, and use this structure to prove that there are exactly two real numbers $x$ such that $x^2=1$.

Problem 4

Let $X$ be $\mathbb{Z}$ or $\mathbb{Q}$, and define a logical formula $\varphi$ by: \[ \forall x \in X \; \exists y \in X \; (x < y \land \forall z \in X \; \neg (x < z \wedge z < y )) \] Write out $\neg \varphi$ as a maximally negated logical formula. Prove that $p$ is true when $X = \mathbb{Z}$, and $\varphi$ is false when $X = \mathbb{Q}$.

Problem 5

Find statements in plain English, involving as few variables as possible, that are represented by each of the following logical formulae.

$\forall d\in\mathbb{N},[(\exists q\in\mathbb{Z}, n=qd) \Rightarrow (d=1 \vee d=n)]$.
$\forall a\in\mathbb{R}, [a>0\Rightarrow (\exists b\in\mathbb{R},(b>0\wedge a<b))]$.
$\exists a\in \mathbb{Z}, [(\exists q\in \mathbb{Z}, 2q=a) \wedge (\exists q\in \mathbb{Z}, 2q+1=a)]$.

Problem 6 (Frobenius)

Suppose $A$ is a predicate depending on a variable $x$ and $B$ a predicate depending on variables $x,y$. Give a proof of \[ (A(x) \land \exists y\; B(x,y)) \To \exists y \; ( A(x) \land B(x,y) ) \] in Lean.

This means that whenever we can infer $\exists y \; ( A(x) \land B(x,y) )$ from $(A(x) \land \exists y\; B(x,y))$. This inference is not possible in logics without implication (such as geometric logic), and as such, there, it is usually added as an extra axiom called the Frobenius axiom.

Problem 7 (Drinker’s paradox).

In this problem you will prove the following seemingly bizarre statement in Lean:

(DP) In an arbitrary pub with at least one person in it, there is someone in the pub such that if that person is drinking then so is everyone else.

Let $P$ be the set of people in the pub, and let $D(x)$ be the predicate “person $x$ is drinking”. Transform the statement DP into a sentence in Lean, in terms of predicate $D(x)$, using quantifiers and implication.
By making use of the law of Excluded Middle give a proof of the statement of the Drinker’s paradox.

Tips & Hints

For problem 6, we want to a constructive proof, so the use of excluded middle and other equivalent or derived classical principles are discouraged. But please submit your classical proof if that is all you have (Incidentally, I’m not sure if finding a classical proof is an easy thing to do in this case).
There are several proofs in the Lean Lab which should help you toward constructing a proof of A x ∧ (∃ y : X, B x y) → ∃ y : X, A x ∧ B x y. For instance, one place you might like to consult is the proof of ∀x (A x ⇒ B x) ⇒ ∃x A x ⇒ ∃x B x. This sentence says if for all elements x, I can infer Bx from Ax, then if Ax is true for some x, then Bx must be true for some x too. This is a good example since you see how the rules ∀-elim (application in lean), ∃-intro (exists.intro), ∃-elim (exists.elim) work together to construct a proof a complicated sentence. This starts at the line 444 of the Lean Lab:
```
  example : (∀ x, A x → B x) → (∃ x, A x) → ∃ x, B x := 
  -- bracketing around ∃ x, A x is necessary.
  begin 
  intro h₁, 
  intro h₂, 
  show ∃ x, B x, from exists.elim h₂ (assume t, assume h₃, exists.intro t (h₁ t h₃) ),
  end   
```
Also, a detailed step-by-step proof of this example with extensive commentary is on the summary slides. You should go through the natural deduction proof on the slides step by step and also go through the lean proof line by line and see how they correspond to each other. Also, This example should be a good template to use to solve the challenges 1-6 that comes after this example in the slides.
For problem 6, make sure you introduce a domain of discourse, variable x of that domain, a unary predicates A and a binary predicate B on the domain. You can do you your proof in a section environment which has all these variables introduced, or you can introduce your variables as explicit arguments in a theorem/example environment.

Problem 7 is a result using classical logic. For the use of classical reasoning in predicate logic, the following lean proof (line 367 of the 🧪) is useful:

  section E_O 
  open classical
  variables E O : ℕ → Prop 
  example : (∀ n : ℕ, ¬ E n → O n) → ∀ n, E n ∨ O n  :=
  begin
  intro h,
  intro n, 
  cases em(E n) with u₁ u₂, 
  {show E n ∨ O n, from or.inl u₁},
  { have u₃ , from h n u₂, 
  show E n ∨ O n, from or.inr u₃},
  end   
  end E_O