メタ理論(古典的命題論理)
論証$ A_1 \cdots A_{n} \implies Bが正しいなら次のいづれかである
1. $ A_1 \cdots A_n \vDash B
2. $ \vDash (A_1 \land \cdots \land A_n) \implies B
このうち，
1↔2
3→4
いまから
2↔4
4→3
を示して，
1↔2↔3↔4を示しましょう
任意の論理式$ A について$ \vDash A \implies \vdash A
LPは全てのトートロジーを証明する
任意の論理式$ A について$ \vdash A \implies \vDash A
LPで証明される論理式は全てトートロジー
公理$ L_1,L_2,L_3
このような一定の公理と推論規則を持つ証明システムを公理系と総称する 公理系$ Sで論理式$ Aを証明することを$ \vdash_S Aと表現する
公理系の特性
公理系$ Sについて
$ Sが（構文論的に）矛盾$ \iff論理式$ Aについて$ \vdash_S Aかつ$ \vdash_S \lnot A
$ Sが健全$ \iff任意の論理式$ Aについて$ \vdash_{S}A \implies \vDash A
$ Sが完全$ \iff任意の論理式$ Aについて$ \vDash A \implies \vdash_{S} A
LPに関する矛盾に関する定理：
次の3つは同値
1. ある論理式$ Aが存在して，$ \vdash_{\text{LP}} Aかつ$ \vdash_{\text{LP}} \lnot A
2. 任意の論理式$ Bについて，$ \vdash_{\text{LP}}B
3. ある論理式$ Aが存在して，$ \vdash_{\text{LP}}A\land\lnot A
2 -> 3: $ B := A \land \lnot A
主張
任意の論理式$ A について$ \vdash_{\text{LP}} A \implies \vDash A
以下$ \vdash_{\text{LP}}を$ \vdashとする
証明
さらに健全性定理から無矛盾性を示すことが出来る
主張
LPで証明されない論理式が存在するので，LPは無矛盾である
証明
反例を示す
トートロジーでない$ p_1 \land \lnot p_1を考える
したがってLPから$ p_1 \land \lnot p_1は証明不可能
これによって「任意の論理式$ Bについて，$ \vdash_{\text{LP}}B」が否定された．
したがって，LPは無矛盾．
任意の論理式$ A について$ \not\vDash A \implies \not\vdash A
任意の論理式$ A について$ \vDash A \implies \vdash A
次の命題を用意
$ \Lambdaが極大
$ \iff任意の論理式$ A \in \bold{F}について$ A \in \Lambdaまたは$ \lnot A \in \Lambda
論理式$ A, Bについて次の5つの性質が成り立つ
1. $ \lnot A \in \Lambda \iff A \notin \Lambda
2. $ A \land B \in \Lambda \iff A \in \Lambda \text{かつ} B \in \Lambda
3. $ A \lor B \in \Lambda \iff A \in \Lambda \text{または} B \in \Lambda
4. $ A \to B \in \Lambda \iff A \notin \Lambda \text{または} B \in \Lambda
5. $ A \equiv B \in \Lambda \iff \left\{ A \in \Lambda \iff B \in \Lambda \right\}
例えば
$ p_1 \in \Lambdaと$ p_1 \to p_2 \in \Lambdaが成立するなら$ p_2 \in \Lambda
$ p_1 \to p_2 \in \Lambda, p_2 \to p_3 \in \Lambda \implies p_1 \to p_3 \in \Lambda
$ v_A:\bold{F} \mapsto \bold{T}
$ v_A(A) = 1 \iff A \in \Lambda
これから帰結として$ v_A(A) = 0 \iff A \notin \Lambda
任意の論理式集合$ \Gammaについて，
この定理から
そして，$ v_a(\lnot A) = 1
なぜなら$ \{\lnot A\}\subseteq \Lambda
完全性定理
任意の論理式$ Aについて$ \vDash A \implies \vdash A
1. 対偶を取る
任意の$ Aについて$ \not\vdash A \implies \not \vDash A
2. $ \not \vdash Aならば$ \not\vdash \lnot\lnot A
$ \lnot\lnot A \to A
論理式集合$ \{\lnot A\}の組み合わせとして存在する唯一の組$ \lnot Aについて，$ \not\vdash \lnot(\lnot A)
$ v_A:\bold{F} \mapsto \bold{T}
$ v_A(A) = 1 \iff A \in \Lambda
6. $ \lnot A \in \Lambdaなので，$ v_A(\lnot A) = 1
7. $ v_A(\lnot A) = 1 \iff v_A(A) = 0
8. $ v_A(A) = 0 \iff \not\vDash A