基本介紹
- 中文名：弗雷格命題演算
- 外文名：Frege's propositional calculus
簡介,Frege 公理證明標準公理,標準公理證明 Frege 公理,THEN-2 公理的真值表,參見,
簡介
在數理邏輯中弗雷格命題演算是第一個公理化的命題演算。它由弗雷格發明，他還在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{\displaystyle \vdash \,}B→A
# | wff | 理由 |
|---|---|---|
1. | A | 前提 |
2. | A→(B→A) | THEN-1 |
3. | B→A | MP 1,2. |
規則 THEN-2*:A→(B→C){\displaystyle \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){\displaystyle \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{\displaystyle \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{\displaystyle \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{\displaystyle \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 公理的時候，這些公理仍然是真的。這些公理提供了合取和析取運算元的完整語法定義。
標準公理證明 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{\displaystyle \vdash }¬¬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{\displaystyle \vdash }C | 總結 1-5 |
7. | A→(B→C), B{\displaystyle \vdash }A→C | DT 6 |
8. | A→(B→C){\displaystyle \vdash }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{\displaystyle \vdash }¬A | 總結 1-7 |
9. | A→B{\displaystyle \vdash }¬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 |
