5. 逻辑

在第 2 章和第 4 章中，我们学习了各种逻辑符号的“语法”，例如 \(\land\)、\(\forall\) 和 \(\to\)。在那些章节中，逻辑推理发生在相当具体的数学情境里：关于自然数、有理数等对象中的等式和不等式的问题。

在本章中，我们采取更抽象的观点，研究逻辑推理过程本身。核心概念是逻辑等价：对一个陈述的逻辑结构所作的、永远有效的变换；之所以有效，是因为变换前后可以只用抽象逻辑推理相互推出，而不依赖当前数学情境的任何特殊内容。

最重要的逻辑等价出现在本章最后一节，即第 5.3 节。这些逻辑等价把否定符号（\(\lnot\)）移到逻辑陈述中更深的位置。合在一起，这些变换给出一种方法，使我们能够推迟并减少与 \(\lnot\) 这个最别扭的逻辑符号打交道。

5.1. 逻辑等价

5.1.1. 例

如果把数、定义、方程和不等式都抽象掉，剩下的就是纯逻辑问题。而 obtain、apply、constructor 等纯逻辑策略仍然可以使用。

example {P Q : Prop} (h1 : P ∨ Q) (h2 : ¬ Q) : P := by
  obtain hP | hQ := h1
  · apply hP
  · contradiction

几乎没有必要尝试用文字写出这样的证明。这里的 \(P\) 和 \(Q\) 是抽象命题（Prop），而这只是一场符号操作游戏。

example (P Q : Prop) : P → (P ∨ ¬ Q) := by
  intro hP
  left
  apply hP

5.1.2. 例

我们可以这样理解命题逻辑陈述。设想每个变量，例如 \(P\)，都可以取“真”或“假”。在逻辑运算下，真与假如何组合有固定规则。例如，\(P \land Q\) 当且仅当 \(P\) 与 \(Q\) 都为真时为真，否则为假。我们可以把这些信息记录在一个称为真值表的表格中：

P	Q	(P ∧ Q)
真	真	真
假	真	假
真	假	假
假	假	假

类似地，\(\lnot P\) 的规则如下：它与 \(P\) 相反。

P	¬P
真	假
假	真

利用基本运算的规则，我们可以从一个较复杂陈述所由构成的运算出发，逐步求出它的真值表。例如，要求 \(\lnot(P \land \lnot Q)\) 的真值表，先计算 \(\lnot Q\) 的表，再计算 \(P \land \lnot Q\) 的表，最后计算 \(\lnot(P \land \lnot Q)\) 的表。

P	Q	¬Q	(P ∧ ¬Q)	¬(P ∧ ¬Q)
真	真	假	假	真
假	真	假	假	真
真	假	真	真	假
假	假	真	假	真

你应该练习手算真值表，但 Lean 命令 #truth_table 也会自动完成它。

#truth_table ¬(P ∧ ¬ Q)

这些图片就是我这样生成的！#truth_table 命令由 Joseph Rotella 编写，并有 Ryan Edmonds 参与贡献；两人都是 Brown University 的学生。

5.1.3. 练习

其余基本逻辑运算的规则如下：

P	Q	(P ∨ Q)
真	真	真
假	真	真
真	假	真
假	假	假

P	Q	(P → Q)
真	真	真
假	真	真
真	假	假
假	假	真

P	Q	(P ↔ Q)
真	真	真
假	真	假
真	假	假
假	假	真

问题

求出 \(P \leftrightarrow (\lnot P \lor Q)\) 的真值表。

然后在 Lean 中检查它。

5.1.4. 例

若两个命题逻辑公式之间的“当且仅当”可以在 Lean 中证明，则称它们逻辑等价。例如：

问题

证明 \(P \lor P\) 与 \(P\) 逻辑等价。

example (P : Prop) : (P ∨ P) ↔ P := by
  constructor
  · intro h
    obtain h1 | h2 := h
    · apply h1
    · apply h2
  · intro h
    left
    apply h

