弗雷格命題演算

在數理邏輯中弗雷格命題演算是第一個公理化的命題演算。它由弗雷格發明，他還在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 $\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 公理的時候，這些公理仍然是真的。這些公理提供了合取和析取算子的完整語法定義。

標準公理證明 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 $\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 $\vdash$ C	總結 1-5
7.	A→(B→C), B $\vdash$ A→C	DT 6
8.	A→(B→C) $\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 $\vdash$ ¬A	總結 1-7
9.	A→B $\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

參見

概念文字
《算術基本定律》由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）」。(英語版本）（部分內容以現代正式符號進行了修訂）