5. Logic
In the course of Chapter 2 and Chapter 4 we learned the “grammar” of the various logical symbols, like \(\land\), \(\forall\) and \(\to\). In those chapters, logical reasoning took place in fairly concrete mathematical situations: problems about equalities and inequalities in the natural numbers, the rational numbers, and so on.
In this chapter, we take a more abstract point of view, studying the process of logical reasoning in its own right. The central concept is the concept of logical equivalence: transformations to the logical structure of a statement which are always valid, because the “before” and “after” can be deduced from each other using only abstract logical reasoning, not anything specific to the mathematical situation at hand.
The most important logical equivalences are those covered in the final section of the chapter, Section 5.3. These are logical equivalences which move a negation symbol (\(\lnot\)) to a deeper position in a logical statement. Taken together, these transformations give us a way to delay and minimize our encounters with \(\lnot\), the most awkward logical symbol.
5.1. Logical equivalence
5.1.1. Example
If you abstract away the numbers, definitions, equations and inequalities, you are left with pure
logic problems. And the pure logic tactics like obtain
, apply
, constructor
, and so on
can still be used.
example {P Q : Prop} (h1 : P ∨ Q) (h2 : ¬ Q) : P := by
obtain hP  hQ := h1
· apply hP
· contradiction
It’s hardly worth trying to write proofs like this in words. The \(P\) and \(Q\) are
abstract propositions (Prop
), and this is just a game of manipulation.
example (P Q : Prop) : P → (P ∨ ¬ Q) := by
intro hP
left
apply hP
5.1.2. Example
We can think of propositional logic statements in the following way. Imagine that each variable, like \(P\), can be either “true” or “false”. There are fixed rules for how truth and falsehood combine under logical operations. For example, \(P \land Q\) is true if \(P\) and \(Q\) are both true, and otherwise it is false. We can record this information in a table called a truth table:
P  Q  (P ∧ Q) 

true  true  true 
false  true  false 
true  false  false 
false  false  false 
Likewise here is the rule for \(\lnot P\): it is the opposite of \(P\).
P  ¬P 

true  false 
false  true 
Using the rules for the basic operations, we can work out the truth table for a more complex statement step by step from the operations it’s composed of. For example, here’s how to find the truth table for \(\lnot(P \land \lnot Q)\): first compute the table for \(\lnot Q\), then for \(P \land \lnot Q\), then finally for \(\lnot(P \land \lnot Q)\).
P  Q  ¬Q  (P ∧ ¬Q)  ¬(P ∧ ¬Q) 

true  true  false  false  true 
false  true  false  false  true 
true  false  true  true  false 
false  false  true  false  true 
You should practise doing this by hand, but the Lean command #truth_table
will also do it
automatically.
#truth_table ¬(P ∧ ¬ Q)
That’s how I generated these pictures! The #truth_table
command was written by Joseph Rotella
with contributions from Ryan Edmonds; both are students at Brown University.
5.1.3. Exercise
Here are the rules for the remaining basic logical operations:
P  Q  (P ∨ Q) 

true  true  true 
false  true  true 
true  false  true 
false  false  false 
P  Q  (P → Q) 

true  true  true 
false  true  true 
true  false  false 
false  false  true 
P  Q  (P ↔ Q) 

