Comp520MLCourse-5.2-HilbertSystem

推导与希尔伯特系统

一个推导系统(Deductive System)由一组称为公理(Axioms)的公式和一组推导规则(Rules of Inference)构成。

在推导系统中,一个证明(Proof)由一个公式序列构成:

\begin{matrix} (1) & S = {A_{1}, \dots, A_{n}} \end{matrix}

$A_i$ $A_{j1}, \cdots , A_{jk}$ $j_1<\cdots <j_k<i$ )根据规则推导出来的公式。

$A_n$ 定理 $S$ $A_n$ 证明 $A_n$ 可证明的 ${\vdash}A_n$ .

$\vdash A$ $A$ 可当作公理一样用于其它定理的证明。

希尔伯特系统是最早的推导系统之一。

$\mathcal{H}$ )

$\vdash(A\rightarrow(B\rightarrow A))$

$\vdash(A\rightarrow (B \rightarrow C)) \rightarrow ((A\rightarrow B) \rightarrow (A\rightarrow C))$

$\vdash(\lnot B \rightarrow \lnot A) \rightarrow (A \rightarrow B)$

$\frac{\vdash A\hspace{5em}\vdash A\rightarrow B}{\vdash B}.$

由三个公理和一个推导规则构成。

$\vdash A\rightarrow{A}$

Proof.

\begin{matrix} (2) & \begin{array}{clcc} 1. & ⊢ (A \to ((A \to A) \to A)) \to ((A \to (A \to A)) \to (A \to A)) & A 2 \\ 2. & ⊢ A \to ((A \to A) \to A) & A 1 \\ 3. & ⊢ (A \to (A \to A)) \to (A \to A) & M P, 1, 2 \\ 4. & ⊢ A \to (A \to A) & A 1 \\ 5. & ⊢ A \to A & M P, 3, 4 \end{array} \end{matrix}

$\mathcal{H}$ 系统中,也可以派生出其它规则。

如前提引入规则(Assumption and Deduction):

$\frac{U\cup\{A\}\vdash B}{U\vdash A\rightarrow B}$

下面借助前提引入规则,证明定理:

\begin{matrix} (3) & ⊢ (A \to B) \to [(B \to C) \to (A \to C)] \end{matrix}

证明：

\begin{matrix} (4) & \begin{array}{clcc} 1. & {A \to B, B \to C, A} ⊢ A & A s s u m p t i o n \\ 2. & {A \to B, B \to C, A} ⊢ A \to B & A s s u m p t i o n \\ 3. & {A \to B, B \to C, A} ⊢ B & M P, 1, 2 \\ 4. & {A \to B, B \to C, A} ⊢ B \to C & A s s u m p t i o n \\ 5. & {A \to B, B \to C, A} ⊢ C & M P, 3, 4 \\ 6. & {A \to B, B \to C} ⊢ A \to C & D e d u c t i o n, 5 \\ 7. & {A \to B} ⊢ [(B \to C) \to (A \to C)] & D e d u c t i o n, 6 \\ 8. & ⊢ (A \to B) \to [(B \to C) \to (A \to C)] & D e d u c t i o n, 7 \end{array} \end{matrix}

$\vdash[A\rightarrow (B\rightarrow C)]\rightarrow [B\rightarrow (A\rightarrow C)].$

证明:

\begin{matrix} (5) & \begin{array}{clcc} 1. & A \to (B \to C), B, A ⊢ A & A s s u m p t i o n \\ 2. & A \to (B \to C), B, A ⊢ A \to (B \to C) & A s s u m p t i o n \\ 3. & A \to (B \to C), B, A ⊢ B \to C & M P, 1, 2 \\ 4. & A \to (B \to C), B, A ⊢ B & A s s u m p t i o n \\ 5. & A \to (B \to C), B, A ⊢ C & M P, 3, 4 \\ 6. & A \to (B \to C), B ⊢ A \to C & D e d u c t i o n, 5 \\ 7. & A \to (B \to C) ⊢ B \to (A \to C) & D e d u c t i o n, 6 \\ 8. & ⊢ [A \to (B \to C)] \to [B \to (A \to C)] & D e d u c t i o n, 7 \end{array} \end{matrix}

