半公理化逻辑

半公理化逻辑 (或半公理化相继式演算) 是将相继式演算中不可逆的规则转化为公理后得到的逻辑. 例如, 与的不可逆规则为:$$\frac{\Gamma ⊢A\Gamma ⊢B}{\Gamma ⊢A\otimes B}$$它会被转化为:$$\frac{}{\Gamma ,A,B⊢A\otimes B}$$这里其实还假设了弱化规则成立, 否则应该是 $A,B⊢A\otimes B$.

由于相继式演算的规则具有左右对称、恰好一种可逆的规律, 因此被转化为公理的推理规则也恰好只有一半, 因此得名.

1推导规则

此处假设结构性规则都成立.

•	恒同规则和切规则: $$\frac{}{\Gamma ,A⊢A}\frac{\Gamma ⊢A\Gamma ,A⊢C}{\Gamma ⊢C}$$

•	蕴涵: $$\frac{\Gamma ,A⊢B}{\Gamma ⊢A\to B}\frac{}{\Gamma ,A,A\to B⊢B}$$

•	与的规则, 极性为正: $$\frac{}{\Gamma ,A,B⊢A\wedge B}\frac{\Gamma ,A\wedge B,A,B⊢C}{\Gamma ,A\wedge B⊢C}$$其单位元的规则: $$\frac{}{\Gamma ⊢1}\frac{\Gamma ⊢C}{\Gamma ,1⊢C}$$

•	与的规则, 极性为负: (..)

•	或: $$\frac{}{\Gamma ,A⊢A\vee B}\frac{}{\Gamma ,B⊢A\vee B}\frac{\Gamma ,A\vee B,A⊢C\Gamma ,A\vee B,B⊢C}{\Gamma ,A\vee B⊢C}$$

2性质

•	半公理化逻辑具有子公式性质.

•	半公理化逻辑中切消除定理并不直接成立, 但它可以通过引入剪规则来实现之.

定义 2.1. 剪规则是一种受限的切规则, 要求被切掉的公式必须是切规则的结论部分的子公式. “剪” 这个动作可以理解为 “小幅度地切”.

3相关概念

•	Curry–Howard 对应下, 线性半公理化逻辑对应异步并发编程.

术语翻译

半公理化相继式演算 • 英文 semi-axiomatic sequent calculus (SAX)

剪规则 • 英文 snip rule