# 自然演绎

## 动机

— Gentzen, 《Untersuchungen über das logische Schließen》(Mathematische Zeitschrift 39, pp.176-210, 1935)

## 判断和命题

### 形成规则

$\frac{A\hbox{ prop} \qquad B\hbox{ prop}}{A \wedge B\hbox{ prop}}\ \wedge_F$

$\frac{J_1 \qquad J_2 \qquad \cdots \qquad J_n}{J}\ \hbox{name}$

$\frac{A\hbox{ prop} \qquad B\hbox{ prop}}{A \vee B\hbox{ prop}}\ \vee_F \qquad \frac{A\hbox{ prop} \qquad B\hbox{ prop}}{A \supset B\hbox{ prop}}\ \supset_F$

$\frac{\hbox{ }}{\top\hbox{ prop}}\ \top_F \qquad \frac{\hbox{ }}{\bot\hbox{ prop}}\ \bot_F \qquad \frac{A\hbox{ prop}}{\neg A\hbox{ prop}}\ \neg_F$

## 介入和除去规则

$\frac{A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I$

$\frac{\ }{\top\hbox{ true}}\ \top_I$

$\frac{A\hbox{ true}}{A \vee B\hbox{ true}}\ \vee_{I1} \qquad \frac{B\hbox{ true}}{A \vee B\hbox{ true}}\ \vee_{I2}$

$\frac{A \wedge B\hbox{ true}}{A\hbox{ true}}\ \wedge_{E1} \qquad \frac{A \wedge B\hbox{ true}}{B\hbox{ true}}\ \wedge_{E2}$

### 例子

$\cfrac{\cfrac{A \wedge B\hbox{ true}}{B\hbox{ true}}\ \wedge_{E2} \qquad \cfrac{A \wedge B\hbox{ true}}{A\hbox{ true}}\ \wedge_{E1}} {B \wedge A\hbox{ true}}\ \wedge_I$

## 假言推导

$\cfrac{A \wedge \left ( B \wedge C \right ) \ true}{\cfrac{B \wedge C \ true}{B \ true} \wedge E_1} \wedge E_2$

$\begin{matrix} A \wedge \left ( B \wedge C \right ) \ true \\ \vdots \\ B \ true \end{matrix}$

$\begin{matrix} D_1 \quad D_2 \cdots D_n \\ \vdots \\ J \end{matrix}$

### 推理规则

$\frac{ \begin{matrix} \frac{}{A \ true} u \\ \vdots \\ B \ true \end{matrix} }{A \supset B \ true} \supset I^u \qquad \frac{A \supset B \ true \quad A \ true}{B \ true} \supset E$

$\cfrac{\frac{{}}{A \ true} u \qquad \frac{{}}{B \ true} w}{ \cfrac{A \wedge B \ true}{ \cfrac{B \supset \left ( A \wedge B \right ) \ true}{ A \supset \left ( B \supset \left ( A \wedge B \right ) \right ) \ true } \supset I^u } \supset I^w } \wedge I$

$\frac{ A \vee B \hbox{ true} \quad \begin{matrix} \frac{}{A \ true} u \\ \vdots \\ C \ true \end{matrix} \quad \begin{matrix} \frac{}{B \ true} w \\ \vdots \\ C \ true \end{matrix} }{C \ true} \vee E^{u,w}$

$\frac{\perp true}{C \ true} \perp\!E$

$\frac{ \begin{matrix} \frac{}{A \ true} u \\ \vdots \\ P \ true \end{matrix} \quad \begin{matrix} \frac{}{A \ true} u \\ \vdots \\ \lnot P \ true \end{matrix} }{\lnot A \ true} \lnot I^u \qquad \frac{\lnot A \ true \quad A \ true}{C \ true} \lnot E$

## 一致性，完备性和规范形式

 $\cfrac { \frac {}{A \ true}u \quad \frac {}{B \ true}w } { \cfrac {A \land B \ true} {A \ true} \lor E_1 } \land I$ ⇒ $\cfrac {} {A \ true} u$

 $\cfrac {} {A \land B \ true}u$ ⇒ $\cfrac { \cfrac {\frac{}{A \land B \ true}u} {A \ true} \land E_1 \quad \cfrac {\frac{}{A \land B \ true}u} {B \ true} \land E_2 }{A \land B \ true} \land I$

## 一阶扩展

 $\frac {v \in V}{v \ term} {var-}F$ $\frac { f \in F \quad t_1 \ term \quad t_2 \ term \quad ... \ t_n \ term } { f (t_1, t_2, ..., t_n) \ term } {app-}F$

 $\frac { \phi \in P \quad t_1 \ term \quad t_2 \ term \quad ...\ t_n \ term } { \phi (t_1, t_2, ..., t_n) \ prop } {pred-}F$

 $\cfrac { \begin{matrix} \frac {}{x \ term}u \\ \vdots \\ A \ prop \\ \end{matrix} } {\forall x. \ A \ prop } \forall F^u$ $\cfrac { \begin{matrix} \frac {}{x \ term}u \\ \vdots \\ A \ prop \\ \end{matrix} } {\exists x. \ A \ prop } \exists F^u$

 $\cfrac { [a/x] A \ true } { \forall x. \ A \ true } \forall I^a$ $\cfrac { \forall x. \ A \ true} { [t/x] A \ true } \forall E$ $\cfrac { [t/x] A \ true} { \exists x. \ A \ true } \exists I$ $\cfrac { \exists x. \ A \ true \quad \begin{matrix} \frac {}{[a/x] A \ true}u \\ \vdots \\ C \ true \end{matrix} } { C \ true } \exists E^{a, u}$

## 高阶扩展

 $\cfrac { \begin{matrix} \frac {}{p \ prop}u \\ \vdots \\ A \ prop \\ \end{matrix} } {\forall p. \ A \ prop } \forall F^u$ $\cfrac { \begin{matrix} \frac {}{p \ prop}u \\ \vdots \\ A \ prop \\ \end{matrix} } {\exists p. \ A \ prop } \exists F^u$

## 证明论

 $\begin{matrix} \frac {}{J_1}u_1 \quad \frac {}{J_2}u_2 \quad \cdots \frac {}{J_n}u_n \\ \vdots \\ J \\ \end{matrix}$ ⇒ $u_1:J_1, u_2:J_2, ..., u_n:J_n \vdash J$

 $\frac {u \in V} {u \ proof} {proof-}F$ $\frac {} {u:A \ true \vdash u : A \ true} hyp$

 $\frac { \pi _1 \ proof \quad \pi _2 \ proof } {(\pi _1, \pi _2) \ proof}{pair-}F$ $\frac { \Gamma \vdash \pi _1 : A \quad \Gamma \vdash \pi _2 : B } { \Gamma \vdash (\pi _1, \pi _2) : A \land B } \land I$

 $\frac { \pi \ proof } { \mathbf{fst}\ \pi \ proof } {fst-}F$ $\frac { \Gamma \vdash \pi : A \land B } { \Gamma \vdash \mathbf{fst}\ \pi : A} \land E_1$ $\frac { \pi \ proof } { \mathbf{snd}\ \pi \ proof } {snd-}F$ $\frac { \Gamma \vdash \pi : A \land B } { \Gamma \vdash \mathbf{snd}\ \pi : B } \land E_2$

 $\frac {\pi \ proof } {\lambda u. \pi \ proof } {\lambda -}F$ $\frac { \Gamma , u:A \vdash \pi : B } { \Gamma \vdash \lambda u. \pi : A \supset B } \supset I$ $\frac { \pi _1 \ proof \quad \pi _2 \ proof } { \pi _1 \pi _2 \ proof } {app-}F$ $\frac { \Gamma \vdash \pi _1 : A \supset B \quad \Gamma \vdash \pi _2 : A } { \Gamma \vdash \pi _1 \pi _2 : B } \supset E$

## 类型论

 $\frac { \Gamma \vdash A \ type \quad \Gamma , x:A \vdash B \ type } {\Gamma \vdash (\Pi x:A). B \ type } {\Pi -}F$ $\frac { \Gamma \vdash A \ type \quad \Gamma , x:A \vdash B \ type } { \Gamma \vdash (\Sigma x:A). B \ type } {\Sigma -}F$

 $\frac { \Gamma, x:A \vdash \pi : B } { \Gamma \vdash \lambda x. \pi : (\Pi x:A). B } \Pi I$ $\frac { \Gamma \vdash \pi _1 : (\Pi x:A). B \quad \Gamma \vdash \pi _2 : A } { \Gamma \vdash \pi _1 \pi _2 : [\pi _2/x] B } \Pi E$
 $\frac { \Gamma \vdash \pi _1 : A \quad \Gamma, x:A \vdash \pi _2 : B } { \Gamma \vdash (\pi _1, \pi _2) : (\Sigma x:A). B } \Sigma I$ $\frac { \Gamma \vdash \pi : (\Sigma x:A). B } { \Gamma \vdash \mathbf{fst} \ \pi : A } \Sigma E _1$ $\frac { \Gamma \vdash \pi : (\Sigma x:A). B } { \Gamma \vdash \mathbf{snd} \ \pi : [ \mathbf{fst} \ \pi /x ] B } \Sigma E _2$

## 经典逻辑

 $\frac {} { A \lor \lnot A \ true } XM$ $\frac { \lnot \lnot A \ true } { A \ true } \lnot \lnot _C$ $\cfrac { \begin{matrix} \frac {} {\lnot A \ true }u \\ \vdots \\ P \ true \end{matrix} \quad \begin{matrix} \frac {} {\lnot A \ true }u \\ \vdots \\ \lnot P \ true \end{matrix} } { A\ true } \bot _C^u$

## 模态逻辑

 $\frac { A \ valid} { \Box A \ true } \Box I$ $\frac { \Box A \ true } { A \ true } \Box E$

 $\frac { \Omega; \ \cdot \vdash \pi : A \ true } { \Omega; \ \cdot \vdash \mathbf{box} \ \pi : \Box A \ true } \Box I$ $\frac { \Omega; \ \Gamma \vdash \pi : \Box A \ true } { \Omega; \ \Gamma \vdash \mathbf{unbox} \ \pi : A \ true } \Box E$

 $\frac {} { \Omega, u: (A \ valid) ; \Gamma \vdash u : A \ true } {valid-}hyp$

## 同相继式演算比较

 $\frac { \Gamma \Rightarrow A } { \Gamma \Rightarrow A \lor B } \lor R _1$ $\frac { \Gamma \Rightarrow B } { \Gamma \Rightarrow A \lor B } \lor R _2$

 $\frac { \Gamma, u:A \Rightarrow C \quad \Gamma, v:B \Rightarrow C } { \Gamma, w: (A \lor B) \Rightarrow C } \lor L$

 $\frac { \Gamma \vdash A \lor B \quad \Gamma, u:A \vdash C \quad \Gamma, v:B \vdash C } { \Gamma \vdash C } \lor E$

 $\frac {} { \Gamma, u:A \Rightarrow A } init$

$\Rightarrow$ 关于 $\vdash$ 的可靠性

$\Rightarrow$ 关于 $\vdash$ 的完备性

相继式演算 自然演绎 $\frac { \Gamma \Rightarrow \pi _1 : A \quad \Gamma \Rightarrow \pi _2 : B } { \Gamma \Rightarrow (\pi _1, \pi _2) : A \land B } \land R$ $\frac { \Gamma \vdash \pi _1 : A \quad \Gamma \vdash \pi _2 : B } { \Gamma \vdash (\pi _1, \pi _2) : A \land B } \land I$

相继式演算 自然演绎 $\frac { \Gamma, v: (A \land B), u:A \Rightarrow \pi : C } { \Gamma, v: (A \land B) \Rightarrow [ \mathbf{fst} \ v/u] \pi : C } \land L_1$ $\frac { \Gamma \vdash \pi : A \land B } { \Gamma \vdash \mathbf{fst} \ \pi : A } \land E _1$ $\frac { \Gamma, v: (A \land B), u:B \Rightarrow \pi : C } { \Gamma, v: (A \land B) \Rightarrow [\mathbf{snd} \ v/u] \pi : C } \land L _2$ $\frac { \Gamma \vdash \pi : A \land B } { \Gamma \vdash \mathbf{snd} \ \pi : B } \land E _2$

## 注释

1. ^ $\frac{A\hbox{ prop} \qquad B\hbox{ prop} \qquad A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I$ 这还可以写为: $\frac{A \wedge B\hbox{ prop} \qquad A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I$ 在这种形式中，第一个前提可以通过针对前面形式的前两个前提的 $\wedge_F$ 形成规则来满足。