什么是证明？

命题逻辑

归纳（Induction）、演绎（Deduction）是同一公理系统的不同表现
- 归纳是从特殊结论到一般结论，比如归纳定义、结构归纳法
- 演绎是从一般结论到特殊结论，比如推理规则、演绎树
- 在从不动点定理到编程语言中，我们考虑归纳。在这里，我们考虑演绎
命题逻辑的语言
- 字母表
  - （命题变量） $p_1, p_2, \ldots$
  - （连词） $\wedge$ 、 $\vee$ 、 $\neg$ 、 $\Rightarrow$
  - （括号） $()$
  - 我们可以将 $\wedge$ 、 $\vee$ 、 $\neg$ 、 $\Rightarrow$ 分别视为与、或、非、推出。不过，我们应该用形式化的方式来演算
- 公式，归纳定义
  - 命题变量是公式
  - 如果 $A$ 、 $B$ 是公式，那么 $(A \wedge B)$ 、 $(A \vee B)$ 、 $(\neg A)$ 、 $(A \Rightarrow B)$ 也是公式
命题逻辑的公理系统
- 公理
  - （公理1） $A \Rightarrow (A \wedge A)$
  - （公理2） $(A \wedge B) \Rightarrow (B \wedge A)$
  - （公理3） $(A \Rightarrow B) \Rightarrow ((A \wedge C) \Rightarrow (B\wedge C))$
  - （公理4） $((A \Rightarrow B) \wedge (B \Rightarrow C)) \Rightarrow (A \Rightarrow C)$
  - （公理5） $B \Rightarrow (A \Rightarrow B)$
  - （公理6） $(A \wedge (A \Rightarrow B)) \Rightarrow B$
  - //
  - （公理7） $A \Rightarrow (A \vee B)$
  - （公理8） $(A \vee B) \Rightarrow (B \vee A)$
  - （公理9） $((A \Rightarrow C) \wedge (B \Rightarrow C)) \Rightarrow ((A \vee B) \Rightarrow C))$
  - //
  - （公理10） $((A \Rightarrow B) \wedge (A \Rightarrow \neg B)) \Rightarrow \neg A$
- 推理规则
  - 如果 $A$ 成立，并且 $A \Rightarrow B$ 成立，那么 $B$ 成立。这称为假言推理（Modus Ponens，MP），它类似于Aristotle的三段论
    $\dfrac{A \quad A \Rightarrow B}{B}$

从公理出发

导出过程（Derivation）是一列公式，其中，为下面两种情形之一
- $A_i$ 为公理
- $A_i$ 由前面的公式、MP得到
- 如果 $B = A_n$ ，那么 $B$ 称为定理（Theorem）。因为导出过程给出了 $B$ 的证明（Proof），所以 $B$ 也称为可证明的（Provable），记为 $\vdash B$
我们只有一个推理规则MP，如果直接从公理出发，那么导出过程会非常繁琐。因此，我们可以先建立一些中间结论，即引理（Lemma）。比如
- （-引入）如果、成立，那么成立
  - 1.（假设） $A$
  - 2.（公理5） $A \Rightarrow (B \Rightarrow A)$
  - 3.（MP 1、2） $B \Rightarrow A$
  - 4.（公理3） $(B \Rightarrow A) \Rightarrow ((B \wedge B) \Rightarrow (A \wedge B))$
  - 5.（MP 3、4） $(B \wedge B) \Rightarrow (A \wedge B)$
  - //
  - 6.（假设） $B$
  - 7.（公理1） $B \Rightarrow (B \wedge B)$
  - 8.（MP 6、7） $B \wedge B$
  - 9.（MP 5、8） $A \wedge B$
- （-传递）如果、成立，那么成立
  - 1.（假设） $A \Rightarrow B$
  - 2.（假设） $B \Rightarrow C$
  - 3.（ $\wedge$ -引入） $(A \Rightarrow B) \wedge (B \Rightarrow C)$
  - 4.（公理4） $((A \Rightarrow B) \wedge (B \Rightarrow C)) \Rightarrow (A \Rightarrow C)$
  - 5.（MP 3、4） $A \Rightarrow C$
- 利用 $\Rightarrow$ -传递，我们可以更方便地证明定理
（定理1）
- 1.（公理5） $A \Rightarrow (B \Rightarrow A)$
- 2.（公理3） $(A \Rightarrow (B \Rightarrow A)) \Rightarrow ((A \wedge B) \Rightarrow ((B \Rightarrow A) \wedge B))$
- 3.（MP 1、2） $(A \wedge B) \Rightarrow ((B \Rightarrow A) \wedge B)$
- 4.（公理2） $((B \Rightarrow A) \wedge B) \Rightarrow (B \wedge (B \Rightarrow A))$
- 5.（ $\Rightarrow$ -传递 3、4） $(A \wedge B) \Rightarrow (B \wedge (B \Rightarrow A))$
- 6.（公理6） $(B \wedge (B \Rightarrow A)) \Rightarrow A$
- 7.（ $\Rightarrow$ -传递 5、6) $(A \wedge B) \Rightarrow A$
定理1的导出过程等价于如下的演绎树，令 $C = (B \Rightarrow A)$
$\dfrac{\dfrac{\dfrac{Ax5 \quad Ax3}{(A \wedge B) \Rightarrow (C \wedge B)} \quad \dfrac{}{(C \wedge B) \Rightarrow (B \wedge C)}}{(A \wedge B) \Rightarrow (B \wedge C)} \quad \dfrac{}{(B \wedge C) \Rightarrow A}}{(A \wedge B) \Rightarrow A}$