true  true  true 
false  true  false 
true  false  false 
false  false  true 
Problem
Work out the truth table for \(P \leftrightarrow (\lnot P \lor Q)\).
Then check it in Lean.
5.1.4. Example
Two propositional logic formulas are said to be logically equivalent, if the “if and only if” between them can be proved in Lean. For example,
Problem
Show that \(P \lor P\) is logically equivalent to \(P\).
example (P : Prop) : (P ∨ P) ↔ P := by
constructor
· intro h
obtain h1  h2 := h
· apply h1
· apply h2
· intro h
left
apply h
An important caveat here is that there is still one logic tactic which hasn’t been introduced yet (see Section 5.2). So there are some pairs of propositional logic formulas which are logically equivalent in a way that we can’t yet demonstrate.
5.1.5. Example
Problem
Show that \(P \land (Q \lor R)\) is logically equivalent to \((P \land Q) \lor (P \land R)\).
This is a long one. I’ve done the first direction and left the second for you.
example (P Q R : Prop) : (P ∧ (Q ∨ R)) ↔ ((P ∧ Q) ∨ (P ∧ R)) := by
constructor
· intro h
obtain ⟨h1, h2  h2⟩ := h
· left
constructor
· apply h1
· apply h2
· right
constructor
· apply h1
· apply h2
· sorry
We will not prove it in this book, but two statements in propositional logic are logically equivalent if and only if they have the same truth table. For example, compare the output of these two Lean commands:
#truth_table P ∧ (Q ∨ R)
#truth_table (P ∧ Q) ∨ (P ∧ R)
5.1.6. Example
We can also perform this kind of abstract logic game when quantifiers are involved.
example {P Q : α → Prop} (h1 : ∀ x : α, P x) (h2 : ∀ x : α, Q x) :
∀ x : α, P x ∧ Q x := by
intro x
constructor
· apply h1
· apply h2
Here the \(P\) and \(Q\) are predicates, abstractions of a statement involving a variable (here called \(x\)). Statements about quantified predicates are sometimes referred to as firstorder logic.
Here’s another example of abstract logical reasoning involving quantifiers.
example {P : α → β → Prop} (h : ∃ x : α, ∀ y : β, P x y) :
∀ y : β, ∃ x : α, P x y := by
obtain ⟨x, hx⟩ := h
intro y
use x
apply hx
The concept of logical equivalence also still makes sense in this setting.
Problem
Show that \(\lnot\exists x, P(x)\) is logically equivalent to \(\forall x, \lnot P(x)\).
example (P : α → Prop) : ¬ (∃ x, P x) ↔ ∀ x, ¬ P x := by
constructor
· intro h a ha
have : ∃ x, P x
· use a
apply ha
contradiction
· intro h h'
obtain ⟨x, hx⟩ := h'
have : ¬ P x := h x
contradiction
5.1.7. Exercises
Prove the following propositional logic statement:
example {P Q : Prop} (h : P ∧ Q) : P ∨ Q := by sorry
Prove the following propositional logic statement:
example {P Q R : Prop} (h1 : P → Q) (h2 : P → R) (h3 : P) : Q ∧ R := by sorry
Prove the following propositional logic statement:
example (P : Prop) : ¬(P ∧ ¬ P) := by sorry
Prove the following propositional logic statement:
example {P Q : Prop} (h1 : P ↔ ¬ Q) (h2 : Q) : ¬ P := by sorry
Prove the following propositional logic statement:
example {P Q : Prop} (h1 : P ∨ Q) (h2 : Q → P) : P := by sorry
Prove the following propositional logic statement:
example {P Q R : Prop} (h : P ↔ Q) : (P ∧ R) ↔ (Q ∧ R) := by sorry
Prove that \(P \land P\) is logically equivalent to \(P\).
example (P : Prop) : (P ∧ P) ↔ P := by sorry
Prove that \(P \lor Q\) is logically equivalent to \(Q \lor P\).
example (P Q : Prop) : (P ∨ Q) ↔ (Q ∨ P) := by sorry
Prove that \(\lnot(P \lor Q)\) is logically equivalent to \(\lnot P \land \lnot Q\).
This theorem is in the library under the name
not_or
. It is one of “De Morgan’s laws”.example (P Q : Prop) : ¬(P ∨ Q) ↔ (¬P ∧ ¬Q) := by sorry
Prove the following firstorder logic statement:
example {P Q : α → Prop} (h1 : ∀ x, P x → Q x) (h2 : ∀ x, P x) : ∀ x, Q x := by sorry
Prove the following firstorder logic statement:
example {P Q : α → Prop} (h : ∀ x, P x ↔ Q x) : (∃ x, P x) ↔ (∃ x, Q x) := by sorry
Show that \(\exists x \ y, P(x, y)\) is logically equivalent to \(\exists y \ x, P(x, y)\).
example (P : α → β → Prop) : (∃ x y, P x y) ↔ ∃ y x, P x y := by sorry
Show that \(\forall x \ y, P(x, y)\) is logically equivalent to \(\forall y \ x, P(x, y)\).
example (P : α → β → Prop) : (∀ x y, P x y) ↔ ∀ y x, P x y := by sorry
Show that \((\exists x, P(x)) \land Q\) is logically equivalent to \(\exists x, (P(x) \land Q)\).
example (P : α → Prop) (Q : Prop) : ((∃ x, P x) ∧ Q) ↔ ∃ x, (P x ∧ Q) := by sorry
5.2. The law of the excluded middle
A tradition which goes back to the ancient Greeks is to give a slightly silly name to a class of numbers, in order to provide shorter theorem statements while studying it. In that vein, I present, just for this section … the superpowered numbers!
Definition
A natural number \(k\) is superpowered, if for every natural number \(n\), the number \(k^{k^n} + 1\) is prime.
def Superpowered (k : ℕ) : Prop := ∀ n : ℕ, Prime (k ^ k ^ n + 1)
5.2.1. Example
Is 0 superpowered? \(0^{0^0}+1=1\), \(0^{0^1}+1=2\), \(0^{0^2}+1=2\), \(0^{0^3}+1=2\). We can also do these calculations in Lean:
#eval 0 ^ 0 ^ 0 + 1  1
#eval 0 ^ 0 ^ 1 + 1  2
#eval 0 ^ 0 ^ 2 + 1  2
The first is not prime, the others are, but taking them together, the “for all” in the definition is false. Formally:
Lemma
0 is not superpowered.
Proof
Suppose 0 were superpowered. Then in particular \(0^{0^0}+1=1\) would be prime, which is a contradiction, since 1 is not prime.
To write this in Lean, we use the lemma not_prime_one
, from an exercise to
Section 4.5.
theorem not_superpowered_zero : ¬ Superpowered 0 := by
intro h
have one_prime : Prime (0 ^ 0 ^ 0 + 1) := h 0
conv at one_prime => numbers  simplifies that statement to `Prime 1`
have : ¬ Prime 1 := not_prime_one
contradiction
Don’t worry too much about the unfamiliar tactic conv
in the above proof – we will not
encounter it outside of this section. Just compare the goal state before and after the use of the
tactic and check that you agree intuitively with the transformation which occurred.
5.2.2. Example
Is 1 superpowered?
#eval 1 ^ 1 ^ 0 + 1  2
#eval 1 ^ 1 ^ 1 + 1  2
#eval 1 ^ 1 ^ 2 + 1  2
Lemma
1 is superpowered.
Proof
Let \(n\) be a natural number. Then \(1^{1^n}+1=1^1+1=2\), which is prime.
To write this in Lean, we use the lemma prime_two
, from Example 4.1.8.
theorem superpowered_one : Superpowered 1 := by
intro n
conv => ring  simplifies goal from `Prime (1 ^ 1 ^ n + 1)` to `Prime 2`
apply prime_two
5.2.3. Example
Is 2 superpowered?
#eval 2 ^ 2 ^ 0 + 1  3
#eval 2 ^ 2 ^ 1 + 1  5
#eval 2 ^ 2 ^ 2 + 1  17
#eval 2 ^ 2 ^ 3 + 1  257
#eval 2 ^ 2 ^ 4 + 1  65537
All these numbers are prime, as it happens. But checking 257 is prime using our usual lemma
better_prime_test
will be a good 30 lines of calculations in Lean, and as for 65537, I
certainly don’t have the patience. The next one will be even worse. Let’s leave the question of
2 open for now.
5.2.4. Example
Is 3 superpowered?
#eval 3 ^ 3 ^ 0 + 1  4
#eval 3 ^ 3 ^ 1 + 1  28
#eval 3 ^ 3 ^ 2 + 1  19684
Nope! It fails even at the first step.
Lemma
3 is not superpowered.
Proof
Suppose 3 were superpowered. Then in particular \(3^{3^0}+1=4\) would be prime, which is a contradiction, since \(4=2\cdot 2\).
Remember to use the lemma not_prime
in Lean to prove that a number is not prime by producing a
factor for it.
theorem not_superpowered_three : ¬ Superpowered 3 := by
intro h
dsimp [Superpowered] at h
have four_prime : Prime (3 ^ 3 ^ 0 + 1) := h 0
conv at four_prime => numbers  simplifies that statement to `Prime 4`
have four_not_prime : ¬ Prime 4
· apply not_prime 2 2
· numbers  show `2 ≠ 1`
· numbers  show `2 ≠ 4`
· numbers  show `4 = 2 * 2`
contradiction
5.2.5. Example
All this was warmup. Here is the question I really want to study.
Problem
Prove that there exists a natural number \(k\), such that \(k\) is superpowered and \(k+1\) is not.
Solution
We consider two cases, depending on whether or not 2 is superpowered.
If 2 is superpowered, then \(k=2\) has the desired property, since 2 is superpowered and 3 is not superpowered.
If not, then \(k=1\) has the desired property, since 1 is superpowered and 2 is not superpowered. 1
The point about this proof is that it works even though we don’t know whether 2 is superpowered or not. Either way, we have a way of solving the problem.
The fact that any statement (such as “2 is superpowered”) must be either true or false is an axiom of mathematics, called the law of the excluded middle. Therefore, this is always a valid case division in a proof, although it is relatively rare to need to do it.
In Lean, you can perform a case division on the truth or falsehood of a statement by using the
tactic by_cases
. In the proof that follows, using this tactic takes us from a goal state of
⊢ ∃ k, Superpowered k ∧ ¬ Superpowered (k + 1)
to a goal state with two goals, one under the assumption Superpowered 2
and one under the
assumption ¬ Superpowered 2
.
h2 : Superpowered 2
⊢ ∃ k, Superpowered k ∧ ¬ Superpowered (k + 1)
h2 : ¬ Superpowered 2
⊢ ∃ k, Superpowered k ∧ ¬ Superpowered (k + 1)
Here is the full proof in Lean.
example : ∃ k : ℕ, Superpowered k ∧ ¬ Superpowered (k + 1) := by
by_cases h2 : Superpowered 2
· use 2
constructor
· apply h2
· apply not_superpowered_three
· use 1
constructor
· apply superpowered_one
· apply h2
5.2.6. Example
As noted above, it’s relatively rare to need to use the law of the excluded middle in a proof. But here is one more example where it’s needed, this time from propositional logic: “two wrongs make a right”.
example {P : Prop} (hP : ¬¬P) : P := by
by_cases hP : P
· apply hP
· contradiction
5.2.7. Exercises
Let us call a real number \(x\) tribalanced, if for every natural number \(n\), the inequality \(\left(1+\frac{x}{n}\right)^n<3\) holds. Show that there exists a real number \(x\), such that \(x\) is tribalanced and \(x+1\) is not.
def Tribalanced (x : ℝ) : Prop := ∀ n : ℕ, (1 + x / n) ^ n < 3 example : ∃ x : ℝ, Tribalanced x ∧ ¬ Tribalanced (x + 1) := by sorry
Prove that \(\lnot P \to \lnot Q\) is logically equivalent to \(Q \to P\). You will need to use the law of the excluded middle.
This logical equivalence is known as the principle of contraposition. You might like to compare their truth tables as a sanity check.
example (P Q : Prop) : (¬P → ¬Q) ↔ (Q → P) := by sorry
In case you’re still wondering: 2 is not superpowered. The question was raised in 1650 by the mathematician Pierre de Fermat, who observed, as we did, that 3, 5, 17, 257 and 65537 are all prime. It was settled in 1732, when Leonhard Euler showed that the next number in the sequence, \(2^{2^5}+1=4294967297\), is equal to \(641 \times 6700417\) and therefore not prime.
Use Euler’s discovery to give a proof without case division to the problem in Example 5.2.5.
example : ∃ k : ℕ, Superpowered k ∧ ¬ Superpowered (k + 1) := by sorry
Footnotes
 1
