子公式性质

在经典相继式演算中, 子公式性质是不使用切规则的证明满足的如下性质:$$\frac{⋮}{\Gamma ⊢\Delta }$$那么在任何 “$⋮$” 处出现的公式 (即命题的表达式) 必定是 $\Gamma ,\Delta$ 的子公式.

子公式的严格定义取决于相继式演算中具体的连接词, 但大致来说, 若将命题表达式视为用逻辑连接词作为节点构成的树, 子公式就是指这个意义下的子树.

1反例

这里给出两种经典的会破坏子公式性质的推导规则:

•	自然演绎中的部分规则, 例如肯定前件: $$\frac{\Gamma ⊢A\to B\Gamma ⊢A}{\Gamma ⊢B}$$不考虑共享的语境 $\Gamma$ 的话, 这里下边只有 $B$, 但上面凭空出现了 $A$, 破坏了子公式性质.

•	切规则: 被切掉的命题就是凭空出现的, 但是我们有切消除定理.

2意义

子公式性质可以用于证明一些在有切规则的相继式演算中不太显然的定理, 比如如下相继式不能证明:$$\varnothing ⊢\varnothing$$根据子公式性质, 可以直接知道它的证明只能是它自己 (空集的子集只能是它自己), 而这不可能.

除此之外, 子公式性质揭露了相继式演算中的推导规则是模块化的这一事实: 每个逻辑连接词的规则都只管理它的参数.

术语翻译

子公式 • 英文 subformula