$\vdash \lnot A\rightarrow (A\rightarrow B).$

证明:

\begin{matrix} (6) & \begin{array}{clcc} 1. & \neg A ⊢ \neg A \to (\neg B \to \neg A) & A 1 \\ 2. & \neg A ⊢ \neg A & A s s u m p t i o n \\ 3. & \neg A ⊢ \neg B \to \neg A & M P, 1, 2 \\ 4. & \neg A ⊢ (\neg B \to \neg A) \to (A \to B) & A 3 \\ 5. & \neg A ⊢ A \to B & M P, 3, 4 \\ 6. & ⊢ \neg A \to (A \to B) & D e d u c t i o n, 5 \end{array} \end{matrix}

$\frac{U\vdash \lnot B \rightarrow \lnot A}{U\vdash A\rightarrow B}$

$\vdash \lnot \lnot A\rightarrow A.$

\begin{matrix} (7) & \begin{array}{clcc} 1. & \neg \neg A ⊢ \neg \neg A \to (\neg \neg \neg \neg A \to \neg \neg A) & A 1 \\ 2. & \neg \neg A ⊢ \neg \neg A & A s s u m p t i o n \\ 3. & \neg \neg A ⊢ \neg \neg \neg \neg A \to \neg \neg A & M P, 1, 2 \\ 4. & \neg \neg A ⊢ \neg A \to \neg \neg \neg A & C o n t r a p o s i t i v e, 3 \\ 5. & \neg \neg A ⊢ \neg \neg A \to A & C o n t r a p o s i t i v e, 4 \\ 6. & \neg \neg A ⊢ A & M P, 2, 5 \\ 7. & ⊢ \neg \neg A \to A & D e d u c t i o n, 6 \end{array} \end{matrix}

$\vdash A\rightarrow \lnot \lnot A.$

证明:

\begin{matrix} (8) & \begin{array}{clc} 1. & ⊢ \neg \neg \neg A \to \neg A & P r o v e d \\ 2. & ⊢ A \to \neg \neg A & C o n t r a p o s i t i v e, 1 \end{array} \end{matrix}

$\frac{U\vdash A\rightarrow B\hspace{5em}U\vdash B\rightarrow C} {U\vdash A\rightarrow C}$

$\vdash(A\rightarrow B)\rightarrow (\lnot B\rightarrow \lnot A).$

证明:

\begin{matrix} (9) & \begin{array}{clc} 1. & A \to B ⊢ A \to B & A s s u m p t i o n \\ 2. & A \to B ⊢ \neg \neg A \to A & P r o v e d \\ 3. & A \to B ⊢ \neg \neg A \to B & T r a n s i t i v i t y, 2, 1 \\ 4. & A \to B ⊢ B \to \neg \neg B & P r o v e d \\ 5. & A \to B ⊢ \neg \neg A \to \neg \neg B & T r a n s i t i v i t y, 3, 4 \\ 6. & A \to B ⊢ \neg B \to \neg A & C o n t r a p o s i t i v e, 5 \\ 7. & ⊢ (A \to B) \to (\neg B \to \neg A) & D e d u c t i o n, 6 \end{array} \end{matrix}

$\frac{U\vdash A \rightarrow (B\rightarrow C)}{U\vdash B \rightarrow (A\rightarrow C)}$

$\vdash A\rightarrow (\lnot A\rightarrow B).$

证明:

\begin{matrix} (10) & \begin{array}{clc} 1. & ⊢ \neg A \to (A \to B) & P r o v e d \\ 2. & ⊢ A \to (\neg A \to B) & E x c h a n g e, 1 \end{array} \end{matrix}

否定之否定规则(Double Negation):