Experts will notice that this proof adapts the idea from a more famous problem: show that there exists an irrational power of an irrational number which is rational.
5.3. Normal form for negations
5.3.1. Example
An important family of logical equivalences allows us to “push” negations inwards in a logical statement. For example, we proved a rule for negating \(\exists\) in Example 5.1.6 (that \(\lnot\exists x, P(x)\) is logically equivalent to \(\forall x, \lnot P(x)\)), and a rule for negating \(\lor\) in the exercises to Section 5.1 (that \(\lnot(P \lor Q)\) is logically equivalent to \(\lnot P \land \lnot Q\)).
Let’s do one more of this form, a rule for negating \(\land\). This one requires the use of the law of the excluded middle. I have done the first half and left the second half for you.
Problem
Show that \(\lnot(P \land Q)\) is logically equivalent to \(\lnot P \lor \lnot Q\).
example (P Q : Prop) : ¬ (P ∧ Q) ↔ (¬ P ∨ ¬ Q) := by
constructor
· intro h
by_cases hP : P
· right
intro hQ
have hPQ : P ∧ Q
· constructor
· apply hP
· apply hQ
contradiction
· left
apply hP
· sorry
Here is the full set of rules, together with their Lean lemma names. The remaining proofs have been left for the exercises to this section.
Operation 
Negationoutward 
Negationinward 
Lean name 
Proof 

