構文論的演繹定理
主張
$ A_1 \cdots A_{n-1}, A_{n} \vdash B \iff A_1 \cdots A_{n-1} \vdash A_{n} \to B
$ A, Bは論理式
証明
$ A_{1}, \cdots A_{n-1}, A_{n} \vdash Bと仮定した時，
このような$ C_1 \cdots C_{m}が存在する
任意の$ C_iについて次のいずれかが成立
2. $ j,k < iが存在する．ただし，$ C_{i}は$ C_{j}と$ C_{k}のモーダス・ポネンスで導出される 今$ C_1について
公理$ L_{k = 1,2,3}とする，次の証明より$ A_{n} \to C_{1}
1. $ C_{i} \to (A_{n} \to C_{1}): $ L_{1}
2. $ C_1 : $ L_{k}
3. $ A_{n} \to C_{1} : $ 1,2 \times \text{mp}
前提$ A_{n}とする（落とされる方の前提），次の証明より$ A_{n} \to C_{1} ($ A_{n} = C_{n})
1. $ (A_{n} \to ((A_{n} \to A_{n}) \to A_{n})) \to ((A_{n} \to (A_{n} \to A_{n})) \to (A_{n} \to A_{n})) : $ L_{2}
2. $ A_{n} \to ((A_{n} \to A_{n}) \to A_{n}) : $ L_{1}
3. $ (A_{n} \to (A_{n} \to A_{n})) \to (A_{n} \to A_{n}) : $ 1,2 \times \text{mp}
4. $ A_{n} \to (A_{n} \to A_{n}) : $ L_{1}
5. $ A_{n} \to A_{n}: $ 3,4 \times \text{mp}
前提$ A_{1 \cdots n-1}のいずれか$ A_{i}とする（落とされない方の前提），次の証明より$ A_{i} \vdash A_{n} \to C_{1}
1. $ A_{i} \to (A_{n} \to A_{i}): $ L_1
2. $ A_{i}: $ \text{Hyp}
3. $ A_{n} \to A_{i}: $ 1, 2 \times \text{mp}
上のやり方で，
$ C_1, \cdots C_{m}の番号の小さな順にモーダス・ポネンスが用いられるまで$ A_{n} \to C_{i}の証明を作る $ j,k<iで$ C_{k}は$ C_j \to C_iである
$ A_n \to C_j, A_n \to C_kの証明は既に完了している（↑）
1. $ ( A \to (C_{j} \to C_{i}) \to ((A_{a} \to C_{j}) \to (A_{a} \to C_{i})): $ L_{2}
2. $ (A \to C_{j}) \to (A_{a} \to C_{i}): $ 1, A_{n} \to (C_j \to C_i) \times \text{mp}
$ A_{n} \to C_kとはつまり$ A_n \to (C_j \to C_i)のことである
3. $ A_{a} \to C_{i}: $ 2, A_n \to C_j \times \text{mp}
これより$ C_{i}が公理，前提のいずれか，あるいはmpの帰結として証明可能である
これによって$ A_{1} \cdots A_{n-1} \vdash A_{n} \to Bの証明を作り出すことが出来る
使い方
$ p_1 \to (p_2 \to p_3), p_2 \vdash p_1 \to p_3の証明
$ \iff p_1 \to (p_2 \to p_3), p_2, p_1 \vdash p_3であるので
1. $ p_1 \to (p_2 \to p_3) : $ \text{Hyp}
2. $ p_2 : $ \text{Hyp}
3. $ p_1 : $ \text{Hyp}
4. $ p2 \to p_3, $ 1,3 \times \text{mp}
5. $ p_3 : $ 2,4 \times \text{mp}
$ \lnot p_2 \to \lnot p_1, p_1 \vdash p_2の証明
$ \iff \lnot p_2 \to \lnot p_1 \vdash p_1 \to p_2
$ \iff \vdash (\lnot p_2 \to \lnot p_1) \to (p_1 \to p_2)
これは$ L_3なので証明完了
$ \lnot p_1 \to (\lnot p_2 \to \lnot p_3), p_3 \vdash (\lnot p_1 \to \lnot p_2) \to p_1
$ \iff \lnot p_1 \to (\lnot p_2 \to \lnot p_3), \lnot p_1 \to \lnot p_2, p_3 \vdash p_1
1. $ \lnot p_1 \to (\lnot p_2 \to \lnot p_3) : $ \text{Hyp}
2. $ (\lnot p_1 \to (\lnot p_2 \to \lnot p_3)) \to ((\lnot p_1 \to \lnot p_2) \to (\lnot p_1 \to \lnot p_3)) : $ L_2
3. $ (\lnot p_1 \to \lnot p_2) \to (\lnot p_1 \to \lnot p_3) : $ 1,2 \times \text{mp}
4. $ \lnot p_1 \to \lnot p_2 : $ \text{Hyp}
5. $ \lnot p_1 \to \lnot p_3 : $ 4,5 \times \text{mp}
6. $ (\lnot p_1 \to \lnot p_3) \to (p_3 \to p_1) : $ L_3
7. $ p_3 \to p_1: $ 5,6 \times \text{mp}
8. $ p_3 : $ \text{Hyp}
9. $ p_1 : $ 7,8 \times \text{mp}