下面定义的命题演算通过公理的方式定义了多数逻辑算子的语法并且它只使用一个推理规则。它也叫做标准命题演算。
公理
编辑
设
ϕ
{\displaystyle \phi }
、
χ
{\displaystyle \chi }
和
ψ
{\displaystyle \psi }
表示合式公式。(wff自身将不包含任何希腊字母,而只包含大写罗马字母、连结算子和圆括号)。公理有
THEN-1:
ϕ
→
(
χ
→
ϕ
)
{\displaystyle \phi \rightarrow (\chi \rightarrow \phi )}
THEN-2:
(
ϕ
→
(
χ
→
ψ
)
)
→
(
(
ϕ
→
χ
)
→
(
ϕ
→
ψ
)
)
{\displaystyle (\phi \rightarrow (\chi \rightarrow \psi ))\rightarrow ((\phi \rightarrow \chi )\rightarrow (\phi \rightarrow \psi ))}
AND-1:
ϕ
∧
χ
→
ϕ
{\displaystyle \phi \land \chi \rightarrow \phi }
AND-2:
ϕ
∧
χ
→
χ
{\displaystyle \phi \land \chi \rightarrow \chi }
AND-3:
ϕ
→
(
χ
→
(
ϕ
∧
χ
)
)
{\displaystyle \phi \rightarrow (\chi \rightarrow (\phi \land \chi ))}
OR-1:
ϕ
→
ϕ
∨
χ
{\displaystyle \phi \rightarrow \phi \lor \chi }
OR-2:
χ
→
ϕ
∨
χ
{\displaystyle \chi \rightarrow \phi \lor \chi }
OR-3:
(
ϕ
→
ψ
)
→
(
(
χ
→
ψ
)
→
(
ϕ
∨
χ
→
ψ
)
)
{\displaystyle (\phi \rightarrow \psi )\rightarrow ((\chi \rightarrow \psi )\rightarrow (\phi \lor \chi \rightarrow \psi ))}
NOT-1:
(
ϕ
→
χ
)
→
(
(
ϕ
→
¬
χ
)
→
¬
ϕ
)
{\displaystyle (\phi \rightarrow \chi )\rightarrow ((\phi \rightarrow \neg \chi )\rightarrow \neg \phi )}
NOT-2:
ϕ
→
(
¬
ϕ
→
χ
)
{\displaystyle \phi \rightarrow (\neg \phi \rightarrow \chi )}
NOT-3:
ϕ
∨
¬
ϕ
{\displaystyle \phi \lor \neg \phi }
公理THEN-2可以被看作是“蕴涵关于蕴涵的分配律”。公理AND-1和AND-2对应于“合取除去”。在AND-1和AND-2之间的关系反映了合取算子的交换律。公理AND-3对应于“合取介入”。公理OR-1和OR-2对应于“析取介入”。在OR-1和OR-2之间的关系反映了析取算子的交换律。公理NOT-1对应于反证法。公理NOT-2说明了“从矛盾中可以推导出任何东西”。公理NOT-3叫做排中律(拉丁语tertium non datur:“排除第三者”)并反映了命题公式的语义求值:公式的真值要么是真要么是假。至少在经典逻辑中,没有第三个真值。直觉逻辑不接受公理NOT-3。
推理规则
编辑
推理规则是肯定前件:
ϕ
,
ϕ
→
χ
⊢
χ
{\displaystyle \phi ,\ \phi \rightarrow \chi \vdash \chi }
.
如果还使用双箭头的等价算子的话,则要增加如下"自然"推理规则:
IFF-1:
ϕ
↔
χ
⊢
χ
→
ϕ
{\displaystyle \phi \leftrightarrow \chi \vdash \chi \rightarrow \phi }
IFF-2:
ϕ
→
χ
,
χ
→
ϕ
⊢
ϕ
↔
χ
{\displaystyle \phi \rightarrow \chi ,\ \chi \rightarrow \phi \vdash \phi \leftrightarrow \chi }
元推理规则
编辑
设一個推導被表示为相继式,各個假设在十字转门(turnstile)的左侧,而结论在十字转门的右侧。则演绎定理可以被陈述如下:
如果相继式
ϕ
1
,
ϕ
2
,
.
.
.
,
ϕ
n
,
χ
⊢
ψ
{\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi }
已经被证明了,则也有可能证明相继式
ϕ
1
,
ϕ
2
,
.
.
.
,
ϕ
n
⊢
χ
→
ψ
{\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \rightarrow \psi }
。
这个演绎定理(DT)自身没有公式化为命题演算:它不是命题演算的定理,而是关于命题演算的一个定理。在这个意义上,它是元定理,相当于关于命题演算可靠性和完备性的定理。
在另一方面,DT对於简化语法上的证明过程是如此的有用以至于它看作和用做推理规则,同肯定前件一起使用。在这个意义上,DT对应于自然条件证明推理规则,它是在本條目中提出的第二个例子的命题演算的一部分。
DT的逆定理也是有效的:
如果相继式
ϕ
1
,
ϕ
2
,
.
.
.
,
ϕ
n
⊢
χ
→
ψ
{\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \rightarrow \psi }
已经被证明了,则也有可能证明相继式
ϕ
1
,
ϕ
2
,
.
.
.
,
ϕ
n
,
χ
⊢
ψ
{\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi }
实际上,DT的逆定理的有效性相对于DT而言是平凡的:
如果
ϕ
1
,
.
.
.
,
ϕ
n
⊢
χ
→
ψ
{\displaystyle \phi _{1},\ ...,\ \phi _{n}\vdash \chi \rightarrow \psi }
则
1:
ϕ
1
,
.
.
.
,
ϕ
n
,
χ
⊢
χ
→
ψ
{\displaystyle \phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi \rightarrow \psi }
2:
ϕ
1
,
.
.
.
,
ϕ
n
,
χ
⊢
χ
{\displaystyle \phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi }
并且可以演绎自(1)和(2)
3:
ϕ
1
,
.
.
.
,
ϕ
n
,
χ
⊢
ψ
{\displaystyle \phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \psi }
通过肯定前件的方式,Q.E.D.
DT的逆命题有着强有力的蕴涵:它可以用来把公理转换成推理规则。例如,公理AND-1
⊢
ϕ
∧
χ
→
ϕ
{\displaystyle \vdash \phi \wedge \chi \rightarrow \phi }
可以通过演绎定理的逆定理的方式被转换成推理规则
ϕ
∧
χ
⊢
ϕ
{\displaystyle \phi \wedge \chi \vdash \phi }
这是合取除去,是前面给出的自然演绎命题演算中使用的十个推理规则中的一个。
证明的例子
编辑
下面是(语法上)证明的一个例子,只涉及到公理THEN-1和THEN-2:
要证明:
A
→
A
{\displaystyle A\rightarrow A}
(蕴涵的自反性)。
证明:
1.
(
A
→
(
(
B
→
A
)
→
A
)
)
→
(
(
A
→
(
B
→
A
)
)
→
(
A
→
A
)
)
{\displaystyle (A\rightarrow ((B\rightarrow A)\rightarrow A))\rightarrow ((A\rightarrow (B\rightarrow A))\rightarrow (A\rightarrow A))}
公理THEN-2通过
ϕ
=
A
{\displaystyle \phi =A}
,
χ
=
B
→
A
{\displaystyle \chi =B\rightarrow A}
,
ψ
=
A
{\displaystyle \psi =A}
2.
A
→
(
(
B
→
A
)
→
A
)
{\displaystyle A\rightarrow ((B\rightarrow A)\rightarrow A)}
公理THEN-1通过
ϕ
=
A
{\displaystyle \phi =A}
,
χ
=
B
→
A
{\displaystyle \chi =B\rightarrow A}
3.
(
A
→
(
B
→
A
)
)
→
(
A
→
A
)
{\displaystyle (A\rightarrow (B\rightarrow A))\rightarrow (A\rightarrow A)}
得自(1)和(2)通过肯定前件。
4.
A
→
(
B
→
A
)
{\displaystyle A\rightarrow (B\rightarrow A)}
公理THEN-1通过
ϕ
=
A
{\displaystyle \phi =A}
,
χ
=
B
{\displaystyle \chi =B}
5.
A
→
A
{\displaystyle A\rightarrow A}
得自(3)和(4)通过肯定前件。