本章所采用的形式理论，其完整内容可以参考一阶逻辑#型式理论。
前提假设以Hyp简记
推论元定理以"D"简记，内容可以参考形式理论#推论元定理。
由推论元定理可以知道$\vdash\mathcal{A}\Rightarrow\mathcal{B}$和$\mathcal{A}\vdash\mathcal{B}$是一样的意思。所以证明过程中，你会看到代号D跟中途运用定理的代号写在一起的简记法，因为我们有时候会用$\mathcal{A}\vdash\mathcal{B}$的形式表达定理。
另外有两个常用的推论，是来自于推论元定理
$\displaystyle (D1)$$\mathcal{A}\Rightarrow\mathcal{B},\mathcal{B}\Rightarrow\mathcal{C}\vdash\mathcal{A}\Rightarrow\mathcal{C}$
$\displaystyle (D2)$$\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C}),\mathcal{B}\vdash\mathcal{A}\Rightarrow\mathcal{C}$
下面应用(D1)或(D2)构造证明的时候，实际上相当于施用两次MP律；但只要我们写出应用(D1)或(D2)所需要的两段$\displaystyle wfs$的代号，省略中间这段真正的过程，对理解证明是无伤大雅的。类似的，证明过程采用的定理，会以代号标记在它的推理结果后面，并写明是运用哪个推理规则，但不会直接列出定理的完全形式。
$\displaystyle(I)$推论的恒等(Identity of imply)
$\vdash\mathcal{A}\Rightarrow\mathcal{A}$
证明：请参考形式理论#证明讲解的范例。
$\displaystyle (DNe)$双否定(消去)(Double negation, elimination)
$\vdash\neg\neg\mathcal{A}\Rightarrow\mathcal{A}$
| 证明 |
|---|
|
(1)$(\neg\mathcal{A}\Rightarrow\neg\neg\mathcal{A})\Rightarrow[(\neg\mathcal{A}\Rightarrow\neg\mathcal{A})\Rightarrow\mathcal{A}]$ (A3) (2)$\neg\mathcal{A}\Rightarrow\neg\mathcal{A}$ (I) (3)$(\neg\mathcal{A}\Rightarrow\neg\neg\mathcal{A})\Rightarrow\mathcal{A}$ (D2 with 1, 2) (4)$\neg\neg\mathcal{A}\Rightarrow(\neg\mathcal{A}\Rightarrow\neg\neg\mathcal{A})$ (A1) (5)$\neg\neg\mathcal{A}\Rightarrow\mathcal{A}$ (D1 with 3, 4) |
$\displaystyle (DNi)$双否定(引入)(Double negation, introduction)
$\vdash\mathcal{A}\Rightarrow\neg\neg\mathcal{A}$
| 证明 |
|---|
|
(1)$(\neg\neg\neg\mathcal{A}\Rightarrow\neg\mathcal{A})\Rightarrow[(\neg\neg\neg\mathcal{A}\Rightarrow\mathcal{A})\Rightarrow\neg\neg\mathcal{A}]$ (A3) (2)$(\neg\neg\neg\mathcal{A}\Rightarrow\mathcal{A})\Rightarrow\neg\neg\mathcal{A}$ (MP with DNe, 1) (3)$\mathcal{A}\Rightarrow(\neg\neg\neg\mathcal{A}\Rightarrow\mathcal{A})$ (A1) (4)$\mathcal{A}\Rightarrow\neg\neg\mathcal{A}$ (D1 with 2,3) |
上面两定理表达了双否定推理上等价于于原$\displaystyle wf$，日后引用两者任一会以DN简写。
$\displaystyle (T1)$(Transposition)
$\neg\mathcal{A}\Rightarrow\neg\mathcal{B}\vdash\mathcal{B}\Rightarrow\mathcal{A}$
| 证明 |
|---|
|
(1)$(\neg\mathcal{A}\Rightarrow\neg\mathcal{B})\Rightarrow[(\neg\mathcal{A}\Rightarrow\mathcal{B})\Rightarrow\mathcal{A}]$ (A3) (2)$\neg\mathcal{A}\Rightarrow\neg\mathcal{B}$ (Hyp) (3)$(\neg\mathcal{A}\Rightarrow\mathcal{B})\Rightarrow\mathcal{A}$ (MP with 1, 2) (4)$\mathcal{B}\Rightarrow(\neg\mathcal{A}\Rightarrow\mathcal{B})$ (A1) (5)$\mathcal{B}\Rightarrow\mathcal{A}$ (D1 with 3, 4) |
$\displaystyle (T2)$(Transposition)
$\mathcal{B}\Rightarrow\mathcal{A}\vdash\neg\mathcal{A}\Rightarrow\neg\mathcal{B}$
| 证明 |
|---|
|
(1)$\neg\neg\mathcal{B}\Rightarrow\mathcal{B}$ (DN) (2)$\mathcal{B}\Rightarrow\mathcal{A}$ (Hyp) (3)$\neg\neg\mathcal{B}\Rightarrow\mathcal{A}$ (D1 with 1, 2) (4)$\mathcal{A}\Rightarrow\neg\neg\mathcal{A}$ (DN) (5)$\neg\neg\mathcal{B}\Rightarrow\neg\neg\mathcal{A}$ (D1 with 3,4) (6)$(\neg\neg\mathcal{B}\Rightarrow\neg\neg\mathcal{A})\Rightarrow(\neg\mathcal{A}\Rightarrow\neg\mathcal{B})$ (T1, D) (7)$\neg\mathcal{A}\Rightarrow\neg\mathcal{B}$ (MP with 5, 6) |
这两个定理表说明$\mathcal{B}\Rightarrow\mathcal{A}$推理上等价于$\neg\mathcal{A}\Rightarrow\neg\mathcal{B}$，日后引用这两个定理其中任一，都用(T)表示。
另外这两个定理也是反证法(proof by contradiction)其中的两种状况。
以下的定理重现了实质条件直观的定义
$\displaystyle(M0)$(material condition)
$\neg\mathcal{A},\mathcal{A}\vdash\mathcal{B}$
(由(D)，也就是$\neg\mathcal{A}\vdash\mathcal{A}\Rightarrow\mathcal{B}$)
| 证明 |
|---|
|
(1)$\neg\mathcal{A}$ (Hyp) (2)$\mathcal{A}$ (Hyp) (3)$(\neg\mathcal{B}\Rightarrow\neg\mathcal{A})\Rightarrow[(\neg\mathcal{B}\Rightarrow\mathcal{A})\Rightarrow\mathcal{B}]$ (A3) (4)$\neg\mathcal{A}\Rightarrow(\neg\mathcal{B}\Rightarrow\neg\mathcal{A})$ (A1) (5)$\neg\mathcal{B}\Rightarrow\neg\mathcal{A}$ (MP with 4, 1) (6)$\mathcal{A}\Rightarrow(\neg\mathcal{B}\Rightarrow\mathcal{A})$ (A1) (7)$\neg\mathcal{B}\Rightarrow\mathcal{A}$ (MP with 6, 2) (8)$(\neg\mathcal{B}\Rightarrow\mathcal{A})\Rightarrow\mathcal{B}$ (MP with 3,5) (9)$\mathcal{B}$ (MP with 8,7) |
$\displaystyle (M1)$(material condition)
$\mathcal{A},\neg\mathcal{B}\vdash\neg(\mathcal{A}\Rightarrow\mathcal{B})$
| 证明 |
|---|
|
首先注意到(0)$\mathcal{A},\mathcal{A}\Rightarrow\mathcal{B}\vdash\mathcal{B}$ (MP) (1)$\mathcal{A}\Rightarrow[(\mathcal{A}\Rightarrow\mathcal{B})\Rightarrow\mathcal{B}]$ (0, D) (2)$[(\mathcal{A}\Rightarrow\mathcal{B})\Rightarrow\mathcal{B}]\Rightarrow\{\neg\mathcal{B}\Rightarrow[\neg(\mathcal{A}\Rightarrow\mathcal{B})]\}$ (T) (3)$\mathcal{A}$ (Hyp) (4)$(\mathcal{A}\Rightarrow\mathcal{B})\Rightarrow\mathcal{B}$ (MP with 1, 3) (5)$\neg\mathcal{B}\Rightarrow[\neg(\mathcal{A}\Rightarrow\mathcal{B})]$ (MP with 2, 4) (6)$\neg\mathcal{B}$ (Hyp) (7)$\neg(\mathcal{A}\Rightarrow\mathcal{B})$ (MP 5, 6) |
$\displaystyle (M2)$(material condition)
$\neg(\mathcal{A}\Rightarrow\mathcal{B})\vdash\neg\mathcal{B}$
| 证明 |
|---|
|
(1)$\mathcal{B}\Rightarrow(\mathcal{A}\Rightarrow\mathcal{B})$ (A1) (2)$[\mathcal{B}\Rightarrow(\mathcal{A}\Rightarrow\mathcal{B})]\Rightarrow\{[\neg(\mathcal{A}\Rightarrow\mathcal{B})]\Rightarrow(\neg\mathcal{B})\}$ (T) (3)$[\neg(\mathcal{A}\Rightarrow\mathcal{B})]\Rightarrow(\neg\mathcal{B})$ (MP with 1, 2) (4)$\neg(\mathcal{A}\Rightarrow\mathcal{B})$ (Hyp) (5)$\neg\mathcal{B}$ (MP with 3, 4) |
$\displaystyle (M3)$(material condition)
$\neg(\mathcal{A}\Rightarrow\mathcal{B})\vdash\mathcal{A}$
| 证明 |
|---|
|
(1)$\neg\mathcal{A}\Rightarrow(\mathcal{A}\Rightarrow\mathcal{B})$ (M0, D) (2)$[\neg\mathcal{A}\Rightarrow(\mathcal{A}\Rightarrow\mathcal{B})]\Rightarrow\{[\neg(\mathcal{A}\Rightarrow\mathcal{B})]\Rightarrow(\neg\neg\mathcal{A})\}$ (T) (3)$[\neg(\mathcal{A}\Rightarrow\mathcal{B})]\Rightarrow(\neg\neg\mathcal{A})$ (MP with 1, 2) (4)$\neg(\mathcal{A}\Rightarrow\mathcal{B})$ (Hyp) (5)$\neg\neg\mathcal{A}$ (MP with 3,4) (6)$\mathcal{A}$ (MP with 5, DN) |
$\displaystyle(C1)$(proof by contradiction)
$\mathcal{A}\Rightarrow\neg\mathcal{B},\mathcal{B}\vdash\neg\mathcal{A}$
| 证明 |
|---|
|
(1)$(\mathcal{A}\Rightarrow\neg\mathcal{B})\Rightarrow(\neg\neg\mathcal{B}\Rightarrow\neg\mathcal{A})$ (T, D) (2)$\mathcal{A}\Rightarrow\neg\mathcal{B}$ (Hyp) (3)$\neg\neg\mathcal{B}\Rightarrow\neg\mathcal{A}$ (MP with 1, 2) (4)$\mathcal{B}$ (Hyp) (5)$\neg\neg\mathcal{B}$ (MP with DN, 4) (6)$\neg\mathcal{A}$ (MP with 3, 5) |
$\displaystyle(C2)$(proof by contradiction)
$\neg\mathcal{A}\Rightarrow\mathcal{B},\neg\mathcal{B}\vdash\mathcal{A}$
证明提示：仿$\displaystyle(C1)$的证明。
利用推论元定理把前提条件移到"$\vdash$"后面，可以发现(C1)和(C2)也是换位。
$\displaystyle (A3')$(Proof by contradiction)
$\mathcal{A}\Rightarrow\mathcal{B},\neg\mathcal{A}\Rightarrow\mathcal{B}\vdash\mathcal{B}$
| 证明 |
|---|
|
(1)$(\neg\mathcal{B}\Rightarrow\neg\neg\mathcal{A})\Rightarrow[(\neg\mathcal{B}\Rightarrow\neg\mathcal{A})\Rightarrow\mathcal{B}]$ (A3) (2)$(\neg\mathcal{A}\Rightarrow\mathcal{B})\Rightarrow(\neg\mathcal{B}\Rightarrow\neg\neg\mathcal{A})$ (T, D) (3)$\neg\mathcal{A}\Rightarrow\mathcal{B}$ (Hyp) (4)$\neg\mathcal{B}\Rightarrow\neg\neg\mathcal{A}$ (MP with 2, 3) (5)$(\neg\mathcal{B}\Rightarrow\neg\mathcal{A})\Rightarrow\mathcal{B}$ (MP with 1, 4) (6)$(\mathcal{A}\Rightarrow\mathcal{B})\Rightarrow(\neg\mathcal{B}\Rightarrow\neg\mathcal{A})$ (T, D) (7)$\mathcal{A}\Rightarrow\mathcal{B}$ (Hyp) (8)$\neg\mathcal{B}\Rightarrow\neg\mathcal{A}$ (MP with 6, 7) (9)$\mathcal{B}$ (MP with 5, 8) |
"且"和"或"的形式定义请参考命题逻辑#且和或
其实由(C1)可以发现"且"的"交换性"：
$\vdash(\mathcal{A}\wedge\mathcal{B})\Rightarrow(\mathcal{B}\wedge\mathcal{A})$
| 证明 |
|---|
|
(1)$(\mathcal{B}\Rightarrow\neg\mathcal{A})\Rightarrow(\mathcal{A}\Rightarrow\neg\mathcal{B})$ (C1, D) (2)$[(\mathcal{B}\Rightarrow\neg\mathcal{A})\Rightarrow(\mathcal{A}\Rightarrow\neg\mathcal{B})]\Rightarrow\{[\neg(\mathcal{A}\Rightarrow\neg\mathcal{B})]\Rightarrow[\neg(\mathcal{B}\Rightarrow\neg\mathcal{A})]\}$ (T, D) (3)$[\neg(\mathcal{A}\Rightarrow\neg\mathcal{B})]\Rightarrow[\neg(\mathcal{B}\Rightarrow\neg\mathcal{A})]$ (MP with 1,2) |
类似的，(C2)正是"或"的"可交换性"：
$\mathcal{A}\vee\mathcal{B}\vdash\mathcal{B}\vee\mathcal{A}$ (C2, D)
"且"的直观意义是实质条件定理的直接结果
$\mathcal{A},\mathcal{B}\vdash\mathcal{A}\wedge\mathcal{B}$ (M1)
$\mathcal{A}\wedge\mathcal{B}\vdash\mathcal{A}$ (M3)
$\mathcal{A}\wedge\mathcal{B}\vdash\mathcal{B}$ (M2)
类似的，"或"的直观意义是(M0)跟推论元定理的直截结果
$\mathcal{A}\vdash\mathcal{A}\vee\mathcal{B}$ (M0, DN)
$\mathcal{B}\vdash\mathcal{A}\vee\mathcal{B}$ (A1, D)
$\mathcal{A}\vee\mathcal{B},\neg\mathcal{A}\vdash\mathcal{B}$ (D)
$\mathcal{A}\vee\mathcal{B},\neg\mathcal{B}\vdash\mathcal{A}$ (交换性, D)
以下的定理则是(A3')的直截结果
$\displaystyle (Dis)$(Disjunction)
$\mathcal{A}\Rightarrow\mathcal{C},\mathcal{B}\Rightarrow\mathcal{C},\mathcal{A}\vee\mathcal{B}\vdash\mathcal{C}$
| 证明 |
|---|
|
(1)$\neg\mathcal{A}\Rightarrow\mathcal{B}$ (Hyp) (2)$\mathcal{B}\Rightarrow\mathcal{C}$ (Hyp) (3)$\neg\mathcal{A}\Rightarrow\mathcal{C}$ (D1 with 1, 2) (4)$\mathcal{A}\Rightarrow\mathcal{C}$ (Hyp) 3,4带入定理(A3')就会得到$\mathcal{C}$。$\Box$ |
以下的定理都可以用真假值去理解；所以被引用时一律以De Morgan代称(纪念英国逻辑学家Augustus De Morgan)
De Morgan I(left)：
$\neg(\mathcal{A}\wedge\mathcal{B})\vdash(\neg\mathcal{A})\vee(\neg\mathcal{B})$
| 证明 |
|---|
|
(1)$\neg\neg[\mathcal{A}\Rightarrow(\neg\mathcal{B})]$ (Hyp) (2)$\mathcal{A}\Rightarrow(\neg\mathcal{B})$ (MP with 1, DN) (3)$\neg\neg\mathcal{A}\Rightarrow\mathcal{A}$ (DN) (4)$\neg\neg\mathcal{A}\Rightarrow(\neg\mathcal{B})$ (D1 with 2, 3) |
De Morgan I(Right)：
$(\neg\mathcal{A})\vee(\neg\mathcal{B})\vdash\neg(\mathcal{A}\wedge\mathcal{B})$
| 证明 |
|---|
|
(1)$\neg\neg\mathcal{A}\Rightarrow(\neg\mathcal{B})$ (Hyp) (2)$\mathcal{A}\Rightarrow\neg\neg\mathcal{A}$ (DN) (3)$\mathcal{A}\Rightarrow(\neg\mathcal{B})$ (D1 with 1, 2) (4)$\neg\neg[\mathcal{A}\Rightarrow(\neg\mathcal{B})]$ (MP with DN, 3) |
De Morgan II(left)：
$\vdash[\neg(\mathcal{A}\vee\mathcal{B})]\Rightarrow[(\neg\mathcal{A})\wedge(\neg\mathcal{B})]$
| 证明 |
|---|
|
注意到(0)$(\neg\mathcal{A})\Rightarrow(\neg\neg\mathcal{B}),\neg\mathcal{A}\vdash\mathcal{B}$ (DN) (1)$[(\neg\mathcal{A})\Rightarrow(\neg\neg\mathcal{B})]\Rightarrow(\neg\mathcal{A}\Rightarrow\mathcal{B})$ (0, D) (2)$\{[(\neg\mathcal{A})\Rightarrow(\neg\neg\mathcal{B})]\Rightarrow(\neg\mathcal{A}\Rightarrow\mathcal{B})\}\Rightarrow\{\neg(\neg\mathcal{A}\Rightarrow\mathcal{B})\Rightarrow\neg[(\neg\mathcal{A})\Rightarrow(\neg\neg\mathcal{B})]\}$ (T) (3)$\neg(\neg\mathcal{A}\Rightarrow\mathcal{B})\Rightarrow\neg[(\neg\mathcal{A})\Rightarrow(\neg\neg\mathcal{B})]$ (MP with 1, 2) |
De Morgan II(right)：
$\vdash[(\neg\mathcal{A})\wedge(\neg\mathcal{B})]\Rightarrow[\neg(\mathcal{A}\vee\mathcal{B})]$
证明提示：仿De Morgan II(left)