弗雷格命题演算

下列定理致力于在 Frege 的 PC 的“定理空间”内找出标准 PC 的余下九个公理，展示标准 PC 的定理被包含在 Frege 的 PC 的定理中。

(出于比喻的目的，这里所谓的理论的“定理空间”，是一个定理的集合，它是合式公式全集的子集。定理通过推理规则的直接方式相互连接起来，形成一种树状网络。)

约定 ((A→B)→B) 等同于 A∨B，¬(A→¬B) 等同于 A∧B。

规则 THEN-1*: A ${\displaystyle \vdash \,}$ B→A

规则 THEN-2*: A→(B→C) ${\displaystyle \vdash \,}$ (A→B)→(A→C)

规则 THEN-3*: A→(B→C) ${\displaystyle \vdash \,}$ B→(A→C)

规则 FRG-1*: A→B ${\displaystyle \vdash \,}$ ¬B→¬A

规则 TH1*: A→B, B→C ${\displaystyle \vdash \,}$ A→C

定理 TH1: (A→B)→((B→C)→(A→C))

定理 TH2: A→(¬A→¬B)

定理 TH3: ¬A→(A→¬B)

定理 TH4: ¬(A→¬B)→A

¬(A→¬B)→A 就是公理 AND-1：A∧B→A。

定理 TH5: (A→¬B)→(B→¬A)

定理 TH6: ¬(A→¬B)→B

¬(A→¬B)→B 就是公理 AND-2：A∧B→B。

定理 TH7: A→A

定理 TH8: A→((A→B)→B)

A→((A→B)→B) 就是公理 OR-1：A→A∨B。

定理 TH9: B→((A→B)→B)

B→((A→B)→B) 就是公理 OR-2：B→A∨B。

定理 TH10: A→(B→¬(A→¬B))

A→(B→¬(A→¬B)) 就是公理 AND-3：A→(B→ A∧B) 。

定理 TH11: (A→B)→((A→¬B)→¬A)

TH11 就是标准 PC 叫做“反证法”的公理 NOT-1。

定理 TH12: ((A→B)→C)→(A→(B→C))

定理 TH13: (B→(B→C))→(B→C)

规则 TH14*: A→(B→P), P→Q ${\displaystyle \vdash \,}$ A→(B→Q)

定理 TH15: ((A→B)→(A→C))→(A→(B→C))

TH15 是公理 THEN-2 的逆命题。

定理 TH16: (¬A→¬B)→(B→A)

定理 TH17: (¬A→B)→(¬B→A)

比较定理 TH17 与定理 TH5。

定理 TH18: ((A→B)→B)→(¬A→B)

定理 TH19: (A→C)→ ((B→C)→(((A→B)→B)→C))

(A→C)→((B→C)→(((A→B)→B)→C)) 就是公理 OR-3：(A→C)→((B→C)→(A∨B→C))。

定理 TH20: (A→¬A)→¬A

TH20 对应于标准 PC 的叫做“排中律”的公理 NOT-3: A∨¬A。

定理 TH21: A→(¬A→B)

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 公理的时候，这些公理仍然是真的。这些公理提供了合取和析取算子的完整语法定义。

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

定理 ST1: A→A

定理 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)

定理 ST4: ¬¬A→A

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。

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

• 概念文字
• 《算术基本定律》由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）”。(英语版本）（部分内容以现代正式符号进行了修订）