命題論理の完全性定理
命題論理の論理式を以下のように定める．
$ \mathsf{Form} \ni \varphi ::= p \mid \lnot \varphi \mid (\varphi \to \psi)
ただし，$ p \in \mathsf{Prop}で，$ \mathsf{Prop}は命題記号と呼ばれる加算無限個の集合とする．
$ \toは右結合として常識的な範囲でカッコを省略する．
論理式$ \varphi,\psiが全く同じ論理式であることを，$ \varphi \equiv \psiと表す．
例えば$ p \to (q \to p) \equiv p \to (q \to p)である．
以下の公理図式をŁukasiewiczの3公理図式という． $ \mathbf{A_1} \coloneqq \Phi \to (\Psi \to \Phi)
$ \mathbf{A_2} \coloneqq (\Phi \to (\Psi \to \Chi)) \to ((\Phi \to \Psi) \to (\Phi \to \Chi))
$ \mathbf{A_3} \coloneqq (\lnot \Phi \to \lnot \Psi) \to (\Psi \to \Phi)
$ \Phi,\Psi,\Chiには適当な論理式を代入することで加算無限個の公理が得られる．
例えば，
$ \mathbf{A_1}_{\lbrack \Phi \mapsto \varphi, \Psi \mapsto \psi \rbrack} \equiv \varphi \to (\psi \to \varphi)
$ \mathbf{A_1}_{\lbrack \Phi \mapsto (\varphi \to \psi), \Psi \mapsto \psi \rbrack} \equiv (\varphi \to \psi) \to (\psi \to (\varphi \to \psi))
Def 3: 命題論理のHilbert流演繹体系$ \mathcal{H}_\mathbf{P}での$ \Gammaからの$ \varphiの証明 命題論理のHilbert流演繹体系$ \mathcal{H}_\mathbf{P}で論理式$ \varphiが論理式の集合$ \Gammaから証明されるとは， 各要素$ \varphi_iが次の条件のどれかを満たす論理式の列$ \varphi_0,\varphi_1,\dots,\varphi_{n}が存在することである．ただし，$ \varphi_{n} \equiv \varphiである．
1. Łukasiewiczの3公理図式$ \bf A_1,A_2,A_3から得られる公理と等しい．
2. $ \varphi_i \in \Gamma
3. $ \varphi_j \equiv \varphi_k \to \varphi_iとなるような$ \varphi_j,\varphi_kが$ j,k < iで存在する．
論理式の列$ \varphi_0,\varphi_1,\dots,\varphi_{n}を，$ \varphiの$ \Gammaでの証明と呼ぶ．
$ \mathcal{H}_\mathbf{P}で$ \Gammaから$ \varphiが証明されることを$ \Gamma \vdash_{\mathcal{H}_\mathbf{P}} \varphiと書き表す．
そしてここでは$ \mathcal{H}_\mathbf{P}しか考えないので，これを省略して$ \Gamma \vdash \varphiと省略する．
$ \Gammaが空集合$ \emptysetであるとき，$ \emptyset \vdash \varphiを更に省略して$ \vdash \varphiと表す．
このとき，$ \varphiは$ \mathcal{H}_\mathbf{P}の定理であるという．
Lem 4: 拡大
$ \Gamma \sube \Deltaとする．$ \Gamma \vdash \varphi \implies \Delta \vdash \varphi．
proof: 自明（証明の定義2より）
特に，$ \mathcal{H}_\mathbf{P}の定理はいかなる$ \Gammaからでも証明可能であることに注意．
Col 5: 便利な事実
任意の$ \varphiに対し，$ \vdash \varphi \to \varphi．
すなわち，$ \varphi \to \varphiは定理である．
proof:
$ \gamma_0 \equiv \mathbf{A_1}_{\lbrack \Phi \mapsto \varphi, \Psi \mapsto (\varphi \to \varphi) \rbrack} \equiv \varphi \to ((\varphi \to \varphi) \to \varphi)
$ \gamma_1 \equiv \mathbf{A_2}_{\lbrack \Phi \mapsto \varphi, \Psi \mapsto (\varphi \to \varphi), \Chi \mapsto (\varphi \to \varphi) \rbrack} \equiv (\varphi \to ((\varphi \to \varphi) \to \varphi)) \to ((\varphi \to (\varphi \to \varphi)) \to (\varphi \to \varphi))
$ \gamma_2 \equiv (\varphi \to (\varphi \to \varphi)) \to (\varphi \to \varphi)
このとき$ \gamma_1 \equiv \gamma_0 \to \gamma_2
$ \gamma_3 \equiv \mathbf{A_1}_{\lbrack \Phi \mapsto \varphi, \Psi \mapsto \varphi \rbrack} \equiv \varphi \to (\varphi \to \varphi)
$ \gamma_4 \equiv \varphi \to \varphi
このとき$ \gamma_2 \equiv \gamma_3 \to \gamma_4
以上より，$ \gamma_0,\dots,\gamma_4は$ \varphi \to \varphiの証明となる．
$ \Gamma \cup \{ \varphi \} \vdash \psi \iff \Gamma \vdash \varphi \to \psi
proof:
$ \implies
1. $ \Gamma \cup \{ \varphi \} \vdash \psi を仮定する．
このとき，$ \Gamma \cup \{ \varphi \}での証明$ \gamma_0,\gamma_1,\dots,\gamma_kが存在し，$ \gamma_k \equiv \psi．
2. 証明の長さの帰納法で証明する．
$ k = 0のとき，
すなわち証明が$ \gamma_0で$ \gamma_0 \equiv \psi．
このとき，$ \psiは公理か，$ \Gammaに含まれるか，$ \varphi \equiv \psiの3通りである．
1. $ \psiは公理または$ \Gammaに含まれるのどちらなら
$ \gamma_1 \equiv \mathbf{A_1}_{\lbrack \Phi \mapsto \psi, \Psi \mapsto \varphi \rbrack} \equiv \psi \to (\varphi \to \psi)とする
$ \gamma_2 \equiv \varphi \to \psiとする．
このとき，$ \gamma_1 \equiv \gamma_0 \to \gamma_2を満たす．
したがって$ \gamma_0,\gamma_1,\gamma_2は$ \Gammaの$ \varphi \to \psiの証明である．
2. $ \psi \equiv \varphiなら$ \varphi \to \psi \equiv \varphi \to \varphi，col 5より常に成り立つ．
$ 1 \leq kのとき
$ \gamma_k \equiv \psi
1. $ \gamma_{k}が公理または$ \Gamma \cup \{ \varphi\}に含まれるのどちらかなら$ k = 0と同様に$ \gamma_{k+1},\gamma_{k+2}を構成する．
2. $ \gamma_j \equiv \gamma_i \to \gamma_{k}とする．（$ i,j < k）
帰納法の仮定より
$ \Gamma \vdash \varphi \to \gamma_iの証明$ \gamma_0,\dots,\gamma_mが存在する．$ \gamma_m \equiv \varphi \to \gamma_i
$ \Gamma \vdash \varphi \to \gamma_jの証明$ \gamma_{m+1},\dots,\gamma_nが存在する．$ \gamma_n \equiv \varphi \to \gamma_j
$ \gamma_0,\dots,\gamma_{m},\gamma_{m+1},\dots,\gamma_nは$ \varphi \to \gamma_jの証明になる．$ \gamma_n \equiv \varphi \to \gamma_j \equiv \varphi \to (\gamma_i \to \gamma_k)
$ \gamma_{n+1} \equiv \mathbf{A_2}_{\lbrack \Phi \mapsto \varphi, \Psi \mapsto \gamma_i, \Chi \mapsto \gamma_k \rbrack} \equiv (\varphi \to (\gamma_i \to \gamma_k)) \to ((\varphi \to \gamma_i) \to (\varphi \to \gamma_k))
$ \gamma_{n+2} \equiv (\varphi \to \gamma_i) \to (\varphi \to \gamma_k)
$ \gamma_{n+1} \equiv \gamma_{n} \to \gamma_{n+2}
$ \gamma_{n+3} \equiv \varphi \to \gamma_k
$ \gamma_{n+2} \equiv \gamma_m \to \gamma_{n+1}
したがって$ \gamma_0,\dots,\gamma_m,\gamma_{m+1},\dots,\gamma_{n},\gamma_{n+1},\gamma_{n+2},\gamma_{n+3}は$ \varphi \to \psiの証明である．❏ $ \impliedby
1. $ \Gamma \vdash \varphi \to \psi を仮定する．
このとき，$ \Gammaでの証明$ \gamma_0,\gamma_2,\dots,\gamma_nが存在し，$ \gamma_n \equiv \varphi \to \psi．
2. $ \gamma_{n+1} \equiv \varphiとすると$ \gamma_{n+1} \in \Gamma \cup \{\varphi \}
3. $ \gamma_{n+2} \equiv \psiとする．
4. $ \gamma_{n} \equiv \gamma_{n+1} \to \gamma_{n+2}となり，$ n,n+1 < n+2
5. 以上より，$ \Gamma \cup \{\varphi\}での証明$ \gamma_0,\dots,\gamma_n,\gamma_{n+1},\gamma_{n+2}が存在するので，$ \Gamma \cup \{ \varphi \} \vdash \psi．❏ Thm 7: 二重否定
$ \Gamma \vdash \varphi \iff \Gamma \vdash \lnot\lnot\varphi
Col 8: 二重否定に関する取り扱い
$ \Gamma \cup \{\varphi\} \vdash \psi \iff \Gamma \cup \{\lnot\lnot\varphi\} \vdash \psi
Def 9: 矛盾
$ \varphi \in \Gammaかつ$ \lnot \varphi \in \Gammaであるような$ \varphiが存在するとき，$ \Gammaは矛盾しているという．
そうでないとき，$ \Gammaは無矛盾であるという．
Col 10
$ \Gammaが矛盾している$ \iff$ \Gamma \vdash \varphiかつ$ \Gamma \vdash \lnot \varphiな$ \varphiが存在する．
proof:
$ \implies
演繹定理より，適当な論理式$ \varphiと論理式の集合$ \Delta_1,\Delta_2に対し，$ \Gamma = \Delta_1 \cup \{\varphi\}かつ$ \Gamma = \Delta_2 \cup \{\lnot\varphi\}．
よって．$ \Gamma = \Delta_1 \cup \Delta_2 \cup \{\varphi,\lnot\varphi\}．
ここから$ \Delta_1 \cup \Delta_2 \cup \{\varphi,\lnot\varphi\} \vdash \varphiかつ$ \Delta_1 \cup \Delta_2 \cup \{\varphi,\lnot\varphi\} \vdash \lnot\varphi
$ \impliedby
$ \Gammaが矛盾しているなら，任意の論理式$ \varphiに対し$ \Gamma \vdash \varphi．
proof
1. 何らかの$ \psiに対し，$ \Gamma \coloneqq \Delta \cup \{\psi,\lnot\psi\}とする．
2. $ \Delta \cup \{\psi,\lnot\psi\} \vdash \varphiを証明する．
3. 演繹定理より，$ \Delta \vdash \lnot \psi \to (\psi \to \varphi)を証明すればよい．
$ \Delta \vdash \mathbf{A_1}_{\lbrack \Phi \mapsto \lnot\psi, \Psi \mapsto \lnot\varphi \rbrack}．
$ \mathbf{A_1}_{\lbrack \Phi \mapsto \lnot\psi, \Psi \mapsto \lnot\varphi \rbrack} \equiv \lnot\psi \to (\lnot\varphi \to \lnot \psi)
$ \Delta \vdash \mathbf{A_3}_{\lbrack \Phi \mapsto \phi, \Psi \mapsto \psi \rbrack}．
$ \mathbf{A_3}_{\lbrack \Phi \mapsto \phi, \Psi \mapsto \psi \rbrack} \equiv (\lnot \varphi \to \lnot \psi) \to (\psi \to \varphi)
Lem 11
$ \Gamma \vdash \varphiかつ$ \Gamma \vdash \lnot \varphiならば，$ \Gammaは矛盾している．
対偶を取ると
$ \Gammaが無矛盾なら$ \Gamma \not\vdash \varphiまたは$ \Gamma \not\vdash \lnot\varphi
$ \varphi,\lnot\varphi少なくともどちらか一方は証明できない．
Def 12
何らかの論理式$ \varphi_0に対し，$ \bot \equiv \lnot(\varphi_0 \to \varphi_0)と定める．
Col 13
$ \not \vdash \bot
Col 13
$ \Gammaが矛盾している$ \iff$ \Gamma \vdash \bot．
proof
$ \impliesLem10より
$ \impliedby
$ \Gamma \vdash \botを仮定する．すなわち，$ \Gamma \vdash \lnot(\varphi_0 \to \varphi_0)
col4より$ \Gamma \vdash (\varphi_0 \to \varphi_0)
Lem 12
$ \Gamma \cup \{\lnot\varphi\}が矛盾する$ \iff $ \Gamma \vdash \varphi
proof: 定義を変えたので↓の証明は違う．
$ \implies
1. $ \Gamma \cup \{\varphi\} \vdash \lnot(p_0 \to p_0)を仮定する．
2. 演繹定理より$ \Gamma \vdash \lnot\varphi \to \lnot(p_0 \to p_0)
3. $ \mathbf{A_3}_{\lbrack \Phi \mapsto \varphi, \Psi \mapsto \psi \rbrack} \equiv (\lnot \varphi \to \lnot (p_0 \to p_0)) \to ((p_0 \to p_0) \to \varphi)
4. 2と3より$ ((p_0 \to p_0) \to \varphi)
5. lem4より$ \vdash (p_0 \to p_0)
6. 4と5より$ \Gamma \vdash \varphi．❏ $ \impliedby
$ \Gamma \vdash \varphiを仮定する．$ \Gamma \cup \{\lnot \varphi\} \vdash \lnot\varphiより$ \varphi,\lnot\varphiの両方が導けるので矛盾．
Lem 10
$ \Gammaが無矛盾なら，任意の論理式$ \varphiに対し，$ \Gamma \cup \{\varphi\}の$ \Gamma \cup \{\lnot \varphi\}の少なくともどちらかは無矛盾．
proof
lem:11の対偶，
$ \Gammaが無矛盾なら$ \Gamma \not\vdash \varphiまたは$ \Gamma \not\vdash \lnot\varphi
lem:12の対偶．
$ \Gamma \not\vdash \varphi$ \implies$ \Gamma \cup \{\lnot \varphi\}が無矛盾．
$ \Gamma \not\vdash \lnot\varphi$ \implies$ \Gamma \cup \{\lnot\lnot\varphi\}が無矛盾．
col:7より$ \Gamma \cup \{\varphi\}も無矛盾．
$ \vdash \varphi \iff \models \varphi
$ \Gamma \models \varphiを以下のように定める．
全ての$ \gamma_1,\dots,\gamma_n \in \Gammaに$ \mathsf{t}を割り当てる任意の付値関数$ Vについて，$ V(\varphi) = \mathsf{t}であるとき．
すなわち任意の付値$ Vに対し，
$ V(\gamma_1) = V(\gamma_2) = \cdots = V(\gamma_n) = \mathsf{t} \implies V(\varphi) = \mathsf{t}
$ \Gamma \vdash \varphi \iff \Gamma \models \varphi