查看“︁弗雷格命题演算”︁的源代码

{{Unreferenced|time=2017-01-31T13:05:11+00:00}}
在[[数理逻辑]]中'''弗雷格命题演算'''是第一个[[公理化]]的[[命题演算]]。它由[[弗雷格]]发明，他还在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 &#9500; 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&or;B，¬(A→¬B) 等同于 A&and;B。

'''规则 THEN-1*:''' A <math>\vdash \,</math> B→A
{| class="wikitable" style="font-family:Arial;" 
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|1. || A ||  前提
|-
|2. || A→(B→A) ||  THEN-1
|-
|3. || B→A	|| MP 1,2.
|}


'''规则 THEN-2*:'''  A→(B→C) <math>\vdash \,</math> (A→B)→(A→C)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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) <math>\vdash \,</math> B→(A→C)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|1. || A→(B→C) || 前提
|-
|2. || (A→(B→C))→(B→(A→C)) || THEN-3
|-
|3. || B→(A→C) || MP 1,2.
|}


'''规则 FRG-1*:''' A→B <math>\vdash \,</math> ¬B→¬A
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|1. || (A→B)→(¬B→¬A) || FRG-1
|-
|2. || A→B || 前提
|-
|3. || ¬B→¬A || MP 2,1.
|}


'''规则 TH1*:''' A→B, B→C <math>\vdash \,</math> A→C
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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))
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|1. || A→(B→A) || THEN-1
|-
|2. || (B→A)→(¬A→¬B) || FRG-1
|-
|3. || A→(¬A→¬B) || TH1* 1,2.
|}


'''定理 TH3:''' ¬A→(A→¬B)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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&and;B→A。

'''定理 TH5:''' (A→¬B)→(B→¬A)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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&and;B→B。

'''定理 TH7:''' A→A
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|1. || A→¬¬A || FRG-3
|-
|2. || ¬¬A→A || FRG-2
|-
|3. || A→A || TH1* 1,2.
|}


'''定理 TH8:''' A→((A→B)→B)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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&or;B。

'''定理 TH9:''' B→((A→B)→B)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|1. || B→((A→B)→B) || THEN-1, 通过 A := B, B := A→B.
|}

B→((A→B)→B) 就是'''公理 OR-2'''：B→A&or;B。

'''定理 TH10:''' A→(B→¬(A→¬B))
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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&and;B) 。


'''定理 TH11:''' (A→B)→((A→¬B)→¬A)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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))
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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 <math>\vdash \,</math> A→(B→Q)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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))
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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))
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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))→<br>
(((¬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&or;B→C))。


'''定理 TH20:''' (A→¬A)→¬A
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|1. || (A→A)→((A→¬A)→¬A) || TH11
|-
|2. || A→A || TH7
|-
|3. || (A→¬A)→¬A || MP 2,1.
|}

TH20 对应于标准 PC 的叫做“[[排中律]]”的'''公理 NOT-3''': A&or;¬A。


'''定理 TH21:''' A→(¬A→B)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|1. || A→(¬A→¬¬B) || TH2, 通过 B := ~B
|-
|2. || ¬¬B→B || FRG-2
|-
|3. || A→(¬A→B) || TH14* 1,2.
|}

TH21 对应于标准 PC 的叫做“[[爆炸原理]]”的'''公理 NOT-2'''。

在设定 A&and;B := ¬(A→¬B) 和 A&or;B := (A→B)→B 之后，标准 PC 的公理已经从 Frege 的 PC 推导出来了。这些表达式不是唯一的，比如，A&or;B 也可以被定义为 (B→A)→A，¬A→B 或 ¬B→A。注意，只有定义 A&or;B := (A→B)→B 不包含否定。在另一方面，A&and;B 不能只用蕴含而不用否定的方式定义。