从假设出发的导出过程

在建立上面的引理时，我们实际上使用了从假设出发的导出过程（Derivation from Assumptions），它在导出过程中，增加了属于假设的情形
- 如果 $B = A_n$ ，那么 $B$ 称为（从 $\Gamma$ 出发）可导出的（Derivable），记为 $\Gamma \vdash B$
- 如果 $B$ 为可证明的，那么 $B$ 为可导出的，此时 $\Gamma = \emptyset$
基本性质
- （公理）如果 $A$ 为公理，那么 $\emptyset \vdash A$
- （假设）如果 $A \in \Gamma$ ，那么 $\Gamma \vdash A$
- （减弱）如果 $\Gamma \vdash A$ ， $\Gamma \subset \Gamma^*$ ，那么 $\Gamma^* \vdash A$
- （MP）如果，，那么
  - 我们有从 $\Gamma$ 、 $\Delta$ 出发的导出过程
    $A_1, \ldots, A_n = A,\; B_1, \ldots, B_m = (A \Rightarrow B).$
  - 因此，我们有从 $\Gamma \cup \Delta$ 出发的导出过程
    $A_1, \ldots, A_n,\; B_1, \ldots, B_m,\; B.$
- 类似地，我们可以得到 $\wedge$ -引入、 $\Rightarrow$ -传递
（演绎定理，Deduction Theorem）如果，那么
- 我们有从 $\Gamma, A$ 出发的导出过程 $B_1, \ldots, B_n = B$ 。对 $n$ 使用数学归纳法
- 当时，我们有如下3种情形
  - 为公理
    - 1.（公理） $\emptyset \vdash B$
    - 2.（公理5） $\emptyset \vdash (B \Rightarrow (A \Rightarrow B))$
    - 3.（MP 1、2） $\emptyset \vdash (A \Rightarrow B)$
    - 4.（减弱） $\Gamma \vdash (A \Rightarrow B)$
  - - 1.（公理1、定理1） $\emptyset \vdash (A \Rightarrow A)$
    - 2.（减弱） $\Gamma \vdash (A \Rightarrow A)$
  - - 1.（假设） $\Gamma \vdash B$
    - 2.（公理5） $\emptyset \vdash (B \Rightarrow (A \Rightarrow B))$
    - 3.（MP 1、2） $\Gamma \vdash (A \Rightarrow B)$
- 如果对于小于的情形成立，那么考虑的情形。我们需要使用一个可证明的定理
  $\emptyset \vdash (A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))$
  - 如果 $B$ 为公理、 $B = A$ 、 $B \in \Gamma$ ，那么由上述可知， $\Gamma \vdash (A \Rightarrow B)$
  - 如果由MP得到，那么存在、，使得、
    - 1.（归纳假设） $\Gamma \vdash (A \Rightarrow B_i)$
    - 2.（归纳假设） $\Gamma \vdash (A \Rightarrow (B_i \Rightarrow B))$
    - 3.（一个可证明的定理） $\emptyset \vdash (A \Rightarrow (B_i \Rightarrow B)) \Rightarrow ((A \Rightarrow B_i) \Rightarrow (A \Rightarrow B))$
    - 4.（MP 2、3） $\Gamma \vdash ((A \Rightarrow B_i) \Rightarrow (A \Rightarrow B))$
    - 5.（MP 1、4） $\Gamma \vdash (A \Rightarrow B)$

公理系统的独立性

Hilbert认为，公理系统应该满足如下条件。对于、，可证明的公式数量记为
- （相容性） $n < 2$
- （完备性） $n > 0$
- （独立性）一条公理不能由其余公理导出
公理系统的例子
- 算术的公理系统具有相容性。然而，由Gödel不完备定理可知，算术的公理系统不具有完备性
- Euclid几何的公理系统具有独立性。其中，平行公设不能由其他公设导出，这可以通过构造非Euclid几何的模型得到。关于平行公设，可参见从Euclid几何到非Euclid几何
- 因此，我们既需要考虑证明论（Proof Theory），也需要考虑模型论（Model Theory）
之前，我们讨论的公理系统为最小逻辑系统，它关于只有一个公理
- （公理10） $((A \Rightarrow B) \wedge (A \Rightarrow \neg B)) \Rightarrow \neg A$
现在，我们添加关于的公理