弗雷格命题演算
| 此条目没有列出任何参考或来源。 (2017年1月31日) |
在数理逻辑中弗雷格命题演算是第一个公理化的命题演算。它由弗雷格发明，他还在1879年发明了谓词演算，作为他的二阶谓词逻辑的一部分(尽管查尔斯·桑德斯·皮尔士首次使用了术语“二阶”并独立于 Frege 开发了自己版本的谓词演算)。
它只使用两个逻辑算子: 蕴涵和否定，并且由六个公理和一个推理规则肯定前件构成。
公理
- THEN-1: A→(B→A)
- THEN-2: (A→(B→C))→((A→B)→(A→C))
- THEN-3: (A→(B→C))→(B→(A→C))
- FRG-1: (A→B)→(¬B→¬A)
- FRG-2: ¬¬A→A
- FRG-3: A→¬¬A
推理规则
- MP: P, P→Q ├ Q
Frege 的命题演算等价于任何其他经典的命题演算，比如有 11 个公理的“标准 PC”。Frege 的 PC 和标准的 PC 共享两个公共的公理: THEN-1 和 THEN-2。注意从 THEN-1 到 THEN-3 的公理只使用(和定义)蕴涵算子，而从 FRG-1 到 FRG-3 的公理定义否定算子。
Frege 公理证明标准公理
下列定理致力于在 Frege 的 PC 的“定理空间”内找出标准 PC 的余下九个公理，展示标准 PC 的定理被包含在 Frege 的 PC 的定理中。
(出于比喻的目的，这里所谓的理论的“定理空间”，是一个定理的集合，它是合式公式全集的子集。定理通过推理规则的直接方式相互连接起来，形成一种树状网络。)
约定 ((A→B)→B) 等同于 A∨B，¬(A→¬B) 等同于 A∧B。
规则 THEN-1*: A B→A
| # | wff | 理由 |
|---|---|---|
| 1. | A | 前提 |
| 2. | A→(B→A) | THEN-1 |
| 3. | B→A | MP 1,2. |
规则 THEN-2*: A→(B→C) (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) 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 ¬B→¬A
| # | wff | 理由 |
|---|---|---|
| 1. | (A→B)→(¬B→¬A) | FRG-1 |
| 2. | A→B | 前提 |
| 3. | ¬B→¬A | MP 2,1. |
规则 TH1*: A→B, B→C 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 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 公理的时候，这些公理仍然是真的。这些公理提供了合取和析取算子的完整语法定义。
标准公理证明 Frege 公理
下一组定理将致力于在标准 PC 的“定理空间”内找到 Frege 的 PC 的余下的四个定理，展示 Frege 的 PC 的理论包含在标准 PC 的理论内。
定理 ST1: A→A
| # | wff | 理由 |
|---|---|---|
| 1. | (A→((B→A)→A))→((A→(B→A))→(A→A)) | THEN-2 |
| 2. | A→((B→A)→A) | THEN-1 |
| 3. | (A→(B→A))→(A→A) | MP 2,1 |
| 4. | A→(B→A) | THEN-1 |
| 5. | A→A | MP 4,3. |
定理 ST2: A→¬¬A
| # | wff | 理由 |
|---|---|---|
| 1. | A | 假设 |
| 2. | A→(¬A→A) | THEN-1 |
| 3. | ¬A→A | MP 1,2 |
| 4. | ¬A→¬A | ST1 |
| 5. | (¬A→A)→((¬A→¬A)→¬¬A) | NOT-1 |
| 6. | (¬A→¬A)→¬¬A | MP 3,5 |
| 7. | ¬¬A | MP 4,6 |
| 8. | A ¬¬A | 总结 1-7 |
| 9. | A→¬¬A | DT 8. |
ST2 是 Frege 的 PC 的公理 FRG-3。
定理 ST3: B∨C→(¬C→B)
| # | wff | 理由 |
|---|---|---|
| 1. | C→(¬C→B) | NOT-2 |
| 2. | B→(¬C→B) | THEN-1 |
| 3. | (B→(¬C→B))→ ((C→(¬C→B))→((B∨C)→(¬C→B))) | OR-3 |
| 4. | (C→(¬C→B))→((B∨C)→(¬C→B)) | MP 2,3 |
| 5. | B∨C→(¬C→B) | MP 1,4. |
定理 ST4: ¬¬A→A
| # | wff | 理由 |
|---|---|---|
| 1. | A∨¬A | NOT-3 |
| 2. | (A∨¬A)→(¬¬A→A) | ST3 |
| 3. | ¬¬A→A | MP 1,2. |
ST4 是 Frege 的 PC 的公理 FRG-2。
证明 ST5: (A→(B→C))→(B→(A→C))
| # | wff | 理由 |
|---|---|---|
| 1. | A→(B→C) | 假设 |
| 2. | B | 假设 |
| 3. | A | 假设 |
| 4. | B→C | MP 3,1 |
| 5. | C | MP 2,4 |
| 6. | A→(B→C), B, A C | 总结 1-5 |
| 7. | A→(B→C), B A→C | DT 6 |
| 8. | A→(B→C) B→(A→C) | DT 7 |
| 9. | (A→(B→C))→(B→(A→C)) | DT 8. |
ST5 是 Frege 的 PC 的公理 THEN-3。
定理 ST6: (A→B)→(¬B→¬A)
| # | wff | 理由 |
|---|---|---|
| 1. | A→B | 假设 |
| 2. | ¬B | 假设 |
| 3. | ¬B→(A→¬B) | THEN-1 |
| 4. | A→¬B | MP 2,3 |
| 5. | (A→B)→((A→¬B)→¬A) | NOT-1 |
| 6. | (A→¬B)→¬A | MP 1,5 |
| 7. | ¬A | MP 4,6 |
| 8. | A→B, ¬B ¬A | 总结 1-7 |
| 9. | A→B ¬B→¬A | DT 8 |
| 10. | (A→B)→(¬B→¬A) | DT 9. |
ST6 是 Frege 的 PC 的公理 FRG-1。
每个 Frege 的公理都可以从标准的公理中推导出来，而每个标准公理都可以用 Frege 的公理推导出来。这意味着两个公理集合是相互依赖的，而没有一个集合中公理独立于另一个集合的公理。所以两个公理集合生成相同的理论: Frege 的 PC 等价于标准 PC。
(如果理论是不同的，则其中一个理论应当包含不能被另一个理论所包含的定理。这些定理可以从它们自己理论的公理集合中推导出来: 但是因为已经展示了这个完整的公理集合可以从另一个理论的公理集合中推导出来，这意味着给定的定理实际上可以从另一个理论的公理集合独立的推导出来，所以给定的定理也属于另一个理论。矛盾: 所以两个公理集合生成相同的定理空间。)
THEN-2 公理的真值表
| A | B | C | A→B | B→C | A→C | A→(B→C) | (A→B)→(A→C) |
|---|---|---|---|---|---|---|---|
| F | F | F | T | T | T | T | T |
| F | F | T | T | T | T | T | T |
| F | T | F | T | F | T | T | T |
| F | T | T | T | T | T | T | T |
| T | F | F | F | T | F | T | T |
| T | F | T | F | T | T | T | T |
| T | T | F | T | F | F | F | F |
| T | T | T | T | T | T | T | T |
参见
- 概念文字
- 《算术基本定律》由Philip A. Ebert和Marcus Rossberg引言进行翻译和编辑。牛津：牛津大学出版社，2013年。 ISBN 978-0-19-928174-9。
- 一种基于算术语言的公式语言，用于纯思想，在：J. van Heijenoort（ed。）， 从弗雷格（Frege）到哥德尔（Gödel）：《数学逻辑资料集》，1879-1931年，马萨诸塞州哈佛大学：哈佛大学出版社，1967年，第5至82页。(英语版本)
- R。L. Mendelsohn， 《戈特洛布·弗雷格（Gottlob Frege）的哲学》，剑桥：剑桥大学出版社，2005年：“附录A. Begriffsschrift的现代符号：（1）至（51）”和“附录B. Begriffsschrift的现代符号：（52）至（68）”。(英语版本）（部分内容以现代正式符号进行了修订）