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
truefalse
falsetrue

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)\).

PQ¬Q(P ∧ ¬Q)¬(P ∧ ¬Q)
truetruefalsefalsetrue
falsetruefalsefalsetrue
truefalsetruetruefalse
falsefalsetruefalsetrue

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:

PQ(P ∨ Q)
truetruetrue
falsetruetrue
truefalsetrue
falsefalsefalse

PQ(P → Q)
truetruetrue
falsetruetrue
truefalsefalse
falsefalsetrue

PQ(P ↔ Q)
truetruetrue
falsetruefalse
truefalsefalse
falsefalsetrue

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 first-order 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

  1. Prove the following propositional logic statement:

    example {P Q : Prop} (h : P  Q) : P  Q := by
      sorry
    
  2. Prove the following propositional logic statement:

    example {P Q R : Prop} (h1 : P  Q) (h2 : P  R) (h3 : P) : Q  R := by
      sorry
    
  3. Prove the following propositional logic statement:

    example (P : Prop) : ¬(P  ¬ P) := by
      sorry
    
  4. Prove the following propositional logic statement:

    example {P Q : Prop} (h1 : P  ¬ Q) (h2 : Q) : ¬ P := by
      sorry
    
  5. Prove the following propositional logic statement:

    example {P Q : Prop} (h1 : P  Q) (h2 : Q  P) : P := by
      sorry
    
  6. Prove the following propositional logic statement:

    example {P Q R : Prop} (h : P  Q) : (P  R)  (Q  R) := by
      sorry
    
  7. Prove that \(P \land P\) is logically equivalent to \(P\).

    example (P : Prop) : (P  P)  P := by
      sorry
    
  8. Prove that \(P \lor Q\) is logically equivalent to \(Q \lor P\).

    example (P Q : Prop) : (P  Q)  (Q  P) := by
      sorry
    
  9. 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
    
  10. Prove the following first-order logic statement:

    example {P Q : α  Prop} (h1 :  x, P x  Q x) (h2 :  x, P x) :  x, Q x := by
      sorry
    
  11. Prove the following first-order logic statement:

    example {P Q : α  Prop} (h :  x, P x  Q x) : ( x, P x)  ( x, Q x) := by
      sorry
    
  12. 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
    
  13. 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
    
  14. 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

  1. 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
    
  2. 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
    
  3. 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.

Table 5.1 Logical equivalences for negations

Operation

Negation-outward

Negation-inward

Lean name

Proof

\(\lnot\)

\(\lnot(\lnot P)\)

\(P\)

not_not

Exercises 5.3.6

\(\lor\)

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

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

not_or

Exercises 5.1.7

\(\land\)

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

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

not_and_or

Example 5.3.1

\(\to\)

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

\(P \land \lnot Q\)

not_imp

Exercises 5.3.6

\(\exists\)

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

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

not_exists

Example 5.1.6

\(\forall\)

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

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

not_forall

Exercises 5.3.6

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 re-stating 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,

\[\begin{split}n ^ 2 & \le 1 ^ 2\\ &<2.\end{split}\]

Case 2 (\(2 \le n\)): It suffices to prove that \(n ^ 2 > 2\). Indeed,

\[\begin{split}2 &< 2 ^ 2\\ & \le n ^ 2.\end{split}\]

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

  1. 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 tactic push_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
    
  2. 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 tactic push_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
    
  3. 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 tactic push_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
    
  4. 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
    
  5. 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
    
  6. 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
    
  7. 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)
    
  8. 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
    
  9. 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
    
  10. 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
    
  11. 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
    
  12. 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 negation-normalizing.

    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
    
  13. 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 negation-normalize 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