|| 証明されたものは正しくあるべき
「証明が正しい」を『定義から構築した成果』
スポンサーリンク
目次
真理値「真か偽を表現する記号」
証明可能性「出力が論理式＋正しい手順」
妥当な推論規則「論理公理と \mathrm{Modus \,\, Ponens} と全称化」
LKの推論規則「真と仮定された論理式記号と各規則」
健全性「証明できるなら正しくなければならない」
Hilbert健全性定理「論理公理＋MP」
Gentzen健全性定理「真仮定記号＋構造規則＋論理規則」
定理の前提
この定理については
\begin{array}{lcl} 公理 && 当たり前すぎて真と仮定される \\ \\ 真理値 && 真偽を記号で表現したもの \\ \\ \\ 証明可能 && 正しい手順から論理式が出力される \\ \\ 推論規則 && 前提から結論が導ける感じを記号化 \end{array}
これらの知識が必須になります。
（知らなくても感覚は分かるかも）
証明可能性
これはこの記事の主題で
\begin{array}{ccc} 証明可能 &\Longleftrightarrow& 正しい手順で論理式が出力される \end{array}
こういった感覚的に導ける定義から
\begin{array}{ccc} 証明可能 & \left\{ \begin{array}{lcc} 論理公理+\mathrm{MP}+\mathrm{UG}から得られる \\ \\ 真仮定記号+記号規則から得られる \end{array} \right. \end{array}
このように意味が変化するため
「健全性」を語る上でかなり重要な部分になります。
（健全性定理全体に要請されるものにもなる）
記号の注意点
ここ以外の記事で → は適当に使っていますが
（厳密には感覚層に近い自然言語定義はある）
\begin{array}{ccl} 他の記事での→ && 左と右の同値かを意識しない接続 \\ \\ この記事での→ && 注釈が無いなら含意に限定 \end{array}
『この記事では』厳密に取り扱うので
\begin{array}{ccc} 適当に使ってる→ && この記事では→_* \end{array}
他の記事での → と混同しないように気を付けてください。
（ \to_* は含意より抽象的で「情報の繋がり」を表現する）
健全性 Soundness
|| 証明されたものが正しくないのはおかしい
「証明されたもの」と「正しい」を繋げる感覚
\begin{array}{lcl} 健全である &\Longleftrightarrow& 証明されたやつ→_* 正しい \\ \\ 健全でない &\Longleftrightarrow& 証明されたやつ →_* おかしい \end{array}
こういう感じの意味を持っています。
（感覚的に安定していて正常な感じ）
\begin{array}{ccccl} 証明可能 && 正しい \\ \\ Γ\vdash φ &⇒& Γ\vDash φ && 全てのΓ,φで真なら健全 \\ \\ Γ\vdash φ &⇒& Γ\vDash φ && 1つでも偽なら健全でない \end{array}
記号ではこのように書かれることが多いです。
（ \vdash は証明可能で \vDash はモデル内で正しい）
健全性定理 Soundness Theorem
|| 健全性を満たすような条件を整備できる
「一階述語論理」などを『整理した結果』のこと
\begin{array}{ccc} && 証明可能 && 正しい \\ \\ 健全性定理 && \vdash &⇒& \vDash \end{array}
これは定理の型としてはこんな感じですが
\begin{array}{ccc} 健全性定理 & \left\{ \begin{array}{ll} \mathrm{Hilbert} 健全性定理 \\ \\ \mathrm{Gentzen}健全性定理 \end{array} \right. \end{array}
実際には２つの狭義的意味があり
それぞれの役割は明確に異なっています。
（他の定理と異なりこれは要請から定義を導いていく）
健全性定理の実態
これは「定理」と名付けられていますが
\begin{array}{ccc} 証明への要請的定義 &\to& 実際の構成 \end{array}
その実態は『構成的定義の整備』で
\begin{array}{lcl} 感覚層定義 && 証明はこういうもの \\ \\ 言語層定義 && 自然言語により具体的操作を定義し接続 \\ \\ 形式層定義 && 許可されるべき記号操作 \end{array}
「実際に行って良い操作」を
『やれないとおかしい』という
「要請」の観点から抽出していきます。
\mathrm{Hilbert} 健全性定理
|| ヒルベルトの時点での証明を扱った健全性定理
「論理公理」と「MP＋全称化」の検証結果
\begin{array}{lcl} 発想段階 && 証明とは→_*論理公理+操作（\mathrm{MP}+\mathrm{UG}） \\ \\ 整理段階 && 材料（論理公理）と操作（\mathrm{MP}+\mathrm{UG}） \\ \\ 検証段階 && 論理公理は真？→_*操作は真保存？ \end{array}
証明の概形はこんな感じになっています。
（証明文になるのは定義の確認段階です）
論理公理は真
ここで確認されるのは
あらゆる「恒真命題」の基礎となる
\begin{array}{ccc} 基礎論理公理 & \left\{ \begin{array}{l} 命題論理公理 \\ \\ 述語論理公理 \\ \\ 等号公理 \end{array} \right. \end{array}
『基礎論理公理』とでも呼ぶべき部分で
\begin{array}{lcl} ほぼ全ての公理 &\to_*& いくつかの公理で導ける \\ \\ &\to_*& 最低限の公理が整理される \\ \\ &\to_*& 整理された結果が基礎論理公理 \\ \\ &\to_*& 基礎で作れないなら論理公理ではない \end{array}
これらを確認することによって
間接的に全体が示されることになります。
（現時点で例外は発見されていないがあっても排除）
命題論理公理と真理値
これは大まかには３つあって
\begin{array}{ccc} 命題論理公理 &\left\{ \begin{array}{l} 後付け無意味 \\ \\ 抽象三段論法 \\ \\ 背理法の根拠 \end{array} \right. \end{array}
それぞれの真理値は
\begin{array}{ccc} p&q && p\to q \\ \\ 1 & 1 && 1 \\ \\ 1 & 0 && 0 \\ \\ 0 & 1 && 1 \\ \\ 0 & 0 && 1 \end{array}
「含意 \to 」の真理値から導かれます。
（感覚的に正しい → 真理値を確認したら確認できた）
後付けの前提は無意味になる
\begin{array}{ccc} p&q && q\to p & p\to (q\to p) \\ \\ 1 & 1 && 1 & 1 \\ \\ 1 & 0 && 1 & 1 \\ \\ 0 & 1 && 0 & 1 \\ \\ 0 & 1 && 1 & 1 \end{array}
抽象化された三段論法
\begin{array}{lcl} A&\Longleftrightarrow& p\to (q\to r) \\ \\ B &\Longleftrightarrow& (p\to q) \to ( p\to r) \\ \\ A\to B&\Longleftrightarrow& \Bigl( p\to (q\to r) \Bigr) \to \Bigl( (p\to q) \to ( p\to r) \Bigr) \end{array}
\begin{array}{ccc} p&q & r && q\to r & A && p\to q & p\to r & B && A\to B \\ \\ 1&1&1 && 1 &1&&1&1&1&& 1 \\ \\ 1&1&0 && 0&0 &&1&0 &0&&1 \\ \\ 1&0&1 && 1 &1&&0&1&1&& 1 \\ \\ 1&0&0 && 1 &1&&0&0&1&& 1 \\ \\ 0&1&1 && 1 &1&&1&1&1&& 1 \\ \\ 0&1&0 && 0 &1&&1&1&1&& 1 \\ \\ 0&0&1 && 1 &1&&1&1&1&& 1 \\ \\ 0&0&0 && 1 &1&&1&1&1&& 1 \end{array}
背理法の根拠
\begin{array}{ccc} p&q && \lnot q\to \lnot p & p\to q && (\lnot p \to \lnot q )\to (p \to q) \\ \\ 1 & 1&& 1&1 && 1 \\ \\ 1 & 0 && 0 & 0 && 1 \\ \\ 0 & 1 && 1&1 && 1 \\ \\ 0 & 0 && 1&1 &&1 \end{array}
ちょっとややこしいですが
\begin{array}{ccc} 後付け無意味 &\to_*& 真 \\ \\ 抽象三段論法 &\to_*& 真 \\ \\ 背理法の根拠 &\to_*& 真 \end{array}
これで「命題論理公理」については確認できました。
（これがHilbert健全性定理の最初の検証）
述語論理公理とモデル
ここからは「真理値の確認」ではなく
『照合』とでも呼ぶべき手順が必要になります。
\begin{array}{lcccc} 具体化 & 全てのxでφ(x)が真 &→& φ(t)は真 \\ \\ 存在宣言 & φ(t)が真 &\to& φ(x)が真のxが存在 \end{array}
やることはほぼ「言い換え」で
（根本的には代入規則の話とも言える）
\begin{array}{lcl} 感覚表現段階 && 「全→個」と「個→存在」 \\ \\ 感覚記号段階 && 予想される述語論理公理の形 \\ \\ 厳密定義段階 && モデルと割り当てで定義 \\ \\ 定義検証段階 && 定義から述語論理公理が得られる \end{array}
その手順の概形はこんな感じです。
（ただ表現を変えただけとも言える）
量化子とモデルと割り当て
「感覚記号段階」から得られる
「厳密定義段階」の「量化子」なんですが
\begin{array}{lclcl} 主観的定義 && M\vDash φ &\Longleftrightarrow & Mの解釈の元でφは真 \\ \\ モデル定義 && M\vDash φ &\Longleftrightarrow & Mをモデルとしφを真と確定 \\ \\ メタ的定義 && M\vDash φ &\Longleftrightarrow & φはMの論理的帰結である \end{array}
「量化子」はこの「モデル」における
（定義時点のモデルはまだ無矛盾を確認する段階に無い）
\begin{array}{ccl} 無矛盾 &\Longleftrightarrow& 現時点で矛盾が発見されてない \\ \\ M\vDash φ &\Longleftrightarrow& Mの基でφは真と確定される \\ \\ s(x\rightharpoonup c) &\Longleftrightarrow& 自由変数xを定数cに置き換える \\ \\ M,s\vDash φ &\Longleftrightarrow& φが変数を引数に持つ時の書き方 \\ \\ |M| &\Longleftrightarrow& 定数と関数の出力結果の集まり \end{array}
『メタレベルの数理モデルにおける定義』から
（意味は数理モデルのものに限定され真と保証される）
\begin{array}{lcl} M,s \vDash \forall x \,\, φ(x) \\ \\ M,s(x\rightharpoonup c) \vDash φ が全てのc\in |M| で成立する\\ \\ \\ M,s \vDash \exists x \,\, φ(x) \\ \\ M,s(x\rightharpoonup c) \vDash φ を満たすc\in |M|が存在する \end{array}
『自然言語との接続』という形で定義されていて
これが「健全性」の根拠になっています。
（これで定義 →_* 公理の順で検証ができる）
数理モデルとメタ記号
以上の定義に出てくる
\begin{array}{ccc} メタ記号 & \left\{ \begin{array}{c} ⇒ && 真偽不明&→_*&真保証 \\ \\ \vDash && 真保証&→_*&真確定 \\ \\ ⇔ && 対象記号 &\to_*& 定義 \end{array} \right. \end{array}
このような記号は
「メタ記号」と呼ばれるもので
\begin{array}{ccl} 感覚層 && 発想の原型となる感覚 \\ \\ 言語層 && 感覚を説明する言語が生まれる \\ \\ 形式層 && 厳密で統一的な形の言語になる \end{array}
それぞれ３層でその意味は定義されています。
（メタ記号は形式層ではただの記号として扱われる）
補足しておくと
これらの「形式層に近い言語層」の定義は
\begin{array}{ccl} A⇒B && Aが真の場合に限りBを真と保証する \\ \\ A\vDash B && Aの保証によりB は真と確定される \\ \\ A⇔B && Aという記号をBと定義する \end{array}
このようになっています。
（健全性定理などの運用段階では形式層に限定される）
また振る舞いを再現するための操作許可として
「記号定義 ⇔ 」の形式層における定義で
\begin{array}{ccc} 入力 &α変換& 出力 \\ \\ x &↦& y \end{array}
「α変換（同意味記号入れ替え）」が許容され
\begin{array}{ccc} A⇔B &\longrightarrow_*& B⇔A \end{array}
その結果として「入れ替え」が許容されます。
（これが許されないというのは実際の観察に違反する）
含意と保証メタ記号
以上のメタ記号により
\begin{array}{ccc} M,s\vDash (φ\to ψ) &\Longleftrightarrow& \Bigl( (M,s\vDash φ) ⇒( M,s\vDash ψ) \Bigr) \end{array}
「含意 \to 」はこのように定義されています。
（この場合は含意 \to が定義される対象記号になる）
補足しておくと
これは「含意 \to を定義したい」という動機から
\begin{array}{lcl} M,s\vDash φ && 確定でφが真になる \\ \\ M,s\vDash ψ && 確定でψが真になる \end{array}
材料の確認
\begin{array}{ccc} M,s \vDash (φ\to ψ) &\Longleftrightarrow& ？ \\ \\ M,s \vDash (φ\to ψ) &\Longleftrightarrow& (M,s\vDash φ)？(M,s\vDash ψ) \end{array}
予想される形を経て
\begin{array}{ccc} ？ &→& (φ→ψ) \\ \\ φ⇒ψ &→& (φ→ψ) \end{array}
「説明のためのメタ記号 ⇒ 」が発想されることで
（ φ が真なら ψ は真であると保証する）
\begin{array}{ccc} M,s\vDash (φ\to ψ) &\Longleftrightarrow& \Bigl( (M,s\vDash φ) ⇒( M,s\vDash ψ) \Bigr) \end{array}
結果的に得られるものになります。
（含意 \to を定義したいという動機から ⇒ は発想される）
述語論理公理検証のための方向性
確認しておくと
\begin{array}{lc} 具体化 && \forall x \,\, φ(x) &\to& φ(t/x) \\ \\ 存在宣言 && φ(t/x) &\to& \exists x \,\, φ(x) \end{array}
示したいのはこれが「真になる」ことで
（ t/x は t が x に代入されたことを表す記号）
\begin{array}{lcl} M,s \vDash \forall x \,\, φ(x) \\ \\ M,s(x\rightharpoonup c) \vDash φ が全てのc\in |M| で成立する\\ \\ \\ M,s \vDash \exists x \,\, φ(x) \\ \\ M,s(x\rightharpoonup c) \vDash φ を満たすc\in |M|が存在する \end{array}
それを示すための材料となる
「量化子の定義」はこんな感じになります。
（量化子の記号的振る舞いと自然言語の接続部分）
代入規則と基礎定義
ここから目的の形を求めるために
\begin{array}{ccc} M,s(x\rightharpoonup c)\vDash φ &\Longleftrightarrow& M,s\vDash φ(c/x) \end{array}
「代入規則」により許可される操作と
（真理値割り当て s のモデル上での記号操作定義）
\begin{array}{ccc} M,s \vDash \forall x \,\, φ(x) \\ \\ \Updownarrow \\ \\ M,s(x\rightharpoonup c) \vDash φ が全てのc\in |M| で成立する \\ \\ \Downarrow \\ \\ M,s(x\rightharpoonup c) \vDash φ が特定のc\in |M| で成立する \\ \\ \Updownarrow \\ \\ M,s(x\rightharpoonup c) \vDash φ \end{array}
「量化子の振る舞い」により定義される操作を
（この自然言語と記号の接続が数学の最も基礎的な定義）
\begin{array}{ccc} M,s \vDash \exists x \,\, φ(x) \\ \\ \Updownarrow \\ \\ M,s(x\rightharpoonup c) \vDash φ が成立する c\in |M| が存在する \\ \\ \Uparrow \\ \\ M,s(x\rightharpoonup c) \vDash φ という関係が c \in |M| で成立する \\ \\ \Updownarrow \\ \\ M,s(x\rightharpoonup c) \vDash φ \end{array}
それぞれ「自然言語」と「記号」に分けて定義します。
（ここで言語層と形式層を明確に分離する）
全称量化の検証
以上を踏まえると
\begin{array}{ccc} M,s(x\rightharpoonup c)\vDash φ &\Longleftrightarrow& M,s\vDash φ(c/x) \\ \\ M,s\vDash (φ\rightharpoonup ψ) &\Longleftrightarrow& \Bigl( (M,s\vDash φ) ⇒( M,s\vDash ψ) \Bigr) \end{array}
後は「代入規則」と「含意」の定義を用いれば
\begin{array}{ccc} M,s \vDash \forall x \,\, φ(x) \\ \\ \Updownarrow \\ \\ M,s(x\rightharpoonup c) \vDash φ が全てのc\in |M| で成立する \\ \\ \Downarrow \\ \\ M,s(x\rightharpoonup c) \vDash φ が特定のc\in |M| で成立する \\ \\ \Updownarrow \\ \\ M,s(x\rightharpoonup c) \vDash φ \\ \\ \Updownarrow \\ \\ M,s\vDash φ(c/x) \end{array}
「自然言語の定義と記号定義を並び替える」形で
（ ⇔ の関係にあるものは入れ替え可能）
\begin{array}{ccc} M,s \vDash \forall x \,\, φ(x) &\Longrightarrow& M,s\vDash φ(c/x) \end{array}
この形と「含意」の定義から
\begin{array}{ccc} M,s &\vDash &\forall x \,\, φ(x) &\to & φ(c/x) \end{array}
こうなるということが分かります。
（やってることは必要な記号操作の定義とその整理）
量化子と変数パターン
「定数」パターンは分かりましたが
\begin{array}{ccc} φ(t/x) & \left\{ \begin{array}{lcc} φ(c/x) && 定数パターン \\ \\ φ(y/x) && 変数パターン \end{array} \right. \end{array}
求めたい「項 t 」の形における
「変数」パターンはまだ分かっていません。
\begin{array}{ccc} M,s\Bigl( x\rightharpoonup s(y) \Bigr) \vDash φ &\Longleftrightarrow& M,s\vDash φ(y/x) \end{array}
これはこの「記号変換定義」を用いることで
（変数割り当て s は s(y)=c も意味する）
\begin{array}{ccc} M,s \vDash \forall x \,\, φ(x) \\ \\ \Updownarrow \\ \\ M,s(x\rightharpoonup s(y)) \vDash φ が全てのs(y)\in |M| で成立する \\ \\ \Downarrow \\ \\ M,s(x\rightharpoonup s(y)) \vDash φ が特定のs(y)\in |M| で成立する \\ \\ \Updownarrow \\ \\ M,s\Bigl( x\rightharpoonup s(y) \Bigr) \vDash φ \\ \\ \Updownarrow \\ \\ M,s\vDash φ(y/x) \end{array}
示すことができますが
\begin{array}{ccc} s(y)&=&c \\ \\ y&=&x \end{array}
「 α 変換である」という注釈が必要だったり
『変数割り当て s がどうなってるか』など
厳密にはきちんと考える必要があります。
変数割り当ての考察と修正
「定数出力」の関数 σ を考えて
（関数 σ(y) で y を先に定数 c にする処理）
\begin{array}{lcl} σ(x)&\Longleftrightarrow& 変数xを引数とする関数σの出力は定数 \\ \\ σ(y)&\Longleftrightarrow& 変数yを引数とする関数σの出力は定数 \end{array}
「変数割り当て s 」の振る舞いを整理すると
\begin{array}{lclcl} M,s &\to_*& M,s,σ &\overset{出力が定数記号なら}{\longrightarrow_*}& M,s \\ \\ M,s &\to_*& M,s,σ &\overset{出力が関数記号なら}{\longrightarrow_*}& M,s,σ \end{array}
これはけっこう簡潔に説明することができます。
（変数割り当てから定数出力関数 σ を分離）
\begin{array}{lcr} s(x\rightharpoonup c) &\Longleftrightarrow& 変数記号xを定数記号cに置換 \\ \\ s(x\rightharpoonup c)\vDash φ &\Longleftrightarrow& φの変数記号xを定数記号cに置換 \end{array}
というのも ↑ のように定義すれば
（変数割り当て s は分岐せず関数 σ は先処理）
\begin{array}{ccc} M,s \vDash \forall x \,\, φ(x) &\overset{sの定数部分が関数なら}{\longrightarrow_*}& M,s,σ \vDash \forall x \,\, φ(x) \end{array}
量化子定義の「定数」「変数」のパターンを
（ M,\vDash の自然言語定義は「モデル M の基で」）
\begin{array}{ll} M,s(x\rightharpoonup c) \vDash φ が&全てのc\in |M| で成立 \\ \\ M,s(x\rightharpoonup σ(y)),σ \vDash φ が & 全てのσ(y)\in |M| で成立\end{array}
『記号表現のみ』で分離できるので
（ ↑ の証明も記号を変えるだけで良い）
\begin{array}{lcl} M,s\Bigl( x\rightharpoonup s(y) \Bigr) \vDash φ &\Longleftrightarrow& M,s\vDash φ(y/x) \\ \\ M,s\Bigl( x\rightharpoonup σ(y) \Bigr),σ \vDash φ &\Longleftrightarrow& M,s,σ\vDash φ(y/x) \end{array}
従来の「曖昧な変数割り当て」より
単純かつ自然な形で量化子定義に接続できます。
（これで s の曖昧で複雑な分岐定義を排除できる）
存在量化と検証
以上の整理と同様に
\begin{array}{lcl} M,s(x\rightharpoonup c) \vDash φ &\Longleftrightarrow& M,s\vDash φ(c/x) \\ \\ M,s(x\rightharpoonup σ(y)),σ \vDash φ &\Longleftrightarrow& M,s,σ\vDash φ(y/x) \end{array}
こちらもほぼ同じ手順を用いれば
（この変形は全称量化と共通）
\begin{array}{ccc} M,s,σ \vDash \exists x \,\, φ(x) \\ \\ \Updownarrow \\ \\ M,s(x\rightharpoonup c) \vDash φ が成立する c\in |M| が存在する \\ \\ \Uparrow \\ \\ M,s(x\rightharpoonup c) \vDash φ という関係が c \in |M| で成立する \\ \\ \Updownarrow \\ \\ M,s(x\rightharpoonup c) \vDash φ \\ \\ \Updownarrow \\ \\ M,s\vDash φ(c/x) \end{array}
定数パターンの定義と
\begin{array}{ccc} M,s,σ \vDash \exists x \,\, φ(x) \\ \\ \Updownarrow \\ \\ M,s(x\rightharpoonup σ(y)),σ \vDash φ が成立する σ(y)\in |M| が存在する \\ \\ \Uparrow \\ \\ M,s(x\rightharpoonup σ(y)),σ \vDash φ という関係が σ(y) \in |M| で成立する \\ \\ \Updownarrow \\ \\ M,s(x\rightharpoonup σ(y)),σ \vDash φ \\ \\ \Updownarrow \\ \\ M,s,σ\vDash φ(y/x) \end{array}
変数パターンの定義から
\begin{array}{lcl} M,s,σ\vDash φ(c/x) &⇒& M,s,σ \vDash \exists x \,\, φ(x) \\ \\ M,s,σ\vDash φ(y/x) &⇒& M,s,σ \vDash \exists x \,\, φ(x) \end{array}
こうなることが分かるので
\begin{array}{lcl} M,s\vDash (φ\to ψ) &\Longleftrightarrow& \Bigl( (M,s\vDash φ) ⇒( M,s\vDash ψ) \Bigr) \\ \\ M,s,σ\vDash (φ\to ψ) &\Longleftrightarrow& \Bigl( (M,s,σ\vDash φ) ⇒( M,s,σ\vDash ψ) \Bigr) \end{array}
後は含意の定義を用いれば
\begin{array}{ccc} φ(t/x) &\to& \exists x \,\, φ(x) \end{array}
「存在量化」でも真になると分かることから
最終的に「述語論理公理は真」を得ることができます。
（ややこしいですが根本的にはこの着地からの逆算）
等号の公理とモデル
これもほぼ『記号の定義』です。
\begin{array}{cc} && x=x \\ \\ x=y &\to& φ(x)↔ φ(y) \\ \\ x_1=y_1∧\cdots ∧x_n=y_n &\to& R(x_1,...,x_n)=R(y_1,...,y_n) \end{array}
これらが『真になるように』定義します。
（これも量化子定義と同様に一種の記号整理）
真になるように定義する
これの具体的な実現方法は
\begin{array}{lclcl} && A=B &\Longleftrightarrow& AとBは同じである \\ \\ M & \vDash & A=B &\Longleftrightarrow& AとBは同じである \\ \\ M,s & \vDash & x=A &\Longleftrightarrow& xとAは同じである \end{array}
「モデル M 上で定義する」という
『真偽が分かるようになる操作』のことで
（モデル上での定義が無いなら真偽は不明）
\begin{array}{lcl} 感覚層 && 一致するという感覚 \\ \\ 言語層 && 同じという自然言語表現の誕生 \\ \\ 形式層 && 同じの統一表現として=を採用 \\ \\ 健全性定理 && モデル上で真偽確定の調整 \end{array}
これにより直接的に「等号公理」は証明されます。
（モデルとの対応となる記号操作の定義が証明の本質）
同一律
まず基礎的な部分から
\begin{array}{lcl} M\vDash c=c &\Longleftrightarrow& cとcは同じである \end{array}
これは最初に定義される部分で
↑ をより一般的にしたものが ↓ になります。
\begin{array}{lcl} M\vDash c=c &\Longleftrightarrow& c\in |M| は c\in |M| と同じである \\ \\ M\vDash a=b &\Longleftrightarrow& a\in |M| は b\in |M| と同じである \\ \\ M,s \vDash x=y &\Longleftrightarrow& s(x) \in |M| は s(y) \in |M| と同じである \end{array}
これにより「等号 = 」は厳密に定義され
\begin{array}{ccc} M,s & \vDash & x=y \end{array}
「真確定記号 \vDash 」により
「証明された」という結果が直接与えられます。
（これが正しくない場合「それ自身」という概念さえ使えない）
同一律と各記号の振る舞い
以上の定義と記号の振る舞いから
\begin{array}{ccc} M,s⊨f(x)=f(y) \\ \\ \Updownarrow \\ \\ f(s(x))∈|M|はf(s(y))∈|M|と同じである \end{array}
「関数」の定義と
（関数記号の自然な振る舞い）
\begin{array}{ccc} x=yはf(x)=f(y)を保証する \\ \\ \Updownarrow \\ \\ M,s\vDash x=y \,\, \Longrightarrow \,\, M,s\vDash f(x)=f(y) \end{array}
「関数」の「記号操作」
（これが違うというのは現実と不整合）
\begin{array}{ccc} M,s⊨x=y \\ \\ \Downarrow \\ \\ \displaystyle \left( \Bigl(M,s⊨φ(x)⇒M,s⊨φ(y) \Bigr) , \Bigl( M,s⊨φ(y)⇒M,s⊨φ(x) \Bigr) \right) \end{array}
そしてこの「記号入れ替えの許可」が定義されます。
（意味が変化しない記号変換を含意で分解した形）
論理式と同値記号
これは「同値記号 ↔ を定義する」という
\begin{array}{ccc} x=y &→& φ(x)↔φ(y) \end{array}
「同値関係からの逆算」から得られる公理で
（量化子同様にこれも原型となる記号が出発点）
\begin{array}{ccc} M,s⊨φ(x)↔φ(y) \\ \\ \Updownarrow \\ \\ \Bigl( M,s⊨φ(x)→φ(y) \Bigr)∧\Bigl( M,s⊨φ(y)→φ(x) \Bigr) \end{array}
この定義から得られる必然的な結果になります。
（やることは記号 ↔ の分解と最小限の定義での説明）
同値記号 ↔ の定義と公理の正当化
これは「論理積 ∧ 」の定義と
（「カンマ , 」は一貫して『記号を区切る記号』です）
\begin{array}{lcc} M,s\vDash φ∧ψ &\Longleftrightarrow& M,s\vDash φ かつ M,s\vDash ψ \\ \\ && \Updownarrow \\ \\ M,s\vDash φ,ψ &\Longleftrightarrow& M,s の基で φ と ψ の真が確定される \end{array}
「含意 \to 」の定義
\begin{array}{lcl} M,s\vDash (φ\to ψ) &\Longleftrightarrow& \Bigl( (M,s\vDash φ) ⇒( M,s\vDash ψ) \Bigr) \\ \\ M,s,σ\vDash (φ\to ψ) &\Longleftrightarrow& \Bigl( (M,s,σ\vDash φ) ⇒( M,s,σ\vDash ψ) \Bigr) \end{array}
そして「許可されるべき記号操作」から
\begin{array}{ccc} M,s⊨x=y \\ \\ \Downarrow \\ \\ \displaystyle \left( \Bigl(M,s⊨φ(x)⇒M,s⊨φ(y) \Bigr) , \Bigl( M,s⊨φ(y)⇒M,s⊨φ(x) \Bigr) \right) \\ \\ \Updownarrow \\ \\ \Bigl(M,s⊨φ(x)→φ(y) \Bigr) , \Bigl( M,s⊨φ(y)→φ(x) \Bigr) \\ \\ \Updownarrow \\ \\ \Bigl(M,s⊨φ(x)→φ(y) \Bigr) ∧ \Bigl( M,s⊨φ(y)→φ(x) \Bigr) \\ \\ \Updownarrow \\ \\ M,s⊨φ(x)↔φ(y) \end{array}
各記号操作を適用する形で
（厳密にはこうなるよう着地を分解して設計されてる）
\begin{array}{rcr} M,s⊨x=y &\Longrightarrow& M,s⊨φ(x)↔φ(y) \\ \\ M,s⊨x=y &\to& φ(x)↔φ(y) \end{array}
これは必然的に証明されます。
（量化子と同様に記号整理のチェック）
関係記号と複数引数
等号公理の３つ目である ↓ も
\begin{array}{ccc} x_1=y_1∧\cdots ∧x_n=y_n &\to& R(x_1,...,x_n)=R(y_1,...,y_n) \end{array}
感覚的な定義であるこれを分解する形で
\begin{array}{ccc} M,s\vDash x_1=y_1∧\cdots ∧x_n=y_n \\ \\ \Updownarrow \\ \\ M,s\vDash (x_1=y_1),\cdots ,(x_n=y_n) \\ \\ \Downarrow \\ \\ ？ \\ \\ \Updownarrow \\ \\ M,s\vDash R(x_1,...,x_n)=R(y_1,...,y_n) \end{array}
その正当性を定義することができます。
（間を埋めるための許可すべき定義を探る）
関数の帰納ステップ
これは関数の定義から
（より広範囲には写像の定義から）
\begin{array}{ccc} x=yはf(x)=f(y)を保証する \\ \\ \Updownarrow \\ \\ M,s\vDash x=y \,\, \Longrightarrow \,\, M,s\vDash f(x)=f(y) \end{array}
「引数を増やす」時の操作を考えると
\begin{array}{ccc} M,s⊨x_1=y_1∧x_2=y_2 \Longrightarrow M,s⊨f(x_1,x_2)=f(y_1,y_2) \\ \\ \Updownarrow \\ \\ M,s⊨x_1=y_1,x_2=y_2 \Longrightarrow M,s⊨f(x_1,x_2)=f(y_1,y_2) \\ \\ \Updownarrow \\ \\ ？ \end{array}
ちょっとややこしいですが
↑ を正当化するような
\begin{array}{lcl} M,s⊨x_1=y_1 &\Longrightarrow& M,s⊨f(x_1,c_2)=f(y_1,c_2) \\ \\ M,s⊨x_2=y_2 &\Longrightarrow& M,s⊨f(c_1,x_2)=f(c_1,y_2)\end{array}
1引数のパターンに寄せた記号操作として
（ ↑ を , で区切るのが正確な表記だが長いので縦置き）
\begin{array}{ccc} \left( \begin{array}{lcl} M,s⊨x_1=y_1 &\Longrightarrow& M,s⊨f(x_1,c_2)=f(y_1,c_2) \\ \\ M,s⊨x_2=y_2 &\Longrightarrow& M,s⊨f(c_1,x_2)=f(c_1,y_2)\end{array} \right) \\ \\ \Updownarrow \\ \\ M,s⊨x_1=y_1,x_2=y_2 \Longrightarrow M,s⊨f(x_1,x_2)=f(y_1,y_2) \end{array}
このような「許可すべき操作」が抽出できます。
（この操作により帰納的定義が可能となる）
この結果として
\begin{array}{ccc} \left( \begin{array}{lcl} M,s⊨x_1=y_1 &\Longrightarrow& M,s⊨f(x_1,...,c_n)=f(y_1,...,c_n) \\ \\ M,s⊨x_2=y_2 &\Longrightarrow& M,s⊨f(c_1,...,c_n)=f(c_1,...,c_n) \\ \\ &\vdots \\ \\ M,s⊨x_n=y_n &\Longrightarrow& M,s⊨f(c_1,...,x_n)=f(c_1,...,y_n) \end{array} \right) \\ \\ \Updownarrow \\ \\ M,s⊨x_1=y_1,...,x_n=y_n \Longrightarrow M,s⊨f(x_1,...,x_n)=f(y_1,...,y_n) \end{array}
このような一般化が可能になるため
（ k 番目から k+1 番目を作れる）
\begin{array}{ccc} M,s⊨x_1=y_1,...,x_n=y_n & \Longrightarrow & M,s⊨f(x_1,...,x_n)=f(y_1,...,y_n) \end{array}
この操作の正しさが保証されます。
（この許可が無い場合 n 引数の関数は未定義記号）
述語でも同様
「関数」で定義したように
\begin{array}{ccc} \left( \begin{array}{lcl} M,s⊨x_1=y_1 &\Longrightarrow& M,s⊨P(x_1,...,c_n)=P(y_1,...,c_n) \\ \\ M,s⊨x_2=y_2 &\Longrightarrow& M,s⊨P(c_1,...,c_n)=P(c_1,...,c_n) \\ \\ &\vdots \\ \\ M,s⊨x_n=y_n &\Longrightarrow& M,s⊨P(c_1,...,x_n)=P(c_1,...,y_n) \end{array} \right) \\ \\ \Updownarrow \\ \\ M,s⊨x_1=y_1,...,x_n=y_n \Longrightarrow M,s⊨P(x_1,...,x_n)=P(y_1,...,y_n) \end{array}
同様の手順を辿れば
（1つの引数だけ入れ替えて他は定数）
\begin{array}{ccc} M,s⊨x_1=y_1,...,x_n=y_n & \Longrightarrow & M,s⊨P(x_1,...,x_n)=P(y_1,...,y_n) \end{array}
「述語」についても定義することができます。
（これが「関係」の具体的な中身になる）
関係の複数引数での公理
以上より
「この定理での関係」は「述語」のことなので
\begin{array}{ccc} M,s⊨x_1=y_1,...,x_n=y_n & \Longrightarrow & M,s⊨R(x_1,...,x_n)=R(y_1,...,y_n) \end{array}
これが定義できたことから
（定数パターンは引数 0 とする）
\begin{array}{ccc} M,s⊨x_1=y_1,...,x_n=y_n \,\, \Longrightarrow \,\, M,s⊨R(x_1,...,x_n)=R(y_1,...,y_n) \\ \\ \Updownarrow \\ \\ M,s⊨x_1=y_1∧...∧x_n=y_n \,\, \Longrightarrow \,\, M,s⊨R(x_1,...,x_n)=R(y_1,...,y_n) \\ \\ \Updownarrow \\ \\ M,s\vDash x_1=y_1∧...∧x_n=y_n → R(x_1,...,x_n)=R(y_1,...,y_n) \end{array}
「等号の公理」は真であると言えます。
（以上でHilbert健全性定理の核は示されたと言える）
\mathrm{MP} は真保存である
これについては
\begin{array}{ccc} \left. \begin{array}{lcc} M,s\vDash φ \\ \\ M,s\vDash φ\to ψ \end{array} \right\} &\to_*& M,s\vDash ψ \end{array}
要はこういう話なんですが
\begin{array}{ccc} M,s\vDash (φ\to ψ) &\Longleftrightarrow& \Bigl( (M,s\vDash φ) ⇒( M,s\vDash ψ) \Bigr) \end{array}
これは「含意の定義」から
\begin{array}{ccl} A⇒B && Aが真の場合に限りBを真と保証する \\ \\ A\vDash B && Aの保証によりB は真と確定される \\ \\ A⇔B && Aという記号をBと定義する \end{array}
記号の意味を確認していくと
\begin{array}{ccc} M,s\vDash (φ\to ψ) &\Longleftrightarrow& \Bigl( (M,s\vDash φ) &⇒&( M,s\vDash ψ) \Bigr) \\ \\ 真確定 && 真確定 && ？ \end{array}
『真と保証される』という形で
\begin{array}{ccc} (M,s\vDash φ) ⇒( M,s\vDash ψ) は全体が真確定 \\ \\ M,s\vDash φは真確定 \\ \\ M,s\vDash φが真確定なのでM,s\vDash ψは真だと保証される \end{array}
すぐに導くことができます。
（全体が真確定なので「保証される」も真確定になる）
\mathrm{Gentzen} 健全性定理
|| LKの推論規則から見た健全性定理
「真仮定論理式記号」と「LKの推論規則」での話
\begin{array}{lcl} 発想段階 && 証明とは→_*真仮定記号+記号規則 \\ \\ 整理段階 && 材料（真仮定記号）+操作（記号規則） \\ \\ 検証段階 && 操作は真保存？ \end{array}
証明の概形はこんな感じです。
（真仮定記号なので真かどうかの確認は不要）
LKの推論規則における証明とは
これは「実際の証明」を厳密にしたもので
\begin{array}{lcl} 証明開始 && 全ての前提と結論を確認 \\ \\ 目標設定 && 規則適用により前提を結論に繋げる \\ \\ \\ 選出 && 使いたい前提を選ぶ \\ \\ 導出 && 取り出した前提に規則を適用 \\ \\ 追加 && 得られたものを前提に追加 \\ \\ 繰り返し && 結論に繋がるまで繰り返す \\ \\ \\ 最終確認 && 証明文全体を作りたい \\ \\ 記号整理 && 得られた真論理式を追加・並び替え \\ \\ 証明完成 && 証明全体が完成する \end{array}
ここではこのような手順に分解されています。
（根本的には実際に行う証明の話でこれはその中身）
記号と要請
「真と仮定されている」などの
『記号の定義』については
\begin{array}{lcl} M && Mはモデル \\ \\ \,s && sは変数割り当て \\ \\ \,, && ,は異なる記号を区切る \\ \\ \,Γ && Γは0個以上の真仮定論理式の有限列 \\ \\ \,Δ && Δは1個以上の真仮定論理式の有限列 \\ \\ \\ M,s⊨Γ &\Longleftrightarrow& M,s上でΓの各論理式は真 \\ \\ M,s⊨Δ &\Longleftrightarrow& M,s上でΔの各論理式は真 \end{array}
このような「記号への要請」という形で
（ Γ,Δ は集合としての定義も見ますが厳密には不適切）
\begin{array}{ccc} Γ\vdash Δ && Γ\vdash Δ は推件式 \end{array}
「自然言語定義」が与えられているので
（任意性での定義も見ますがそちらも厳密には不適切）
\begin{array}{ccc} 要請 && 確認 \\ \\ Mはモデルであるべき &\to& Mの性質確認 \end{array}
これに当てはまらないものは要請段階で弾かれます。
（つまり要請により記号の中身は縛りを受ける）
補足しておくと
\begin{array}{ccl} A && Aは真と仮定される論理式 \\ \\ B && Bは真と仮定される論理式 \\ \\ &\vdots \\ \\ φ && φは真と仮定される論理式 \\ \\ ψ && ψは真と仮定される論理式 \\ \\ &\vdots \end{array}
「論理式を表現する記号」については
「採用」の段階で個人の選択が必要になります。
（これらは実際に真かどうかは考慮されない）
要請的定義の解釈と許可される操作
記号定義において
\begin{array}{lcl} M && Mはモデル \\ \\ \,s && sは変数割り当て \\ \\ \,, && ,は異なる記号を区切る \\ \\ \,Γ && Γは0個以上の真仮定論理式の有限列 \\ \\ \,Δ && Δは1個以上の真仮定論理式の有限列 \\ \\ \\ M,s⊨Γ &\Longleftrightarrow& M,s上でΓの各論理式は真 \\ \\ M,s⊨Δ &\Longleftrightarrow& M,s上でΔの各論理式は真 \end{array}
このように定義されていることから分かるように
\begin{array}{lcl} Γの中の論理式ψ &\Longleftrightarrow& ψは真と仮定される論理式 \\ \\ Δの中の論理式φ &\Longleftrightarrow& φは真と仮定される論理式 \end{array}
『真仮定論理式記号 ψ,φ 』は
\begin{array}{ccc} 導出されたφ &\Longleftrightarrow& φは真仮定論理式記号 \end{array}
「いつでも使える前提」として機能します。
（結論側も前提として扱えるようになる）
推件式とメタ的意味への接続
この定理の核は
『実際の推論で観察できる』 ↓ の接続で
\begin{array}{lccc} 形式層 && Γ\vdash Δ \\ \\ && \Updownarrow \\ \\ 言語層 && 初期推件式から規則適用でΔへ至る \\ \\ && \Updownarrow \\ \\ 言語層 && 公理系Γに規則を適用してΔを導ける \\ \\ && \Downarrow \\ \\ 言語層 && (Γが真)から(Δが真)を導ける \\ \\ && \Updownarrow \\ \\ 言語層 && (Γが真確定)は(Δが真確定)を保証する \\ \\ && \Updownarrow \\ \\ 形式層 && M,s\vDash Γ \,\, \Longrightarrow \,\, M,s\vDash Δ \\ \\ && \Updownarrow \\ \\ 形式層 && Γ\vDash Δ \end{array}
この「接続の定義（自然言語の解釈部分）」により
（各記号は要請的定義により固定されている）
\begin{array}{ccc} Γ\vdash Δ &\Longrightarrow& Γ\vDash Δ \end{array}
「健全性」の確認が行われます。
（この接続が無い場合は結論 Γ\vDash Δ に繋がらない）
推件式計算と定義の接続
「推件式の計算」における上と下
（推件式の詳細についてはこの記事では語りません）
\begin{array}{ccc} 証明計算 && \displaystyle \frac{上の推件式から}{下の推件式が得られる} \end{array}
この位置についての定義は
（この記号操作はシークエント計算とも呼ばれる）
\begin{array}{ccc} 保証記号 & 上の推件式&⇒&下の推件式 \\ \\ & 記号操作前 && 記号操作後 \end{array}
こういったメタ記号によって定義することができます。
（構造規則を推件式に繋げたいという動機から得られる）
初期推件式と同一律
「初期推件式」というのは
\mathrm{Gentzen} 健全性定理の出発点になるもので
\begin{array}{ccc} 同一律 && \displaystyle \frac{}{A\vdash A} \end{array}
この「 A\vdash A 」がそれに当たります。
（ A が真ならもちろん A が真は導ける）
\begin{array}{ccc} \displaystyle \frac{根拠無し}{(A が真)から (Aが真)は証明できる} \end{array}
これを「無条件に正しい」とすることで
『証明の最小単位』が得られる感じです。
（初期推件式のみ上の推件式を必要としない）
証明の概形
「 \mathrm{Gentzen} 健全性定理」の証明は
\displaystyle \frac{}{A\vdash A}
「同一律」の推件式に対して
「弱化規則」のような記号操作を適用することや
\begin{array}{ccc} \displaystyle \frac{A\vdash A}{A,B\vdash A} && \displaystyle \frac{A\vdash A}{A\vdash A,B} \end{array}
『論理記号の定義』を用いることで
\begin{array}{ccl} \displaystyle \frac{A,B\vdash A}{A∧B\vdash A} \end{array}
着地となる「規則」の形へ持っていく作業です。
（これもHilbert健全性定理と同様に結論からの逆算）
なので型としては
\begin{array}{ccl} 同一律&\to_*&許可されるべき記号操作を適用 \\ \\ &\to_*& 論理記号定義で対応付け \end{array}
こんな感じのことをすることで健全性は証明されます。
（これにより各規則が定義により証明される）
証明計算と同一律変形許可
「構造規則の原型」を考えると
\begin{array}{lcl} 重複省略L && A\vdash A &\Longleftrightarrow& A,A \vdash A \\ \\ 重複省略R && A\vdash A &\Longleftrightarrow& A \vdash A,A \\ \\ \\ 追加L && A\vdash A &\Longrightarrow& A,B\vdash A \\ \\ 追加R && A\vdash A &\Longrightarrow& A\vdash A,B \end{array}
このような記号操作も許可されるべきで
（交換は追加の後にしか定義できない）
\begin{array}{lcl} A\vdash A ⇔ A,A \vdash A &\Longleftrightarrow& 前件のAの重複は省略可 \\ \\ A\vdash A ⇔ A \vdash A,A &\Longleftrightarrow& 後件のAの重複は省略可 \\ \\ \\ A\vdash A ⇒ A,B \vdash A &\Longleftrightarrow& 前件に真仮定記号Bを追加可 \\ \\ A\vdash A ⇒ A \vdash A,B &\Longleftrightarrow& 後件に真仮定記号Bを追加可 \end{array}
それぞれの「自然言語定義」はこのようになっています。
（これらがコンテキストと構造規則の原型になる）
補足しておくと
\begin{array}{lcl} 前件 &\Longleftrightarrow& 記号\vdash の左側 &\Longleftrightarrow& Γ\vdash ΔのΓ \\ \\ 後件 &\Longleftrightarrow& 記号\vdash の右側 &\Longleftrightarrow& Γ\vdash ΔのΔ \end{array}
「前件」「後件」の定義はこんな感じです。
（メタ記号の定義なのでこれも本質は自然言語定義）
部分操作の分離によって基礎を定義
ただ ↑ のままでは
\begin{array}{lcl} A,A,B&\vdash& A && ？ \\ \\ A,B,C&\vdash& B,A,C && ？ \end{array}
「複数の論理式の変形」に対応していないため
\begin{array}{lcl} 重複省略 && A &\Longleftrightarrow& A,A \\ \\ 追加 && A &\Longrightarrow& A,B \end{array}
厳密にはこのような形で記号操作を分離する必要があり
（これらを便宜的に部分操作と呼ぶことにする）
\begin{array}{ccc} 推件式S &\Longrightarrow& Sに部分操作を適用した推件式 \end{array}
このような宣言もまた基礎として定義する必要があります。
（双方向かどうかは部分操作の内容に依存）
追加における制限
また同一律からの定義がそうであるように
\begin{array}{ccc} 追加 && A &\Longrightarrow& A,B \end{array}
「追加できる記号」には
『推件式で扱うための制約』として
\begin{array}{ccc} Bは真仮定論理式記号 &\Longrightarrow& Bは追加可能である \end{array}
『真仮定論理式記号である』という制限が付きます。
（これがあることで「導出されたもの」も前提に追加できる）
基礎定義と入れ替え
「追加」が定義された後
\begin{array}{ccc} 追加L && A\vdash A &\Longrightarrow& A,B\vdash A \\ \\ 追加R && A\vdash A &\Longrightarrow& A\vdash A,B \end{array}
この形に定義されるのが「交換」で
\begin{array}{ccc} 交換 && A,B &\Longrightarrow& B,A \end{array}
その定義は部分操作としてこのように定義されます。
（基礎定義と同様コンテキストが無い形）
\begin{array}{ccc} A,B \Leftrightarrow B,A \\ \\ \Updownarrow \\ \\ 並び変えても証明計算上では違いが無い \end{array}
言語層の定義はこんな感じ。
（大前提として「証明である」という要請がある）
証明の基礎的概形
以上をまとめると
\begin{array}{lcl} 証明要請定義 && 証明文での記号操作を実現したい \\ \\ \\ 基礎記号定義 && 記号への要請的定義 \\ \\ 推件式定義 && Γ\vdash Δ への要請を定義 \\ \\ 証明計算定義 && 証明計算の上下を⇒で定義 \\ \\ \\ 推件式の定義分離 && 部分操作+推件式同士の関係 \\ \\ 部分操作定義 && 重複排除+追加+交換 \\ \\ 証明計算と推件式 && 操作適用前⇒操作適用後 \\ \\ \\ 基礎定義完了 && 証明計算の記号操作が明確に \end{array}
「証明計算」の記号操作は
このような形で保証されていることがわかります。
記号規則の概形
「証明計算」の概形がまとまったので
\begin{array}{c} \displaystyle \frac{L,A,B,R\vdash Δ}{L,B,A,R\vdash Δ}(\mathrm{PL}) & \displaystyle \frac{Γ\vdash L,A,B,R}{Γ\vdash L,B,A,R}(\mathrm{PR}) \\ \\ \\ \displaystyle \frac{L,A,A,R\vdash Δ}{L,A,R\vdash Δ}(\mathrm{CL}) & \displaystyle \frac{Γ\vdash L,A,A,R}{Γ\vdash L,A,R}(\mathrm{CR}) \\ \\ \\ \displaystyle \frac{L,A,R\vdash Δ}{L,A,B,R\vdash Δ}(\mathrm{WL}) & \displaystyle \frac{Γ\vdash L,A,R}{Γ\vdash L,A,B,R}(\mathrm{WR}) \end{array}
次は本丸となるこれらを整備するために
\begin{array}{rcr} Lはコンテキスト &\Longleftrightarrow& Lは0個以上の論理式の有限列 \\ \\ Rはコンテキスト &\Longleftrightarrow& Rは0個以上の論理式の有限列 \end{array}
まずは「コンテキスト」について整理してみます。
（構造規則と論理規則で一番謎な部分）
基礎定義とコンテキスト
「構造規則」という着地を目指して
↑ の「追加 \mathrm{ad} （弱化の基礎定義）」を用いると
\begin{array}{ccc} \displaystyle \frac{A,B\vdash A}{A,B,C\vdash A}(\mathrm{adL}) &&\displaystyle \frac{A,B\vdash A}{A,B\vdash A,C}(\mathrm{adR}) \end{array}
このような操作が可能になることから
\begin{array}{ccc} A,B_1,B_2,...,B_n \vdash A,C_1,C_2,...,C_n \end{array}
この「任意の真仮定論理式記号」の「追加」
という操作が許可されるので
\begin{array}{ccc} 操作しない & 操作する & 操作しない \\ \\ & A & B_1,...,B_{n} \\ \\ A,B_1 ,..., B_{k-1} & B_k & B_{k+1},..., B_n \\ \\ A,B_1 ,..., B_{n-1} & B_n \\ \\ &A& C_1,...,C_n \\ \\ A, C_1,...,C_{k-1} &C_{k} &C_{k+1},...,C_n \\ \\ A, C_1,...,C_{n-1} &C_{n} \end{array}
『操作しない真仮定論理式記号の有限列』として
（実際の運用で規則適用外の記号の処理は必要）
\begin{array}{ccc} \mathrm{Left} \,\, \mathrm{Context} & 規則適用記号 & \mathrm{Right} \,\, \mathrm{Context} \\ \\ & A & B_1,...,B_{n} \\ \\ A,B_1 ,..., B_{k-1} & B_k & B_{k+1},..., B_n \\ \\ A,B_1 ,..., B_{n-1} & B_n \\ \\ A,B_1 ,..., B_{k-1} & B_k,B_{k+1} & B_{k+2},..., B_n \end{array}
「コンテキスト」はこのように定めることができます。
（これにより加工済み証明文との対応が取れる）
またこれに加えて
\begin{array}{lcl} 規則適用前 && コンテキストはそのまま \\ \\ 規則適用記号選択 && コンテキストの再定義開始 \\ \\ 規則適用 && 操作対象の記号を変更 \\ \\ 記号整理 && 変更後記号と規則適用外記号 \\ \\ コンテキスト初期化 && コンテキスト記号の中身を空に \\ \\ コンテキスト再定義 && コンテキスト記号の再利用 \\ \\ 規則適用後 && コンテキストの中身も変わる \end{array}
『同一視の許可』により
（主な目的は変更しない部分の表記の簡略化）
\begin{array}{lcl} L,A,B,R\vdash φ && ここの中身は固定 \\ \\ L,B,A,R\vdash φ && 規則適用後は同一とは限らない \end{array}
「同一記号の使用」については
このような形で正当化されます。
（同一視許可が無い場合コンテキストの記号操作は曖昧）
コンテキストの省略
↑ の話に付け加えておくと
\begin{array}{ccc} 交換 && A,B &\Longrightarrow& B,A \end{array}
「交換 \mathrm{c} 」の部分操作により
\begin{array}{ccc} \displaystyle \frac{\displaystyle \frac{A,B,C,D,E \vdash φ }{ A,B,C,E,D \vdash φ }(\mathrm{cL})}{A,B,E,C,D \vdash φ}(\mathrm{cL}) \end{array}
「任意の記号」は『左詰め』『右詰め』が可能なので
（統合したいコンテキスト側に寄せられる）
\begin{array}{ccc} L,A,R\vdash φ &\Longrightarrow& L,A \vdash φ \end{array}
コンテキストはこのように簡略表記することが可能です。
（いずれにせよ『証明では』意味が変わらない）
コンテキストの解釈
感覚的には分かると思うんですが
\begin{array}{ccl} コンテキスト &\Longleftrightarrow& 操作対象外の記号の有限列 \\ \\ コンテキスト &\Longleftarrow& 存在はするが省略される部分 \end{array}
これは要は「実際の証明」での
『いちいち全ての前提や結論を記述しない』という
（記述しないだけで結論も前提も存在はそのまま）
\begin{array}{ccc} 使える部分だけ見る &\to& 新たな結論を得る \end{array}
「省略の感覚」を表したものに過ぎません。
（つまり『その時には見ないもの』でしかない）
「部分操作」における『追加』で
「後から補強できる」ものでしかないため
\begin{array}{lcl} 証明開始 && 全ての前提と結論を確認 \\ \\ 目標設定 && 規則適用により前提を結論に繋げる \\ \\ \\ 選出 && 使いたい前提を選ぶ \\ \\ 導出 && 取り出した前提に規則を適用 \\ \\ 追加 && 得られたものを前提に追加 \\ \\ 繰り返し && 結論に繋がるまで繰り返す \\ \\ \\ 最終確認 && 証明文全体を作りたい \\ \\ 記号整理 && 得られた真論理式を追加・並び替え \\ \\ 証明完成 && 証明全体が完成する \end{array}
この中身は『形式的な記号操作』上では
「モデル上で真である」なら無くても良いです。
（厳密には結論部分に最低１つは論理式が必要）
構造規則
「コンテキスト」が見た目ややこしいですが
「証明計算」が定義できている以上
\begin{array}{c} \displaystyle \frac{L,A,B,R\vdash Δ}{L,B,A,R\vdash Δ}(\mathrm{PL}) & \displaystyle \frac{Γ\vdash L,A,B,R}{Γ\vdash L,B,A,R}(\mathrm{PR}) \\ \\ \\ \displaystyle \frac{L,A,A,R\vdash Δ}{L,A,R\vdash Δ}(\mathrm{CL}) & \displaystyle \frac{Γ\vdash L,A,A,R}{Γ\vdash L,A,R}(\mathrm{CR}) \\ \\ \\ \displaystyle \frac{L,A,R\vdash Δ}{L,A,B,R\vdash Δ}(\mathrm{WL}) & \displaystyle \frac{Γ\vdash L,A,R}{Γ\vdash L,A,B,R}(\mathrm{WR}) \end{array}
これらは「コンテキスト」「部分操作」の定義により
直ちに『証明される』と言えます。
論理規則
これの証明は
ほぼ「自然言語定義による接続」で
\begin{array}{ccc} \mathrm{Not} && \displaystyle \frac{Γ\vdash L,A}{Γ,\lnot A \vdash L}(\mathrm{\lnot L}) & \displaystyle \frac{A,R\vdash Δ}{R\vdash Δ, \lnot A}(\mathrm{\lnot R}) \\ \\ \\ \mathrm{And} && \displaystyle \frac{A,B,R\vdash Δ}{A∧B,R\vdash Δ}(\mathrm{∧L}) & \displaystyle \frac{Γ\vdash L,A \quad Γ\vdash L,B}{Γ\vdash L,A∧B}(\mathrm{∧R}) \\ \\ \\ \mathrm{Or} && \displaystyle \frac{A,R\vdash Δ \quad B,R\vdash Δ}{A∨B,R\vdash Δ}(\mathrm{∨L}) & \displaystyle \frac{Γ\vdash L,A}{Γ\vdash L,A∨B}(\mathrm{∨R}) \\ \\ \\ \mathrm{If} && \displaystyle \frac{R\vdash L,A \quad B,R\vdash L}{A\to B,R\vdash L}(\mathrm{\to L}) & \displaystyle \frac{A,R\vdash L,B}{R\vdash L,A\to B}(\mathrm{\to R}) \end{array}
これらはただそれを表現した結果になります。
\begin{array}{ccc} \mathrm{All} && \displaystyle \frac{L,P(t)\vdash Δ}{L,\forall x\,\, P(x) \vdash Δ}(\mathrm{\forall L}) & \displaystyle \frac{Γ\vdash L,P(y)}{Γ\vdash L,\forall x \,\, P(x)}(\mathrm{\forall R}) \\ \\ \\ \mathrm{Exist} && \displaystyle \frac{L,P(y)\vdash Δ}{L,\exists x \,\, P(x) \vdash Δ}(\mathrm{\exists L}) & \displaystyle \frac{Γ\vdash L,P(t)}{Γ\vdash L,\exists x \,\, P(x)}(\mathrm{\exists R}) \end{array}
なのでこれも確認すべきは「定義」です。
（これらも定義の整理によって示される形）
論理結合子規則
『証明できる』という記述や
「操作しない部分」の記述を省略し
\begin{array}{ccc} Γ⊢Δ &\Longleftrightarrow& \left\{ \begin{array}{lcl} Γを前提として使える \\ \\ とするなら（\vdash の自然言語定義） \\ \\ Δ を結論として導ける \end{array} \right. \end{array}
『コンテキストは後で追加できる』ことを利用すると
「否定」と「含意L」はいったん置いておくなら
（他と違ってこれらの定義には注意が必要）
\begin{array}{ccc} A,B\vdash Δ \\ \\ \Updownarrow \\ \\ A,Bを前提として使える \\ \\ \Downarrow \\ \\ A,Bが両方成立するという前提が使える \\ \\ \Updownarrow \\ \\ A∧B\vdash Δ \end{array}
まず「論理積L」はこんな感じで
\begin{array}{ccc} Γ_1\vdash A \quad Γ_2\vdash B \\ \\ \Updownarrow \\ \\ AとBが結論として導かれる \\ \\ \Downarrow \\ \\ AとBが両方成立するという結論が導かれる \\ \\ \Updownarrow \\ \\ Γ_1,Γ_2\vdash A∧B \end{array}
同様に「論理積R」もこんな感じになります。
（ Γ は厳密には区別が必要で同一とは限らない）
\begin{array}{ccc} A\vdash Δ_1 \quad B\vdash Δ_2 \\ \\ \Updownarrow \\ \\ Aは前提でBも前提 \\ \\ \Downarrow \\ \\ AかBが成立するを前提として使える \\ \\ \Updownarrow \\ \\ A∨B\vdash Δ_1,Δ_2 \end{array}
また「論理和L」はこういう感じで
（厳密には追加が適用された上でこの定義が来る）
\begin{array}{ccc} Γ\vdash A \\ \\ \Updownarrow \\ \\ Aが結論として導かれる \\ \\ \Downarrow \\ \\ AかBが成立するという結論が導かれる \\ \\ \Updownarrow \\ \\ Γ\vdash A∨B \end{array}
「 A が真仮定論理式である」以上
「論理和R」もまたこんな感じになります。
（こちらも厳密には追加が適用された後に定義される）
最後、同様に定義すると
\begin{array}{ccc} A\vdash B \\ \\ \Updownarrow \\ \\ 前提Aから結論Bが導かれる \\ \\ \Downarrow \\ \\ AならばBが結論として導かれる \\ \\ \Updownarrow \\ \\ A\vdash A\to B \end{array}
「含意R」もそのままこんな感じになります。
（感覚的な話をそのまま表現してるだけ）
\begin{array}{ccc} \displaystyle \frac{A\vdash B}{A,A\to B\vdash B}(\mathrm{adL}) \end{array}
加えてこの「含意R」と「追加」により
「 \mathrm{MP} の正当性」が定理として与えられます。
（規則により A\to B は真仮定論理式記号になる）
否定と真仮定
これは記号操作と自然言語定義はシンプルなので
\begin{array}{ccc} Γ\vdash A,Δ \\ \\ \Updownarrow \\ \\ Aが結論として導かれる \\ \\ \Downarrow \\ \\ Aが導かれないならAは前提として使えない \\ \\ \Updownarrow \\ \\ Γ,\lnot A \vdash Δ \end{array}
両者とも「感覚的には明らか」なんですが
\begin{array}{ccc} Γ,A\vdash Δ \\ \\ \Updownarrow \\ \\ Aが前提として使える \\ \\ \Downarrow \\ \\ Aが前提として使えないならAは導かれない \\ \\ \Updownarrow \\ \\ Γ\vdash \lnot A,Δ \end{array}
「真仮定記号である」という点で
\begin{array}{rcr} Aは真と仮定された論理式記号である \\ \\ \lnot Aは真と仮定された論理式記号である \end{array}
少し注意が必要になります。
見てわかる通り
『モデルの中で考える』なら
\begin{array}{l} M,s\vDash A &真&偽 \\ \\ M,s\vDash \lnot A & 偽 & 真 \end{array}
『否定 \lnot を素直に扱う』場合
これらはこのようになるはず
\begin{array}{rcr} Aは真と仮定された論理式記号である \\ \\ \lnot Aは真と仮定された論理式記号である \end{array}
しかし「推件式の記号への要請」はこのようになるので
少なくとも『偽と仮定される』ことはありません。
否定と前件後件入れ替え
↑ の話で分かる通り
『否定』の「自然言語的義」については
\begin{array}{lcc} \lnot Aは真と仮定された論理式記号である \\ \\ \lnot Aは記号操作の段階では偽にならない \end{array}
『形式層での整合性』をとる必要があって
（形式段階では真仮定の要請を満たす必要がある）
\begin{array}{ccc} \lnot && 証明計算時点では真偽の入れ替えが起きない \end{array}
そのために
『否定記号 \lnot の意味』について
（形式層では『位置入れ替えの履歴』を意味する）
\begin{array}{rcr} A & \Longleftrightarrow & 真仮定 \\ \\ M,s \vDash A & \Longleftrightarrow & M,s \not\vDash \lnot A \\ \\ \\ \lnot A & \Longleftrightarrow &真仮定 \\ \\ M,s \vDash \lnot A & \Longleftrightarrow &M,s \not\vDash A \end{array}
この形を壊さないように
\begin{array}{ccccr} モデル定義前 && \lnot & \Longleftrightarrow & 前件と後件の入れ替え記号 \\ \\ モデル定義後 && \lnot & \Longleftrightarrow & 真偽の入れ替え記号 \end{array}
意味をこのように分ける必要があります。
（つまりモデル内でのみ真偽入れ替えを行う）
補足しておくと
\begin{array}{lcl} 0は自然数である && 真になり得る \\ \\ 0は自然数ではない && 真になり得る \end{array}
「両方とも真仮定」は一般的にあり得る状態です。
（真偽が確定するモデル内では起き得ない）
含意Lと真理値
最後の「含意L」については
\begin{array}{ccc} Γ,A\to B\vdash Δ \\ \\ \Updownarrow \\ \\ A\to Bが前提として使える \\ \\ \Uparrow \\ \\ A\to B と \lnot A ∨ B の真理値は一致する \\ \\ \Uparrow \\ \\ Γ , \lnot A ∨ B \vdash Δ \\ \\ \Uparrow \\ \\ 否定Lと論理和Lを使える \\ \\ \Uparrow \\ \\ Γ\vdash A,Δ \quad B\vdash Δ \\ \\ \Uparrow \\ \\ Γ\vdash A \quad B\vdash Δ \end{array}
「直感的意味」ではなく
\begin{array}{ccc} A &B& \lnot A & \lnot B & & A→B & \lnot A∨B \\ \\ 1&1&0&0 && 1 & 1 \\ \\ 1&0&0&1 && 0 & 0 \\ \\ 0&1&1&0 && 1 & 1 \\ \\ 0&0&1&1 && 1 & 1 \end{array}
『真理値の一致』により結果が与えられていて
\begin{array}{ccc} \displaystyle \frac{ \displaystyle \frac{\displaystyle \frac{Γ \vdash A}{Γ \vdash A,Δ}(\mathrm{adR})}{Γ,\lnot A\vdash Δ \quad B\vdash Δ}(\mathrm{\lnot L}) }{Γ, \lnot A∨B\vdash Δ }(\mathrm{∨L}) \end{array}
この既存規則による変形と
\begin{array}{ccc} モデル内 && A→B &\Longleftrightarrow& \lnot A∨B \\ \\ モデル外 && A→B &\Longleftarrow& \lnot A∨B \end{array}
この関係が本体になります。
（モデル内での真理値一致が根拠の入れ替え操作許可）
量化子規則
これらの「代入」周りは面倒ですが
\begin{array}{ccc} \mathrm{All} && \displaystyle \frac{L,P(t)\vdash Δ}{L,\forall x\,\, P(x) \vdash Δ}(\mathrm{\forall L}) & \displaystyle \frac{Γ\vdash L,P(y)}{Γ\vdash L,\forall x \,\, P(x)}(\mathrm{\forall R}) \\ \\ \\ \mathrm{Exist} && \displaystyle \frac{L,P(y)\vdash Δ}{L,\exists x \,\, P(x) \vdash Δ}(\mathrm{\exists L}) & \displaystyle \frac{Γ\vdash L,P(t)}{Γ\vdash L,\exists x \,\, P(x)}(\mathrm{\exists R}) \end{array}
基本的には直感的な操作です。
（代入周りの話は別記事で詳しく解説）
量化子と自由変数
これは「 P(y) が真仮定である」ことから
\begin{array}{ccc} P(y)\vdash Δ &\Longrightarrow& P(y) は真仮定記号である \\ \\ Γ \vdash P(y) &\Longrightarrow& P(y) は真仮定記号である \end{array}
「変数のパターン」では
\begin{array}{lcl} P(y) &⇒& \forall x \,\, P(x) \\ \\ P(y) &⇒& \exists x \,\, P(x) \end{array}
これは『必ず成立しなければならない』と言えて
（自然言語定義の接続を考えると）
\begin{array}{ccc} 自由変数y+定数c &\Longleftrightarrow& 項t \end{array}
「定数でも成立するかどうか」についてだけは
確認が必要な部分になります。
自由変数パターンの自然言語定義
これらは本質的には言い換えに過ぎず
\begin{array}{ccc} P(y) \\ \\ \Downarrow \\ \\ P(y)は真仮定論理式記号である \\ \\ \Downarrow \\ \\ yに関係なくP(y)は真仮定である \\ \\ \Downarrow \\ \\ 全てのx でP(x) は成立する \\ \\ \Updownarrow \\ \\ \forall x \,\, P(x) \end{array}
「表現する方法」に変化があるだけで
\begin{array}{c} P(y) \\ \\ \Downarrow \\ \\ P(y)は真仮定論理式記号である \\ \\ \Downarrow \\ \\ P(y)が真仮定であるためのyが存在しなければならない \\ \\ \Downarrow \\ \\ P(x) が成立するxが存在する \\ \\ \Updownarrow \\ \\ \exists x \,\, P(x) \end{array}
『主張の中身』には変化がありません。
（ただし中身に言及している点で明確に役割が異なる）
定数でも成立するはず
「項 t 」の部分はこれを前提としていて
\begin{array}{ccc} 自由変数y &\to_*& 項t \\ \\ &\to_*&定数cでも成立 \end{array}
まず最初の段階では
「成立するはずだ」という予想が来ます。
\begin{array}{ccc} Γ\vdash P(c) \\ \\ \Downarrow \\ \\ P(c)は結論として導かれる \\ \\ \Downarrow \\ \\ P(c)以外で成立するかは分からない \\ \\ × \\ \\ 全てのx でP(x) は成立するが結論として導かれる \\ \\ \Updownarrow \\ \\ Γ\vdash \forall x \,\, P(x) \end{array}
しかし「 \forall \mathrm{R} 」を確認してみると
これは明らかに「モデル上では」成立しません。
\begin{array}{ccc} Γ\vdash P(c) \\ \\ \Downarrow \\ \\ P(c)は結論として導かれる \\ \\ \Downarrow \\ \\ P(x)が成立するcが存在するが結論として導かれる \\ \\ \Downarrow \\ \\ P(x) が成立するxは存在するが結論として導かれる \\ \\ \Updownarrow \\ \\ Γ\vdash \exists x \,\, P(x) \end{array}
逆に「 \exists \mathrm{R} 」では成立すると言えますが
（これの成立のために前提を変化させる必要は無い）
\begin{array}{ccc} P(c) \vdash Δ \\ \\ \Downarrow \\ \\ P(c)からΔが導かれる \\ \\ \Downarrow \\ \\ P(c)以外からΔを導けることは保証しない \\ \\ × \\ \\ P(a)でもΔを導ける \\ \\ \Downarrow \\ \\ P(x) が成立するxは存在するが前提として使える \\ \\ \Updownarrow \\ \\ \exists x \,\, P(x) \vdash Δ \end{array}
これは「 \exists \mathrm{L} 」では逆の結果になります。
（下の存在論理式が持つ情報は上の具体例より多い）
\begin{array}{ccc} P(c) \vdash Δ \\ \\ \Downarrow \\ \\ P(c)からΔが導かれる \\ \\ \Downarrow \\ \\ 前提が増えてもP(c)が前提ならΔは導かれる \\ \\ \Downarrow \\ \\ P(x)が真になるパターンを任意に追加できる \\ \\ \Downarrow \\ \\ cを含む任意の x でP(x) は成立するからΔが導かれる \\ \\ \Updownarrow \\ \\ \forall x \,\, P(x) \vdash Δ \end{array}
これも似たような感じになりそうですが
「 \forall \mathrm{L} 」の方は定数でも成立します。
（構造としては追加を大量に行った形を言い換えただけ）
まあ要はこういう話で
\begin{array}{lcl} P(c) \vdash Δ &\Rightarrow& \forall x \,\, P(x) \vdash Δ && 〇 \\ \\ P(c) \vdash Δ &\Rightarrow& \exists x \,\, P(x) \vdash Δ && △ \\ \\ Γ\vdash P(c) &\Rightarrow& Γ\vdash \exists x \,\, P(x) && 〇 \\ \\ Γ\vdash P(c) &\Rightarrow& Γ\vdash \forall x \,\, P(x) && △ \end{array}
「定数でダメな場合」が
『項 t で定義できない』規則になります。
長くなりましたが
以上で健全性定理の証明は終わりです。