弗雷格命题演算
Frege 公理证明标准公理

下列定理致力于在 Frege 的 PC 的“定理空间”内找出标准 PC 的余下九个公理，展示标准 PC 的定理被包含在 Frege 的 PC 的定理中。
(出于比喻的目的，这里所谓的理论的“定理空间”，是一个定理的集合，它是合式公式全集的子集。定理通过推理规则的直接方式相互连接起来，形成一种树状网络。)
约定 ((A→B)→B) 等同于 A∨B，¬(A→¬B) 等同于 A∧B。
规则 THEN-1*: A  \vdash \, B→A
| # | wff | 理由 |
| --- | --- | --- |
| 1. | A | 前提 |
| 2. | A→(B→A) | THEN-1 |
| 3. | B→A | MP 1,2. |
规则 THEN-2*:  A→(B→C)  \vdash \, (A→B)→(A→C)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | A→(B→C) | 前提 |
| 2. | (A→(B→C))→((A→B)→(A→C)) | THEN-2 |
| 3. | (A→B)→(A→C) | MP 1,2. |
规则 THEN-3*: A→(B→C)  \vdash \, B→(A→C)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | A→(B→C) | 前提 |
| 2. | (A→(B→C))→(B→(A→C)) | THEN-3 |
| 3. | B→(A→C) | MP 1,2. |
规则 FRG-1*: A→B  \vdash \, ¬B→¬A
| # | wff | 理由 |
| --- | --- | --- |
| 1. | (A→B)→(¬B→¬A) | FRG-1 |
| 2. | A→B | 前提 |
| 3. | ¬B→¬A | MP 2,1. |
规则 TH1*: A→B, B→C  \vdash \, A→C
| # | wff | 理由 |
| --- | --- | --- |
| 1. | B→C | 前提 |
| 2. | (B→C)→(A→(B→C)) | THEN-1 |
| 3. | A→(B→C) | MP 1,2 |
| 4. | (A→(B→C))→((A→B)→(A→C)) | THEN-2 |
| 5. | (A→B)→(A→C) | MP 3,4 |
| 6. | A→B | 前提 |
| 7. | A→C | MP 6,5. |
定理 TH1: (A→B)→((B→C)→(A→C))
| # | wff | 理由 |
| --- | --- | --- |
| 1. | (B→C)→(A→(B→C)) | THEN-1 |
| 2. | (A→(B→C))→((A→B)→(A→C)) | THEN-2 |
| 3. | (B→C)→((A→B)→(A→C)) | TH1* 1,2 |
| 4. | ((B→C)→((A→B)→(A→C)))→((A→B)→((B→C)→(A→C))) | THEN-3 |
| 5. | (A→B)→((B→C)→(A→C)) | MP 3,4. |
定理 TH2: A→(¬A→¬B)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | A→(B→A) | THEN-1 |
| 2. | (B→A)→(¬A→¬B) | FRG-1 |
| 3. | A→(¬A→¬B) | TH1* 1,2. |
定理 TH3: ¬A→(A→¬B)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | A→(¬A→¬B) | TH 2 |
| 2. | (A→(¬A→¬B))→(¬A→(A→¬B)) | THEN-3 |
| 3. | ¬A→(A→¬B) | MP 1,2. |
定理 TH4: ¬(A→¬B)→A
| # | wff | 理由 |
| --- | --- | --- |
| 1. | ¬A→(A→¬B) | TH3 |
| 2. | (¬A→(A→¬B))→(¬(A→¬B)→¬¬A) | FRG-1 |
| 3. | ¬(A→¬B)→¬¬A | MP 1,2 |
| 4. | ¬¬A→A | FRG-2 |
| 5. | ¬(A→¬B)→A | TH1* 3,4. |
¬(A→¬B)→A 就是公理 AND-1：A∧B→A。
定理 TH5: (A→¬B)→(B→¬A)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | (A→¬B)→(¬¬B→¬A) | FRG-1 |
| 2. | ((A→¬B)→(¬¬B→¬A))→(¬¬B→((A→¬B)→¬A)) | THEN-3 |
| 3. | ¬¬B→((A→¬B)→¬A) | MP 1,2 |
| 4. | B→¬¬B | FRG-3, 通过 A := B |
| 5. | B→((A→¬B)→¬A) | TH1* 4,3 |
| 6. | (B→((A→¬B)→¬A))→((A→¬B)→(B→¬A)) | FRG-1 |
| 7. | (A→¬B)→(B→¬A) | MP 5,6. |
定理 TH6: ¬(A→¬B)→B
| # | wff | 理由 |
| --- | --- | --- |
| 1. | ¬(B→¬A)→B | TH4, 通过 A := B, B := A |
| 2. | (B→¬A)→(A→¬B) | TH5, 通过 A := B, B := A |
| 3. | ((B→¬A)→(A→¬B))→(¬(A→¬B)→¬(B→¬A)) | FRG-1 |
| 4. | ¬(A→¬B)→¬(B→¬A) | MP 2,3 |
| 5. | ¬(A→¬B)→B | TH1* 4,1. |
¬(A→¬B)→B 就是公理 AND-2：A∧B→B。
定理 TH7: A→A
| # | wff | 理由 |
| --- | --- | --- |
| 1. | A→¬¬A | FRG-3 |
| 2. | ¬¬A→A | FRG-2 |
| 3. | A→A | TH1* 1,2. |
定理 TH8: A→((A→B)→B)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | (A→B)→(A→B) | TH7, 通过 A := A→B |
| 2. | ((A→B)→(A→B))→(A→((A→B)→B)) | THEN-3 |
| 3. | A→((A→B)→B) | MP 1,2. |
A→((A→B)→B) 就是公理 OR-1：A→A∨B。
定理 TH9: B→((A→B)→B)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | B→((A→B)→B) | THEN-1, 通过 A := B, B := A→B. |
B→((A→B)→B) 就是公理 OR-2：B→A∨B。
定理 TH10: A→(B→¬(A→¬B))
| # | wff | 理由 |
| --- | --- | --- |
| 1. | (A→¬B)→(A→¬B) | TH7 |
| 2. | ((A→¬B)→(A→¬B))→(A→((A→¬B)→¬B) | THEN-3 |
| 3. | A→((A→¬B)→¬B) | MP 1,2 |
| 4. | ((A→¬B)→¬B)→(B→¬(A→¬B)) | TH5 |
| 5. | A→(B→¬(A→¬B)) | TH1* 3,4. |
A→(B→¬(A→¬B)) 就是公理 AND-3：A→(B→ A∧B) 。
定理 TH11: (A→B)→((A→¬B)→¬A)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | A→(B→¬(A→¬B)) | TH10 |
| 2. | (A→(B→¬(A→¬B)))→((A→B)→(A→¬(A→¬B))) | THEN-2 |
| 3. | (A→B)→(A→¬(A→¬B)) | MP 1,2 |
| 4. | (A→¬(A→¬B))→((A→¬B)→¬A) | TH5 |
| 5. | (A→B)→((A→¬B)→¬A) | TH1* 3,4. |
TH11 就是标准 PC 叫做“反证法”的公理 NOT-1。
定理 TH12: ((A→B)→C)→(A→(B→C))
| # | wff | 理由 |
| --- | --- | --- |
| 1. | B→(A→B) | THEN-1 |
| 2. | (B→(A→B))→(((A→B)→C)→(B→C)) | TH1 |
| 3. | ((A→B)→C)→(B→C) | MP 1,2 |
| 4. | (B→C)→(A→(B→C)) | THEN-1 |
| 5. | ((A→B)→C)→(A→(B→C)) | TH1* 3,4. |
定理 TH13: (B→(B→C))→(B→C)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | (B→(B→C))→((B→B)→(B→C)) | THEN-2 |
| 2. | (B→B)→( (B→(B→C))→(B→C)) | THEN-3* 1 |
| 3. | B→B | TH7 |
| 4. | (B→(B→C))→(B→C) | MP 3,2. |
规则 TH14*: A→(B→P), P→Q  \vdash \, A→(B→Q)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | P→Q | 前提 |
| 2. | (P→Q)→(B→(P→Q)) | THEN-1 |
| 3. | B→(P→Q) | MP 1,2 |
| 4. | (B→(P→Q))→((B→P)→(B→Q)) | THEN-2 |
| 5. | (B→P)→(B→Q) | MP 3,4 |
| 6. | ((B→P)→(B→Q))→ (A→((B→P)→(B→Q))) | THEN-1 |
| 7. | A→((B→P)→(B→Q)) | MP 5,6 |
| 8. | (A→(B→P))→(A→(B→Q)) | THEN-2* 7 |
| 9. | A→(B→P) | 前提 |
| 10. | A→(B→Q) | MP 9,8. |
定理 TH15: ((A→B)→(A→C))→(A→(B→C))
| # | wff | 理由 |
| --- | --- | --- |
| 1. | ((A→B)→(A→C))→(((A→B)→A)→((A→B)→C)) | THEN-2 |
| 2. | ((A→B)→C)→(A→(B→C)) | TH12 |
| 3. | ((A→B)→(A→C))→(((A→B)→A)→(A→(B→C))) | TH14* 1,2 |
| 4. | ((A→B)→A)→( ((A→B)→(A→C))→(A→(B→C))) | THEN-3* 3 |
| 5. | A→((A→B)→A) | THEN-1 |
| 6. | A→( ((A→B)→(A→C))→(A→(B→C)) ) | TH1* 5,4 |
| 7. | ((A→B)→(A→C))→(A→(A→(B→C))) | THEN-3* 6 |
| 8. | (A→(A→(B→C)))→(A→(B→C)) | TH13 |
| 9. | ((A→B)→(A→C))→(A→(B→C)) | TH1* 7,8. |
TH15 是公理 THEN-2 的逆命题。
定理 TH16: (¬A→¬B)→(B→A)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | (¬A→¬B)→(¬¬B→¬¬A) | FRG-1 |
| 2. | ¬¬B→((¬A→¬B)→¬¬A) | THEN-3* 1 |
| 3. | B→¬¬B | FRG-3 |
| 4. | B→((¬A→¬B)→¬¬A) | TH1* 3,2 |
| 5. | (¬A→¬B)→(B→¬¬A) | THEN-3* 4 |
| 6. | ¬¬A→A | FRG-2 |
| 7. | (¬¬A→A)→(B→(¬¬A→A)) | THEN-1 |
| 8. | B→(¬¬A→A) | MP 6,7 |
| 9. | (B→(¬¬A→A))→((B→¬¬A)→(B→A)) | THEN-2 |
| 10. | (B→¬¬A)→(B→A) | MP 8,9 |
| 11. | (¬A→¬B)→(B→A) | TH1* 5,10. |
定理 TH17: (¬A→B)→(¬B→A)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | (¬A→¬¬B)→(¬B→A) | TH16, 通过 B := ¬B |
| 2. | B→¬¬B | FRG-3 |
| 3. | (B→¬¬B)→(¬A→(B→¬¬B)) | THEN-1 |
| 4. | ¬A→(B→¬¬B) | MP 2,3 |
| 5. | (¬A→(B→¬¬B))→((¬A→B)→(¬A→¬¬B)) | THEN-2 |
| 6. | (¬A→B)→(¬A→¬¬B) | MP 4,5 |
| 7. | (¬A→B)→(¬B→A) | TH1* 6,1. |
比较定理 TH17 与定理 TH5。
定理 TH18: ((A→B)→B)→(¬A→B)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | (A→B)→(¬B→(A→B)) | THEN-1 |
| 2. | (¬B→¬A)→(A→B) | TH16 |
| 3. | (¬B→¬A)→(¬B→(A→B)) | TH1* 2,1 |
| 4. | ((¬B→¬A)→(¬B→(A→B)))→(¬B→(¬A→(A→B))) | TH15 |
| 5. | ¬B→(¬A→(A→B)) | MP 3,4 |
| 6. | (¬A→(A→B))→(¬(A→B)→A) | TH17 |
| 7. | ¬B→(¬(A→B)→A) | TH1* 5,6 |
| 8. | (¬B→(¬(A→B)→A))→ ((¬B→¬(A→B))→(¬B→A)) | THEN-2 |
| 9. | (¬B→¬(A→B))→(¬B→A) | MP 7,8 |
| 10. | ((A→B)→B)→(¬B→¬(A→B)) | FRG-1 |
| 11. | ((A→B)→B)→(¬B→A) | TH1* 10,9 |
| 12. | (¬B→A)→(¬A→B) | TH17 |
| 13. | ((A→B)→B)→(¬A→B) | TH1* 11,12. |
定理 TH19: (A→C)→ ((B→C)→(((A→B)→B)→C))
| # | wff | 理由 |
| --- | --- | --- |
| 1. | ¬A→(¬B→¬(¬A→¬¬B)) | TH10 |
| 2. | B→¬¬B | FRG-3 |
| 3. | (B→¬¬B)→(¬A→(B→¬¬B)) | THEN-1 |
| 4. | ¬A→(B→¬¬B) | MP 2,3 |
| 5. | (¬A→(B→¬¬B))→((¬A→B)→(¬A→¬¬B)) | THEN-2 |
| 6. | (¬A→B)→(¬A→¬¬B) | MP 4,5 |
| 7. | ¬(¬A→¬¬B)→¬(¬A→B) | FRG-1* 6 |
| 8. | ¬A→(¬B→¬(¬A→B)) | TH14* 1,7 |
| 9. | ((A→B)→B)→(¬A→B) | TH18 |
| 10. | ¬(¬A→B)→¬((A→B)→B) | FRG-1* 9 |
| 11. | ¬A→(¬B→¬((A→B)→B)) | TH14* 8,10 |
| 12. | ¬C→(¬A→(¬B→¬((A→B)→B))) | THEN-1* 11 |
| 13. | (¬C→¬A)→(¬C→(¬B→¬((A→B)→B))) | THEN-2* 12 |
| 14. | (¬C→(¬B→¬((A→B)→B)))→((¬C→¬B)→(¬C→¬((A→B)→B))) | THEN-2 |
| 15. | (¬C→¬A)→ ((¬C→¬B)→(¬C→¬((A→B)→B))) | TH1* 13,14 |
| 16. | (A→C)→(¬C→¬A) | FRG-1 |
| 17. | (A→C)→((¬ C→¬B)→(¬C→¬((A→B)→B))) | TH1* 16,15 |
| 18. | (¬C→¬((A→B)→B))→(((A→B)→B)→C) | TH16 |
| 19. | (A→C)→ ((¬C→¬B)→(((A→B)→B)→C)) | TH14* 17,18 |
| 20. | (B→C)→(¬C→¬B) | FRG-1 |
| 21. | ((B→C)→(¬C→¬B))→  (((¬C→¬B)→ (((A→B)→B)→C) )→( (B→C)→ (((A→B)→B)→C))) | TH1 |
| 22. | ((¬C→¬B)→ (((A→B)→B)→C) )→( (B→C)→ (((A→B)→B)→C)) | MP 20,21 |
| 23. | (A→C)→ ((B→C)→(((A→B)→B)→C)) | TH1* 19,22. |
(A→C)→((B→C)→(((A→B)→B)→C)) 就是公理 OR-3：(A→C)→((B→C)→(A∨B→C))。
定理 TH20: (A→¬A)→¬A
| # | wff | 理由 |
| --- | --- | --- |
| 1. | (A→A)→((A→¬A)→¬A) | TH11 |
| 2. | A→A | TH7 |
| 3. | (A→¬A)→¬A | MP 2,1. |
TH20 对应于标准 PC 的叫做“排中律”的公理 NOT-3: A∨¬A。
定理 TH21: A→(¬A→B)
| # | wff | 理由 |
| --- | --- | --- |
| 1. | A→(¬A→¬¬B) | TH2, 通过 B := ~B |
| 2. | ¬¬B→B | FRG-2 |
| 3. | A→(¬A→B) | TH14* 1,2. |
TH21 对应于标准 PC 的叫做“爆炸原理”的公理 NOT-2。
在设定 A∧B := ¬(A→¬B) 和 A∨B := (A→B)→B 之后，标准 PC 的公理已经从 Frege 的 PC 推导出来了。这些表达式不是唯一的，比如，A∨B 也可以被定义为 (B→A)→A，¬A→B 或 ¬B→A。注意，只有定义 A∨B := (A→B)→B 不包含否定。在另一方面，A∧B 不能只用蕴含而不用否定的方式定义。
在某种意义上，表达式 A∧B 和 A∨B 可以被当作"黑箱"。在这些黑箱内部包含只由蕴涵和否定构成的公式。黑箱可以包含任何东西，在加入标准 PC 的 AND-1 到 AND-3 和 OR-1 到 OR-3 公理的时候，这些公理仍然是真的。这些公理提供了合取和析取算子的完整语法定义。