\begin{matrix} (11) & \frac{U ⊢ \neg \neg A}{U ⊢ A} \end{matrix}

反证规则(Reductio Ad Absurdum):

\begin{matrix} (12) & \frac{U ⊢ \neg A \to false}{U ⊢ A} \end{matrix}

$\vdash (A\rightarrow \lnot A)\rightarrow \lnot A.$

\begin{matrix} (13) & \begin{array}{clcc} 1. & A \to \neg A, \neg \neg A ⊢ \neg \neg A & A s s u m p t i o n \\ 2. & A \to \neg A, \neg \neg A ⊢ A & D o u b l e N e g a t i o n, 1 \\ 3. & A \to \neg A, \neg \neg A ⊢ A \to \neg A & A s s u m p t i o n \\ 4. & A \to \neg A, \neg \neg A ⊢ \neg A & M P, 2, 3 \\ 5. & A \to \neg A, \neg \neg A ⊢ A \to (\neg A \to f a l s e) & P r o v e d \\ 6. & A \to \neg A, \neg \neg A ⊢ \neg A \to f a l s e & M P, 2, 5 \\ 7. & A \to \neg A, \neg \neg A ⊢ f a l s e & M P, 4, 6 \\ 8. & A \to \neg A ⊢ \neg \neg A \to f a l s e & D e d u c t i o n, 7 \\ 9. & A \to \neg A ⊢ \neg A & R e d u c t i o a d a b s u r d u m, 8 \\ 10. & ⊢ (A \to \neg A) \to \neg A & D e d u c t i o n, 9 \end{array} \end{matrix}

希尔伯特系统的变种:

$1$

$2$

$3^\prime$

$Axiom\,3^\prime \,\,\,\vdash (\lnot B\rightarrow \lnot A)\rightarrow ((\lnot B\rightarrow A)\rightarrow B)$ .

\begin{matrix} (14) & \begin{array}{clc} 1. & \neg B \to \neg A, \neg B \to A, \neg B ⊢ \neg B & A s s u m p t i o n \\ 2. & \neg B \to \neg A, \neg B \to A, \neg B ⊢ \neg B \to A & A s s u m p t i o n \\ 3. & \neg B \to \neg A, \neg B \to A, \neg B ⊢ A & M P, 1, 2 \\ 4. & \neg B \to \neg A, \neg B \to A, \neg B ⊢ \neg B \to \neg A & A s s u m p t i o n \\ 5. & \neg B \to \neg A, \neg B \to A, \neg B ⊢ A \to B & C o n t r a p o s i t i v e, 4 \\ 6. & \neg B \to \neg A, \neg B \to A, \neg B ⊢ B & M P, 3, 5 \\ 7. & \neg B \to \neg A, \neg B \to A ⊢ \neg B \to B & D e d u c t i o n, 7 \\ 8. & \neg B \to \neg A, \neg B \to A ⊢ (\neg B \to B) \to B & P r o v e d \\ 9. & \neg B \to \neg A, \neg B \to A ⊢ B & M P, 8, 9 \\ 10. & \neg B \to \neg A ⊢ (\neg B \to A) \to B & D e d u c t i o n, 9 \\ 11. & ⊢ (\neg B \to \neg A) \to ((\neg B \to A) \to B) & D e d u c t i o n, 10 \end{array} \end{matrix}

不一定是三个公理,以下是四个公理的推导系统:

\begin{matrix} (15) & \begin{array}{lc} A x i o m 1 & ⊢ A \lor A \to A \\ A x i o m 2 & ⊢ A \to A \lor B \\ A x i o m 3 & ⊢ A \lor B \to B \lor A \\ A x i o m 4 & ⊢ (B \to C) \to (A \lor B \to A \lor C) \end{array} \end{matrix}

梅瑞狄斯定理(Meredith's Axiom):

\begin{matrix} (15) & ⊢ ({[(A \to B) \to (\neg C \to \neg D)] \to C} \to E) \to [(E \to A) \to (D \to A)] \end{matrix}