自然演绎

在逻辑学中, 自然演绎是一种使用直觉主义相继式的逻辑.

1推导规则

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

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

•	蕴涵, 其中第二条规则叫做肯定前件: $$\frac{\Gamma ,A⊢B}{\Gamma ⊢A\to B}\frac{\Gamma ⊢A\to B\Gamma ⊢A}{\Gamma ⊢B}$$

•	与的规则: $$\frac{\Gamma ⊢A\Gamma ⊢B}{\Gamma ⊢A\wedge B}\frac{\Gamma ⊢A\wedge B}{\Gamma ⊢A}\frac{\Gamma ⊢A\wedge B}{\Gamma ⊢B}$$其单位元的规则: $$\frac{}{\Gamma ⊢1}$$

•	或: $$\frac{\Gamma ⊢A}{\Gamma ⊢A\vee B}\frac{\Gamma ⊢B}{\Gamma ⊢A\vee B}\frac{\Gamma ⊢A\vee B\Gamma ,A⊢C\Gamma ,B⊢C}{\Gamma ⊢C}$$其单位元的规则: $$\frac{\Gamma ⊢0}{\Gamma ⊢C}$$

2性质

在使用相同的逻辑连接词时, 自然演绎等价于相继式演算. 另外自然演绎满足切消除定理, 即切规则是可容许规则.

3相关概念

•	相继式演算, 参见自然演绎–相继式演算类比.

术语翻译

自然演绎 • 英文 natural deduction