弗雷格命题演算
维基百科,自由的 encyclopedia
在数理逻辑中弗雷格命题演算是第一个公理化的命题演算。它由弗雷格发明,他还在1879年发明了谓词演算,作为他的二阶谓词逻辑的一部分(尽管查尔斯·桑德斯·皮尔士首次使用了术语“二阶”并独立于 Frege 开发了自己版本的谓词演算)。
此条目没有列出任何参考或来源。 (2017年1月31日) |
它只使用两个逻辑算子: 蕴涵和否定,并且由六个公理和一个推理规则肯定前件构成。
公理
- 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 的公理定义否定算子。