\(\lnot\) 
\(\lnot(\lnot P)\) 
\(P\) 


\(\lor\) 
\(\lnot(P \lor Q)\) 
\(\lnot P \land \lnot Q\) 


\(\land\) 
\(\lnot(P \land Q)\) 
\(\lnot P \lor \lnot Q\) 


\(\to\) 
\(\lnot(P \to Q)\) 
\(P \land \lnot Q\) 


\(\exists\) 
\(\lnot(\exists x, P(x))\) 
\(\forall x, \lnot P(x)\) 


\(\forall\) 
\(\lnot(\forall x, P(x))\) 
\(\exists x, \lnot P(x)\) 

5.3.2. Example
By applying these rules in sequence, any mathematical statement can be brought to a form with “negations on the inside”. This is generally the most convenient form for proofs (compare the relative awkwardness of the contradiction proofs in Section 4.4 and Section 4.5 with the proofs in earlier sections).
Here is an example of this process.
Problem
Show that \(\lnot(\forall m :\mathbb{Z}, m\ne 2 \to \exists n:\mathbb{Z},n^2 = m)\) is logically equivalent to \(\exists m :\mathbb{Z}, m\ne 2\land \forall n :\mathbb{Z},n^2 ≠ m\).
We can prove this in Lean with a calculation using the rel
tactic, rewriting at each step by
one of the rules in Table 5.1.
example :
¬(∀ m : ℤ, m ≠ 2 → ∃ n : ℤ, n ^ 2 = m) ↔ ∃ m : ℤ, m ≠ 2 ∧ ∀ n : ℤ, n ^ 2 ≠ m :=
calc ¬(∀ m : ℤ, m ≠ 2 → ∃ n : ℤ, n ^ 2 = m)
↔ ∃ m : ℤ, ¬(m ≠ 2 → ∃ n : ℤ, n ^ 2 = m) := by rel [not_forall]
_ ↔ ∃ m : ℤ, m ≠ 2 ∧ ¬(∃ n : ℤ, n ^ 2 = m) := by rel [not_imp]
_ ↔ ∃ m : ℤ, m ≠ 2 ∧ ∀ n : ℤ, n ^ 2 ≠ m := by rel [not_exists]
5.3.3. Example
Try it yourself!
Problem
Show that \(\lnot(\forall n :\mathbb{Z}, \exists m : \mathbb{Z}, n^2 < m < (n+1)^2)\) is logically equivalent to \(\exists n :\mathbb{Z}, \forall m : \mathbb{Z}, n^2 \geq m \lor m \geq (n+1)^2\).
In this problem, in addition to the rules from Table 5.1, you’ll need
to use the lemma not_lt
to convert the negation of a \(<\) to a \(\geq\).
Also notice that \(n^2 < m < (n+1)^2\) is shorthand for \(n^2 < m \land m < (n+1)^2\). We have encountered this point before, in Example 1.4.4.
example : ¬(∀ n : ℤ, ∃ m : ℤ, n ^ 2 < m ∧ m < (n + 1) ^ 2)
↔ ∃ n : ℤ, ∀ m : ℤ, n ^ 2 ≥ m ∨ m ≥ (n + 1) ^ 2 :=
sorry
5.3.4. Example
This process is clearly very formulaic. You should learn to do it in your head.
And as usual, when a proof process is formulaic, there is a Lean tactic to do it for us. The tactic
is called push_neg
. Here it is, with output, on the last two examples:
#push_neg ¬(∀ m : ℤ, m ≠ 2 → ∃ n : ℤ, n ^ 2 = m)
 ∃ m : ℤ, m ≠ 2 ∧ ∀ (n : ℤ), n ^ 2 ≠ m