在某种意义上，表达式 A&and;B 和 A&or;B 可以被当作"黑箱"。在这些黑箱内部包含只由蕴涵和否定构成的公式。黑箱可以包含任何东西，在加入标准 PC 的 AND-1 到 AND-3 和 OR-1 到 OR-3 公理的时候，这些公理仍然是真的。这些公理提供了[[合取]]和[[析取]]算子的完整语法定义。

==标准公理证明 Frege 公理==

下一组定理将致力于在标准 PC 的“定理空间”内找到 Frege 的 PC 的余下的四个定理，展示 Frege 的 PC 的理论包含在标准 PC 的理论内。

'''定理 ST1:''' A→A
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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 <math>\vdash</math> ¬¬A 
|总结 1-7
|-
|9. || A→¬¬A || DT 8.
|}

ST2 是 Frege 的 PC 的公理 FRG-3。

'''定理 ST3:''' B&or;C→(¬C→B)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|1. || C→(¬C→B) || NOT-2
|-
|2. || B→(¬C→B) || THEN-1
|-
|3.
|(B→(¬C→B))→ ((C→(¬C→B))→((B&or;C)→(¬C→B)))
|OR-3
|-
|4. || (C→(¬C→B))→((B&or;C)→(¬C→B)) || MP 2,3
|-
|5. || B&or;C→(¬C→B) || MP 1,4.
|}


'''定理 ST4:''' ¬¬A→A
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|1. || A&or;¬A || NOT-3
|-
|2. || (A&or;¬A)→(¬¬A→A) || ST3
|-
|3. || ¬¬A→A || MP 1,2.
|}

ST4 是 Frege 的 PC 的公理 FRG-2。

'''证明 ST5:''' (A→(B→C))→(B→(A→C))
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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 <math>\vdash</math> C || 总结 1-5
|-
|7. || A→(B→C), B <math>\vdash</math> A→C || DT 6
|-
|8. || A→(B→C) <math>\vdash</math> B→(A→C) || DT 7
|-
|9. || (A→(B→C))→(B→(A→C)) || DT 8.
|}

ST5 是 Frege 的 PC 的公理 THEN-3。


'''定理 ST6:''' (A→B)→(¬B→¬A)
{| class="wikitable" style="font-family:Arial;"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|理由
|-
|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 <math>\vdash</math> ¬A || 总结 1-7
|-
|9. || A→B <math>\vdash</math> ¬B→¬A || DT 8
|-
|10. || (A→B)→(¬B→¬A) || DT 9.
|}

ST6 是 Frege 的 PC 的公理 FRG-1。

每个 Frege 的公理都可以从标准的公理中推导出来，而每个标准公理都可以用 Frege 的公理推导出来。这意味着两个公理集合是相互依赖的，而没有一个集合中公理独立于另一个集合的公理。所以两个公理集合生成相同的理论: Frege 的 PC 等价于标准 PC。

(如果理论是不同的，则其中一个理论应当包含不能被另一个理论所包含的定理。这些定理可以从它们自己理论的公理集合中推导出来: 但是因为已经展示了这个完整的公理集合可以从另一个理论的公理集合中推导出来，这意味着给定的定理实际上可以从另一个理论的公理集合独立的推导出来，所以给定的定理也属于另一个理论。矛盾: 所以两个公理集合生成相同的定理空间。)

==THEN-2 公理的真值表==

{| class="wikitable" style="font-family:Arial;"
! A !! B !! C !! A→B !! B→C !! A→C !! A→(B→C) !! (A→B)→(A→C)
|- align=center
| F || F || F || T || T || T || T || T
|- align=center
| F || F || T || T || T || T || T || T
|- align=center
| F || T || F || T || F || T || T || T
|- align=center
| F || T || T || T || T || T || T || T
|- align=center
| T || F || F || F || T || F || T || T
|- align=center
| T || F || T || F || T || T || T || T
|- align=center
| T || T || F || T || F || F || F || F
|- align=center
| 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）”。(英语版本）（部分内容以现代正式符号进行了修订）




[[Category:逻辑史]]
[[Category:逻辑演算]]