这里有一个重要提醒：还有一个逻辑策略尚未介绍（见第 5.2 节）。因此，有些命题逻辑公式对虽然逻辑等价，但我们还不能演示这种等价。

5.1.5. 例

问题

证明 \(P \land (Q \lor R)\) 与 \((P \land Q) \lor (P \land R)\) 逻辑等价。

这个证明比较长。我已经完成了一个方向，把另一个方向留给你。

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

本书中不会证明这一点，但命题逻辑中的两个陈述逻辑等价，当且仅当它们有相同的真值表。例如，比较下面两个 Lean 命令的输出：

#truth_table P ∧ (Q ∨ R)
#truth_table (P ∧ Q) ∨ (P ∧ R)

5.1.6. 例

当涉及量词时，我们也可以进行这种抽象逻辑游戏。

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

这里的 \(P\) 和 \(Q\) 是谓词，即涉及某个变量（这里称为 \(x\)）的陈述的抽象。关于量化谓词的陈述有时称为一阶逻辑。

下面是另一个涉及量词的抽象逻辑推理例子。

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

逻辑等价的概念在这个语境中也仍然有意义。

问题

证明 \(\lnot\exists x, P(x)\) 与 \(\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. 练习

1. 证明下面的命题逻辑陈述：

   example {P Q : Prop} (h : P ∧ Q) : P ∨ Q := by
     sorry
   

2. 证明下面的命题逻辑陈述：

   example {P Q R : Prop} (h1 : P → Q) (h2 : P → R) (h3 : P) : Q ∧ R := by
     sorry
   

3. 证明下面的命题逻辑陈述：

   example (P : Prop) : ¬(P ∧ ¬ P) := by
     sorry
   

4. 证明下面的命题逻辑陈述：

   example {P Q : Prop} (h1 : P ↔ ¬ Q) (h2 : Q) : ¬ P := by
     sorry
   

5. 证明下面的命题逻辑陈述：

   example {P Q : Prop} (h1 : P ∨ Q) (h2 : Q → P) : P := by
     sorry
   

6. 证明下面的命题逻辑陈述：

   example {P Q R : Prop} (h : P ↔ Q) : (P ∧ R) ↔ (Q ∧ R) := by
     sorry
   

7. 证明 \(P \land P\) 与 \(P\) 逻辑等价。

   example (P : Prop) : (P ∧ P) ↔ P := by
     sorry
   

8. 证明 \(P \lor Q\) 与 \(Q \lor P\) 逻辑等价。

   example (P Q : Prop) : (P ∨ Q) ↔ (Q ∨ P) := by
     sorry
   

9. 证明 \(\lnot(P \lor Q)\) 与 \(\lnot P \land \lnot Q\) 逻辑等价。这个定理在库中名为 not_or。它是“德摩根律”之一。

   example (P Q : Prop) : ¬(P ∨ Q) ↔ (¬P ∧ ¬Q) := by
     sorry
   

10. 证明下面的一阶逻辑陈述：

    example {P Q : α → Prop} (h1 : ∀ x, P x → Q x) (h2 : ∀ x, P x) : ∀ x, Q x := by
      sorry
    

11. 证明下面的一阶逻辑陈述：

    example {P Q : α → Prop} (h : ∀ x, P x ↔ Q x) : (∃ x, P x) ↔ (∃ x, Q x) := by
      sorry
    

12. 证明 \(\exists x \ y, P(x, y)\) 与 \(\exists y \ x, P(x, y)\) 逻辑等价。

    example (P : α → β → Prop) : (∃ x y, P x y) ↔ ∃ y x, P x y := by
      sorry
    

13. 证明 \(\forall x \ y, P(x, y)\) 与 \(\forall y \ x, P(x, y)\) 逻辑等价。

    example (P : α → β → Prop) : (∀ x y, P x y) ↔ ∀ y x, P x y := by
      sorry
    

14. 证明 \((\exists x, P(x)) \land Q\) 与 \(\exists x, (P(x) \land Q)\) 逻辑等价。

    example (P : α → Prop) (Q : Prop) : ((∃ x, P x) ∧ Q) ↔ ∃ x, (P x ∧ Q) := by
      sorry
    

5.2. 排中律

一种可追溯到古希腊的传统，是给某一类数起一个稍显俏皮的名称，以便在研究它们时能写出更短的定理陈述。本着这种精神，我只在本节中介绍……超能数！

定义

自然数 \(k\) 称为超能的，如果对每个自然数 \(n\)，数 \(k^{k^n} + 1\) 都是素数。

def Superpowered (k : ℕ) : Prop := ∀ n : ℕ, Prime (k ^ k ^ n + 1)

5.2.1. 例

0 是超能的吗？\(0^{0^0}+1=1\)，\(0^{0^1}+1=2\)，\(0^{0^2}+1=2\)，\(0^{0^3}+1=2\)。我们也可以在 Lean 中做这些计算：

#eval 0 ^ 0 ^ 0 + 1 -- 1
#eval 0 ^ 0 ^ 1 + 1 -- 2
#eval 0 ^ 0 ^ 2 + 1 -- 2

第一个数不是素数，其余的是素数；但合在一起看，定义中的“对所有”是假的。形式化地说：

引理

0 不是超能的。

证明

假设 0 是超能的。那么特别地，\(0^{0^0}+1=1\) 应该是素数；但这与 1 不是素数矛盾。

为了在 Lean 中书写这个证明，我们使用来自第 4.5 节练习的引理 not_prime_one。

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

不要太担心上面证明中不熟悉的策略 conv；在本节之外我们不会遇到它。只需比较使用该策略前后的目标状态，并检查你是否直观同意所发生的变换。

5.2.2. 例

1 是超能的吗？

#eval 1 ^ 1 ^ 0 + 1 -- 2
#eval 1 ^ 1 ^ 1 + 1 -- 2
#eval 1 ^ 1 ^ 2 + 1 -- 2

引理

1 是超能的。

证明

设 \(n\) 为自然数。则 \(1^{1^n}+1=1^1+1=2\)，而 2 是素数。

为了在 Lean 中书写这个证明，我们使用例 4.1.8 中的引理 prime_two。

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. 例

2 是超能的吗？

#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

这些数碰巧都是素数。但用我们通常的引理 better_prime_test 检查 257 是素数，在 Lean 中要写差不多 30 行计算；至于 65537，我肯定没有这个耐心。下一个数会更糟。我们暂且搁置 2 是否超能的问题。

5.2.4. 例

3 是超能的吗？

#eval 3 ^ 3 ^ 0 + 1 -- 4
#eval 3 ^ 3 ^ 1 + 1 -- 28
#eval 3 ^ 3 ^ 2 + 1 -- 19684

不是！它第一步就失败了。

引理

3 不是超能的。

证明

假设 3 是超能的。那么特别地，\(3^{3^0}+1=4\) 应该是素数；但这与 \(4=2\cdot 2\) 矛盾。

记得在 Lean 中使用引理 not_prime，通过给出一个因子来证明某个数不是素数。

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. 例

前面这些都是热身。下面才是我真正想研究的问题。

问题

证明：存在自然数 \(k\)，使得 \(k\) 是超能的，而 \(k+1\) 不是超能的。

解答

我们按照 2 是否超能分两种情形讨论。

如果 2 是超能的，那么 \(k=2\) 具有所需性质，因为 2 是超能的，而 3 不是超能的。

如果不是，那么 \(k=1\) 具有所需性质，因为 1 是超能的，而 2 不是超能的。1

这个证明的要点是：即使我们不知道 2 是否超能，它仍然有效。无论是哪种情形，我们都有办法解决问题。

任意陈述（例如“2 是超能的”）必须为真或为假，这是数学的一条公理，称为排中律。因此，这在证明中总是一种有效的分类讨论，尽管真正需要这样做的情况相对少见。

在 Lean 中，可以使用策略 by_cases 按一个陈述的真假进行分类讨论。在下面的证明中，使用该策略会把我们从如下目标状态

⊢ ∃ k, Superpowered k ∧ ¬ Superpowered (k + 1)

变为含有两个目标的目标状态：一个在假设 Superpowered 2 下，另一个在假设 ¬ Superpowered 2 下。

h2 : Superpowered 2
⊢ ∃ k, Superpowered k ∧ ¬ Superpowered (k + 1)

h2 : ¬ Superpowered 2
⊢ ∃ k, Superpowered k ∧ ¬ Superpowered (k + 1)

下面是完整的 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 {P : Prop} (hP : ¬¬P) : P := by
  by_cases hP : P
  · apply hP
  · contradiction

5.2.7. 练习

1. 若对每个自然数 \(n\)，不等式 \(\left(1+\frac{x}{n}\right)^n<3\) 都成立，则称实数 \(x\) 为三平衡的。证明：存在实数 \(x\)，使得 \(x\) 是三平衡的，而 \(x+1\) 不是三平衡的。

   def Tribalanced (x : ℝ) : Prop := ∀ n : ℕ, (1 + x / n) ^ n < 3
   
   example : ∃ x : ℝ, Tribalanced x ∧ ¬ Tribalanced (x + 1) := by
     sorry
   

2. 证明 \(\lnot P \to \lnot Q\) 与 \(Q \to P\) 逻辑等价。你需要使用排中律。这个逻辑等价称为逆否命题原理。作为可靠性检查，你也可以比较它们的真值表。

   example (P Q : Prop) : (¬P → ¬Q) ↔ (Q → P) := by
     sorry
   

3. 如果你还在好奇：2 不是超能的。这个问题由数学家 Pierre de Fermat 于 1650 年提出；他像我们一样观察到 3、5、17、257 和 65537 都是素数。1732 年，Leonhard Euler 证明序列中的下一个数 \(2^{2^5}+1=4294967297\) 等于 \(641 \times 6700417\)，因而不是素数，问题由此解决。请使用 Euler 的发现，给出一个不分类讨论的证明来解决例 5.2.5 中的问题。

   example : ∃ k : ℕ, Superpowered k ∧ ¬ Superpowered (k + 1) := by
     sorry
   

脚注

1

有经验的读者会注意到，这个证明改编自一个更著名的问题：证明存在某个无理数的无理数次幂是有理数。

5.3. 否定的范式

5.3.1. 例

有一类重要的逻辑等价允许我们把否定在逻辑陈述中向内“推进”。例如，我们在例 5.1.6 中证明了否定 \(\exists\) 的规则（\(\lnot\exists x, P(x)\) 与 \(\forall x, \lnot P(x)\) 逻辑等价），又在第 5.1 节练习中证明了否定 \(\lor\) 的规则（\(\lnot(P \lor Q)\) 与 \(\lnot P \land \lnot Q\) 逻辑等价）。

我们再做一个同类规则，即否定 \(\land\) 的规则。这个规则需要使用排中律。我已经完成了前半部分，把后半部分留给你。

问题

证明 \(\lnot(P \land Q)\) 与 \(\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

下面给出完整的一组规则，以及它们在 Lean 中的引理名称。余下证明留作本节练习。

表 5.1 否定的逻辑等价

运算	否定外层形式	否定内层形式	Lean 名称	证明
\(\lnot\)	\(\lnot(\lnot P)\)	\(P\)	not_not	练习 5.3.6
\(\lor\)	\(\lnot(P \lor Q)\)	\(\lnot P \land \lnot Q\)	not_or	练习 5.1.7
\(\land\)	\(\lnot(P \land Q)\)	\(\lnot P \lor \lnot Q\)	not_and_or	例 5.3.1
\(\to\)	\(\lnot(P \to Q)\)	\(P \land \lnot Q\)	not_imp	练习 5.3.6
\(\exists\)	\(\lnot(\exists x, P(x))\)	\(\forall x, \lnot P(x)\)	not_exists	例 5.1.6
\(\forall\)	\(\lnot(\forall x, P(x))\)	\(\exists x, \lnot P(x)\)	not_forall	练习 5.3.6

5.3.2. 例

依次应用这些规则后，任何数学陈述都可以化为“否定在内侧”的形式。这通常是证明中最方便的形式（可比较第 4.4 节和第 4.5 节中反证法证明的相对笨拙，与更早章节中证明的差别）。

下面是这个过程的一个例子。

问题

证明 \(\lnot(\forall m :\mathbb{Z}, m\ne 2 \to \exists n:\mathbb{Z},n^2 = m)\) 与 \(\exists m :\mathbb{Z}, m\ne 2\land \forall n :\mathbb{Z},n^2 ≠ m\) 逻辑等价。

在 Lean 中，我们可以用一个计算式证明完成它：使用 rel 策略，并在每一步用表 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. 例

请你自己试一试！

问题

证明 \(\lnot(\forall n :\mathbb{Z}, \exists m : \mathbb{Z}, n^2 < m < (n+1)^2)\) 与 \(\exists n :\mathbb{Z}, \forall m : \mathbb{Z}, n^2 \geq m \lor m \geq (n+1)^2\) 逻辑等价。

在本题中，除了表 5.1 中的规则外，你还需要使用引理 not_lt，把一个 \(<\) 的否定转化为 \(\geq\)。

还要注意，\(n^2 < m < (n+1)^2\) 是 \(n^2 < m \land m < (n+1)^2\) 的简写。我们以前在例 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. 例

这个过程显然非常程式化。你应该学会在脑中完成它。照常，只要一个证明过程是程式化的，Lean 中就会有策略替我们完成。这个策略名为 push_neg。下面是在前两个例子上使用它并显示输出的样子：

#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

在脑中求出下面各否定的形式，然后用 Lean 输出检查你的结果。

#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)

本节末尾还有更多这种类型的练习。

5.3.5. 例

我们来说明向内推进否定的过程在普通证明中如何有用。回到例 4.5.4 的问题。

问题

证明：不存在自然数 \(n\)，使得 \(n^2=2\)。

当时，我们观察到这个问题的解答似乎与例 2.3.2 的解答非常相似。

问题

设 \(n\) 为任意自然数。证明 \(n ^ 2 \ne 2\)。

现在我们可以理解原因：两个问题的陈述是逻辑等价的！两个解答中的数学思想相同，但例 2.3.2 的解答在概念上更简单，因为它不涉及矛盾。我们可以把例 4.5.4 重新表述为例 2.3.2 的形式，然后写出例 2.3.2 的解答，从而给出更易理解的解答。

解答

只需证明：对任意自然数 \(n\)，都有 \(n ^ 2 \ne 2\)。

我们分别讨论 \(n \le 1\) 和 \(2 \le n\) 两种情形。

情形 1（\(n \le 1\)）：只需证明 \(n ^ 2 < 2\)。确实，

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

情形 2（\(2 \le n\)）：只需证明 \(n ^ 2 > 2\)。确实，

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

下面是在 Lean 中的样子。我留了一点给你完成。

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. 练习

1. 证明 \(\lnot(\lnot P)\) 与 \(P\) 逻辑等价。本练习的要点是你正在证明表 5.1 中的引理 not_not。所以不要使用该引理，也不要使用依赖它的策略 push_neg；请从零开始证明它。你需要使用排中律。

   example (P : Prop) : ¬ (¬ P) ↔ P := by
     sorry
   

2. 证明 \(\lnot(P \to Q)\) 与 \(P \land \lnot Q\) 逻辑等价。本练习的要点是你正在证明表 5.1 中的引理 not_imp。所以不要使用该引理，也不要使用依赖它的策略 push_neg；请从零开始证明它。你需要使用排中律。

   example (P Q : Prop) : ¬ (P → Q) ↔ (P ∧ ¬ Q) := by
     sorry
   

3. 证明 \(\lnot\forall x, P(x)\) 与 \(\exists x, \lnot P(x)\) 逻辑等价。本练习的要点是你正在证明表 5.1 中的引理 not_forall。所以不要使用该引理，也不要使用依赖它的策略 push_neg；请从零开始证明它。你需要使用排中律。

   example (P : α → Prop) : ¬ (∀ x, P x) ↔ ∃ x, ¬ P x := by
     sorry
   

4. 使用表 5.1 中的规则逐步证明：\(\lnot(\forall a b :\mathbb{Z}, ab=1 \to a = 1 \lor b = 1)\) 与 \(\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. 使用表 5.1 中的规则逐步证明：\(\lnot(\exists x:\mathbb{R},\forall y:\mathbb{R}, y \le x)\) 与 \(\forall x:\mathbb{R},\exists y:\mathbb{R}, y > x\) 逻辑等价。

   example : (¬ ∃ x : ℝ, ∀ y : ℝ, y ≤ x) ↔ (∀ x : ℝ, ∃ y : ℝ, y > x) :=
     sorry
   

6. 使用表 5.1 中的规则逐步证明：\(\lnot(\exists m:\mathbb{Z},\forall n:\mathbb{Z},m=n+5)\) 与 \(\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. 在脑中求出下面各否定的形式，然后用 Lean 输出检查你的结果。

   #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. 证明：并非对所有实数 \(x\)，都有 \(x^2\geq x\)。（我们已经在例 4.5.1 中解决过它；但这一次，请给出一个以 push_neg 开始的证明。）

   example : ¬ (∀ x : ℝ, x ^ 2 ≥ x) := by
     push_neg
     sorry
   

9. 证明：不存在实数 \(t\)，使得 \(t \le 4\) 且 \(t\geq 5\)。（我们已经在第 4.5 节的练习中解决过它；但这一次，请给出一个以 push_neg 开始的证明。）

   example : ¬ (∃ t : ℝ, t ≤ 4 ∧ t ≥ 5) := by
     push_neg
     sorry
   

10. 证明 7 不是偶数。（我们已经在第 4.5 节的练习中解决过它；但这一次，请给出一个以 push_neg 开始的证明。）

    example : ¬ Int.Even 7 := by
      dsimp [Int.Even]
      push_neg
      sorry
    

11. 设 \(p\) 和 \(k\) 为自然数，且 \(k\ne 1\)、\(k\ne p\)、\(k\mid p\)。证明 \(p\) 不是素数。（我们已经在例 4.5.7 中解决过它；但这一次，请给出一个以 push_neg 开始的证明。）

    example {p : ℕ} (k : ℕ) (hk1 : k ≠ 1) (hkp : k ≠ p) (hk : k ∣ p) : ¬ Prime p := by
      dsimp [Prime]
      push_neg
      sorry
    

12. 证明：不存在整数 \(a\)，使得对所有整数 \(n\)，都有 \(2a^3 ≥ na+7\)。建议结构：先把否定规范化。你可能会觉得，把这个事实与第 2.5 节第 8 题比较很有意思。这个陈述为假而那一个为真，怎么可能？

    example : ¬ ∃ a : ℤ, ∀ n : ℤ, 2 * a ^ 3 ≥ n * a + 7 := by
      sorry
    

13. 设 \(p \geq 2\) 为非素自然数。证明存在自然数 \(m\)，满足 \(2 \le m < p\)，且 \(m\) 是 \(p\) 的因子。我们把这个引理记录下来，以便以后用名称 exists_factor_of_not_prime 调用。建议结构：先设置一个中间目标，即“并非任意满足 \(2 \le m < p\) 的自然数 \(m\) 都不是 \(p\) 的因子”，并使用例 4.4.4 中的引理 prime_test 通过反证法证明它。然后把该结果的否定规范化。

    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