Mathematical logic (3) Natural deduction 自然演绎

1. Language 语言组成

1.1 Alphabet 符号系统

$$\Sigma = \{(,),\neg,\land,\lor,\to,\leftrightarrow,p,q,r,\dots\}$$

1.2 Formulas 公式

1. Atoms $p, q, r, s, \dots$ are formulas.
2. If $A, B$ are formulas, then $(\neg A), (A \land B), (A \lor B), (A \to B), (A \leftrightarrow B)$ are also formulas.

2. Inference Rules 推理规则

2.1 Reflectivity 自反

$$\Sigma \cup \{\alpha\} \vdash \alpha$$

2.2 Rules for More

Name	$\vdash$-notation	inference notation
$\to$-elimination ($\to_e$)	If $\Sigma \vdash_{ND}(\alpha \to \beta)$ and $\Sigma \vdash_{ND} \alpha$, then $\Sigma \vdash_{ND} \beta$	$\dfrac{(\alpha \to \beta) \text{ } \alpha}{\beta}$
$\to$-introduction ($\to_i$)	If $\Sigma, \alpha \vdash_{ND} \beta$, then $\Sigma \vdash_{ND} (\alpha \to \beta)$	$\dfrac{\boxed{\begin{aligned}&\alpha \\ &\vdots \\ &\beta\end{aligned}}}{\alpha \to \beta}$
$\land$-elimination	If $\Sigma \vdash_{ND} \alpha \land \beta$, then $\Sigma \vdash_{ND} \alpha$ (or $\Sigma \vdash_{ND} \beta$)	$\dfrac{\alpha \land \beta}{\alpha} \quad \dfrac{\alpha \land \beta}{\beta}$
$\land$-introduction	If $\Sigma \vdash_{ND} \alpha$ and $\Sigma \vdash_{ND} \beta$, then $\Sigma \vdash_{ND} (\alpha \land \beta)$	$\dfrac{\alpha \quad \beta}{\alpha \land \beta}$
$\lor$-elimination	If $\Sigma, \alpha_1 \vdash_{ND} \beta$ and $\Sigma, \alpha_2 \vdash_{ND} \beta$, then $\Sigma, (\alpha_1 \lor \alpha_2) \vdash_{ND} \beta$	$\dfrac{(\alpha_1 \lor \alpha_2) \quad \boxed{\begin{aligned}&\alpha_1 \\ &\vdots \\ &\beta\end{aligned}} \quad \boxed{\begin{aligned}&\alpha_2 \\ &\vdots \\ &\beta\end{aligned}}}{\beta}$
$\lor$-introduction	If $\Sigma \vdash_{ND} \alpha$, then $\Sigma \vdash_{ND} (\alpha \lor \beta)$ and $\Sigma \vdash_{ND} (\beta \lor \alpha)$	$\dfrac{\alpha}{(\alpha \lor \beta)} \quad \dfrac{\alpha}{(\beta \lor \alpha)}$
$\neg$-introduction	If $\Sigma, \alpha \vdash_{ND} \ \perp$, then $\Sigma \vdash_{ND} \neg \alpha$	$\dfrac{\boxed{\begin{aligned}&\alpha \\ &\vdots \\ &\perp\end{aligned}}}{\neg \alpha}$
$\perp$-elimination	If $\Sigma \vdash_{ND} \ \perp$, then $\Sigma \vdash_{ND} \alpha$	$\dfrac{\perp}{\alpha}$
$\perp$-introduction	If $\Sigma \vdash_{ND} \alpha$ and $\Sigma \vdash_{ND} \neg \alpha$, then $\Sigma \vdash_{ND} \ \perp$	$\dfrac{\alpha \quad \neg \alpha}{\perp}$
$\neg \neg$-elimination	If $\Sigma \vdash_{ND} \neg \neg \alpha$, then $\Sigma \vdash_{ND} \alpha$	$\dfrac{\neg \neg \alpha}{\alpha}$

3 Derived Rules

3.1 Modus Tollens 否定后件

$$\{(p \to q), (\neg q) \vdash_{ND}(\neg p)\} \quad \text{noted as} \quad \dfrac{(p \to q) \quad \neg q}{\neg p}$$

Proof:

$$\begin{aligned} &1. \quad (p \to q) \quad \text{Premise} \\ &2. \quad (\neg q) \quad \quad \ \ \text{Premise} \\ &\boxed{ \begin{aligned} &3. \quad p \quad \quad \quad \ \ \text{Assumption} \\ &4. \quad q \quad \quad \quad \ \to_e: 1, 3 \\ &5. \ \ \perp \quad \quad \quad \ \ \perp_i: 2, 4 \\ \end{aligned} }\\ &6. \quad \neg p \quad \quad \quad \ \neg_i: 3-6 \end{aligned}$$

3.2 Double Negation Introduction

$$\Sigma, \alpha \vdash_{ND} (\neg(\neg \alpha)) \quad \text{noted as} \quad \dfrac{\alpha}{\neg \neg \alpha}$$

Proof:

$$\begin{aligned} &1. \quad \alpha \quad \quad \quad \text{Premise} \\ &\boxed{ \begin{aligned} &2. \quad (\neg \alpha) \quad \ \text{Assumption} \\ &3. \ \ \perp \quad \quad \ \ \ \perp_i: 1, 2\\ \end{aligned} }\\ &4. (\neg(\neg \alpha)) \quad \neg_i: 2-3 \end{aligned}$$

3.3 Reductio Ad Absurbum 归谬法

$$\dfrac{\boxed{\begin{aligned}&\neg \alpha \\ &\ \ \vdots \\ &\perp\end{aligned}}}{ \alpha}$$

3.4 Tertiam Non Datur 排中律

$$\emptyset \vdash_{ND} (\alpha \lor (\neg \alpha))$$

Proof:

$$\begin{aligned} &\boxed{ \begin{aligned} &1. \quad \neg (\alpha \lor (\neg \alpha)) \quad \quad \text{Assumption} \\ &\boxed{ \begin{aligned} &2. \quad \alpha \quad \quad \quad \quad \quad \quad \ \ \text{Assumption} \\ &3. \quad (\alpha \lor \neg \alpha) \quad \quad \quad \ \lor_i: 2 \\ &4. \quad \perp \quad \quad \quad \quad \quad \quad \perp_i: 1, 3 \\ \end{aligned} }\\ &5. \quad \neg \alpha \quad \quad \quad \quad \quad \quad \neg_i: 2-4 \\ &6. \quad (\alpha \lor \neg \alpha) \quad \quad \quad \ \ \lor_i: 5 \\ &7. \quad \perp \quad \quad \quad \quad \quad \quad \ \perp_i: 1, 6 \end{aligned}}\\ &8. \quad (\alpha \lor \neg \alpha) \quad \quad \quad \ \ \ \text{Reductio ad Absurbum: 1-7} \end{aligned}$$