#push_neg ¬(∀ n : ℤ, ∃ m : ℤ, n ^ 2 < m ∧ m < (n + 1) ^ 2)
 ∃ n : ℤ, ∀ m : ℤ, m ≤ n ^ 2 ∨ (n + 1) ^ 2 ≤ m
Work out the following negations in your head, then check your work using the Lean output.
#push_neg ¬(∃ m n : ℤ, ∀ t : ℝ, m < t ∧ t < n)
#push_neg ¬(∀ a : ℕ, ∃ x y : ℕ, x * y ∣ a → x ∣ a ∧ y ∣ a)
#push_neg ¬(∀ m : ℤ, m ≠ 2 → ∃ n : ℤ, n ^ 2 = m)
There are more exercises of this style at the end of the section.
5.3.5. Example
Let’s show how the process of pushing negations inwards is useful in regular proofs. We return to the problem from Example 4.5.4.
Problem
Show that there does not exist a natural number \(n\), such that \(n^2=2\).
At the time, we observed that the solution to this problem seemed very similar to that of Example 2.3.2.
Problem
Let \(n\) be any natural number. Show that \(n ^ 2 \ne 2\).
Now we can understand why: the statements of the two problems are logically equivalent! The mathematical ideas in the two solutions are the same, but Example 2.3.2’s solution is conceptually simpler because it doesn’t involve a contradiction. We can give a more comprehensible solution to Example 4.5.4 by restating it in the form Example 2.3.2 and then writing out Example 2.3.2’s solution.
Solution
It suffices to prove that for any natural number \(n\), we have \(n ^ 2 \ne 2\).
We consider separately the cases \(n \le 1\) and \(2 \le n\).
Case 1 (\(n \le 1\)): It suffices to prove that \(n ^ 2 < 2\). Indeed,
Case 2 (\(2 \le n\)): It suffices to prove that \(n ^ 2 > 2\). Indeed,
Here’s how this looks in Lean. I left a bit for you.
example : ¬ (∃ n : ℕ, n ^ 2 = 2) := by
push_neg
intro n
have hn := le_or_succ_le n 1
obtain hn  hn := hn
· apply ne_of_lt
calc
n ^ 2 ≤ 1 ^ 2 := by rel [hn]
_ < 2 := by numbers
· sorry
5.3.6. Exercises
Show that \(\lnot(\lnot P)\) is logically equivalent to \(P\).
The point of this exercise is that you are proving the lemma
not_not
, from Table 5.1. So don’t use that lemma or the tacticpush_neg
which depends on it; instead prove this from scratch. You will need to use the law of the excluded middle.example (P : Prop) : ¬ (¬ P) ↔ P := by sorry
Prove that \(\lnot(P \to Q)\) is logically equivalent to \(P \land \lnot Q\).
The point of this exercise is that you are proving the lemma
not_imp
, from Table 5.1. So don’t use that lemma or the tacticpush_neg
which depends on it; instead prove this from scratch. You will need to use the law of the excluded middle.example (P Q : Prop) : ¬ (P → Q) ↔ (P ∧ ¬ Q) := by sorry
Show that \(\lnot\forall x, P(x)\) is logically equivalent to \(\exists x, \lnot P(x)\).
The point of this exercise is that you are proving the lemma
not_forall
, from Table 5.1. So don’t use that lemma or the tacticpush_neg
which depends on it; instead prove this from scratch. You will need to use the law of the excluded middle.example (P : α → Prop) : ¬ (∀ x, P x) ↔ ∃ x, ¬ P x := by sorry
Show step by step using the rules in Table 5.1 that \(\lnot(\forall a b :\mathbb{Z}, ab=1 \to a = 1 \lor b = 1)\) is logically equivalent to \(\exists a b :\mathbb{Z}, ab = 1\land a \ne 1 \land b \ne 1\).
example : (¬ ∀ a b : ℤ, a * b = 1 → a = 1 ∨ b = 1) ↔ ∃ a b : ℤ, a * b = 1 ∧ a ≠ 1 ∧ b ≠ 1 := sorry
Show step by step using the rules in Table 5.1 that \(\lnot(\exists x:\mathbb{R},\forall y:\mathbb{R}, y \le x)\) is logically equivalent to \(\forall x:\mathbb{R},\exists y:\mathbb{R}, y > x\).
example : (¬ ∃ x : ℝ, ∀ y : ℝ, y ≤ x) ↔ (∀ x : ℝ, ∃ y : ℝ, y > x) := sorry
Show step by step using the rules in Table 5.1 that \(\lnot(\exists m:\mathbb{Z},\forall n:\mathbb{Z},m=n+5)\) is logically equivalent to \(\forall m:\mathbb{Z},\exists n:\mathbb{Z},m\ne n+5\).
example : ¬ (∃ m : ℤ, ∀ n : ℤ, m = n + 5) ↔ ∀ m : ℤ, ∃ n : ℤ, m ≠ n + 5 := sorry
Work out the following negations in your head, then check your work using the Lean output.
#push_neg ¬(∀ n : ℕ, n > 0 → ∃ k l : ℕ, k < n ∧ l < n ∧ k ≠ l) #push_neg ¬(∀ m : ℤ, m ≠ 2 → ∃ n : ℤ, n ^ 2 = m) #push_neg ¬(∃ x : ℝ, ∀ y : ℝ, ∃ m : ℤ, x < y * m ∧ y * m < m) #push_neg ¬(∃ x : ℝ, ∀ q : ℝ, q > x → ∃ m : ℕ, q ^ m > x)
Show that it is not true that for all real numbers \(x\), we have \(x^2\geq x\).
(We solved this already in Example 4.5.1, but this time, give a proof which begins with
push_neg
.)example : ¬ (∀ x : ℝ, x ^ 2 ≥ x) := by push_neg sorry
Show that there does not exist a real number \(t\), such that \(t \le 4\) and \(t\geq 5\).
(We solved this already in the exercises to Section 4.5, but this time, give a proof which begins with
push_neg
.)example : ¬ (∃ t : ℝ, t ≤ 4 ∧ t ≥ 5) := by push_neg sorry
Show that 7 is not even.
(We solved this already in the exercises to Section 4.5, but this time, give a proof which begins with
push_neg
.)example : ¬ Int.Even 7 := by dsimp [Int.Even] push_neg sorry
Let \(p\) and \(k\) be natural numbers, with \(k\ne 1\), \(k\ne p\), and \(k\mid p\). Show that \(p\) is not prime.
(We solved this already in Example 4.5.7, but this time, give a proof which begins with
push_neg
.)example {p : ℕ} (k : ℕ) (hk1 : k ≠ 1) (hkp : k ≠ p) (hk : k ∣ p) : ¬ Prime p := by dsimp [Prime] push_neg sorry
Show that it is not true that there exists an integer \(a\), such that for all integers \(n\), \(2a^3 ≥ na+7\).
Suggested structure: Start your proof by negationnormalizing.
You might find it interesting to compare this fact with Exercise 8 in Section 2.5. How is it possible that this statement is false and that one is true?
example : ¬ ∃ a : ℤ, ∀ n : ℤ, 2 * a ^ 3 ≥ n * a + 7 := by sorry
Let \(p \geq 2\) be a natural number which is not prime. Show that there exists a natural number \(2 \le m < p\) which is a factor of \(p\).
We record this lemma for future use under the name
exists_factor_of_not_prime
.Suggested structure: Set up an intermediate goal that it is not true that any natural number \(2 \le m < p\) is not a factor of \(p\), and prove it by contradiction using the lemma
prime_test
from Example 4.4.4. Then negationnormalize that result.example {p : ℕ} (hp : ¬ Prime p) (hp2 : 2 ≤ p) : ∃ m, 2 ≤ m ∧ m < p ∧ m ∣ p := by have H : ¬ (∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p) · intro H sorry sorry