|| 正しいなら証明できるでしょ
『正しい』を「証明できる」で定義するには
スポンサーリンク
目次
完全性「正しいなら証明できるはず」
無矛盾「現時点で矛盾が無いこと（永劫ではない）」
非証明可能「証明ができない（矛盾だけじゃない）」
公理観察「公理が数学でどういう位置にあるか」
矛盾修正過程「矛盾が証明されてそれを修正するまで」
完全性定理「正しさを証明的正しさに限定」
真確定と証明可能の接続「完全性定理の核となる概念接続」
正しさの種類「完全性定理で扱うのは証明的な正しさ」
定理の前提
この話で出てくる記号は特殊なので
\begin{array}{ccl} M && Mはモデル \\ \\ Γ && Γは0個以上の真仮定論理式の有限列 \\ \\ φ && φは真仮定論理式 \end{array}
ここでしっかり確認しておいてください。
（記号に性質を要請する形で定義される）
補足しておくと
\begin{array}{lcl} Γ_0 &=& × && 省略可 \\ \\ Γ_2 &=& p,p→q \end{array}
「真仮定論理式有限列 Γ 」の中身はこんな感じです。
（有限列なので無限個になることは無い）
健全性定理も前提になる
「推論規則」の定義については
\begin{array}{ccl} \vdash && 推論規則が使える \\ \\ \vDash && 推論規則が使えない \end{array}
「健全性定理」という形で独立しているとして
（モデル上の話と推論規則を切り離す）
\begin{array}{lcl} M\vDash φ &\Longleftrightarrow& モデルM上でφは真確定 \\ \\ M\vDash Γ &\Longleftrightarrow& モデルM上でΓの各論理式は真確定 \end{array}
この「真確定記号 \vDash 」は
『モデル上での記号の振る舞い』を意味するとします。
（下の Γ の定義は有限個の論理式をまとめた省略表現）
メタ記号の意味
この記事で扱う ↓ の記号は
\begin{array}{ccc} メタ記号 & \left\{ \begin{array}{ccl} \vdash && 証明可能（推件式） \\ \\ \vDash && 真確定（真偽確定宣言） \\ \\ ⇒ && 真保証（根拠の提示）\\ \\ ⇔ && 記号定義 \\ \\ , && 記号区分 \end{array} \right. \end{array}
「健全性定理」で扱ったものと同じで
\begin{array}{ccc} Γ\vdash φ &\Longleftrightarrow& 前提Γから結論φが導かれる \\ \\ Γ\vDash φ &\Longleftrightarrow& Γがφの真を確定させる \\ \\ A⇒B &\Longleftrightarrow& Aが真ならBの真を保証する \\ \\ A⇔B && AをBと定義する \end{array}
こういう意味を持つとします。
（循環回避のため定義記号は自然言語で同一視する）
ローカルなメタ記号
またこの記事に限り
\begin{array}{ccc} A\to_* B &\Longleftrightarrow& AからBに繋がる \end{array}
これは「含意 \to 」との混同を避けるため
このような意味で用いることにします。
（他の記事で適当に使ってる \to はこれ）
完全性 Completeness
|| 正しいものは証明されるという性質
「正しい」のなら『証明できるはず』
\begin{array}{ccc} Γ\vDash φ & \Longrightarrow & Γ \vdash φ \end{array}
「完全性定理」が提供するのは
\begin{array}{lcl} Γ\vDash φ \overset{〇}{\Longrightarrow} Γ \vdash φ && 完全性が成立する \\ \\ Γ\vDash φ \overset{×}{\Longrightarrow} Γ \vdash φ && 完全性が成立しない \end{array}
「完全性が成立する条件」です。
（基本的には成立せず範囲は限定的）
完全性定理 Completeness Theorem
|| 正しいを厳密に証明で定義する
「正しい」なら『証明されなければならない』
\begin{array}{ccc} 正しい &なら & 証明できる & はず \\ \\ モデル上で真 &なら& 証明できる & が保証される \\ \\ Γ\vDash φ &⇒& Γ\vdash φ \end{array}
『完全性が成立する範囲』を整備した成果で
\begin{array}{lclcl} 健全性定理 && 証明への要請 &\to_*& 証明の構成 \\ \\ 完全性定理 && 完全性成立要請 &\to_*& 成立条件整備 \end{array}
これも形としては「健全性定理」と同様です。
（完全性成立という要請を満たす具体的な条件がこれ）
無矛盾 Consistency
|| 今の時点で矛盾が無い
これは「数学全体に要請される」もので
\begin{array}{ccc} 無矛盾 &\Longleftrightarrow& 現時点で矛盾が無い \end{array}
「永遠に矛盾が無い」を意味しません。
（既存の理論はどれだけ正確でも全てこの状態）
\begin{array}{ccc} Γ \not\vdash \bot &\Longleftrightarrow& 前提Γは現時点で矛盾 \bot を導かない \end{array}
また記号ではこのように表現されます。
（非証明可能記号 \not\vdash については後述）
非証明可能 Unprovable
|| 証明可能と対になる概念
「導かれない」を表現するためのもの
\begin{array}{lcl} Γ\vdash φ &\Longleftrightarrow& 前提Γからφが導かれる \\ \\ Γ \not\vdash φ &\Longleftrightarrow& 前提Γからφが導かれない \end{array}
「記号表現」と「自然言語定義」はこんな感じです。
（証明可能 \vdash と同様に推件式で定義できる）
非証明可能と反証明可能
↓ は一見すると同様に見えますが
\begin{array}{ccl} 非証明可能 && Γ \not\vdash φ \\ \\ 反証明可能 && Γ \vdash \lnot φ \end{array}
「非証明可能 \not\vdash 」という概念は
「反証可能」とは明確に異なった概念になります。
（単純な否定 \lnot ではうまく定義できない）
というのも
「連続体仮説 \mathrm{CH} 」や「ススリン仮説 \mathrm{SH} 」など
（より広範には否定できる根拠が無い予想なども）
\begin{array}{lcr} Γ &\not\vdash & \mathrm{CH} \\ \\ Γ & \not\vdash & \lnot\mathrm{CH} \end{array}
『有限の記述での証明が未発見のもの』は
「真とも偽とも判断ができない」ため
（前提 Γ などに有限が要請される）
\begin{array}{ccc} 非証明可能 & \left\{ \begin{array}{lcl} 矛盾する \\ \\ 有限個の記号で表現できる推論が未発見 \end{array} \right. \end{array}
「反証されたもの \lnot φ 」もまた
『証明ができないもの』に含まれる場合があります。
（つまり非証明は反証明を意味するとは限らない）
公理観察 Axioms
「無矛盾」というのは
「モデル M 」の観点から見た場合
\begin{array}{lcl} Mを構成 &\to_*& 公理が選択される \\ \\ & \to_* & 選択された公理の記号列がΓに \\ \\ \\ &\to_* & 推論規則が採用される \\ \\ &\to_* & 導出されたものはモデル内に追加 \\ \\ &\to_* & 導出されたものはΓに追加できる \end{array}
『動的な評価』であるため
（導かれるものが増える度に評価する）
\begin{array}{ccc} 公理有限列Γ & \left\{ \begin{array}{lcl} 推論規則適用前のΓ \\ \\ 推論規則適用後の追加されたΓ \end{array} \right. \end{array}
これらは区別する必要があります。
（静的に扱えるのは公理を選択した時点の Γ ）
採用段階公理有限列 Γ
そして「公理有限列 Γ 」を区別し
「静的な公理の有限列 Γ 」を採用する場合
\begin{array}{lcl} 採用公理 && Γ && 無矛盾評価はまだ \\ \\ 公理追加 && Γ,A && 無矛盾評価はまだ \end{array}
「公理」が『無条件で真と仮定される』ことから
『この時点での追加』は好きに行えると言えます。
（無矛盾と同様にこれで矛盾が出る可能性はある）
矛盾修正過程 Consistency-Seeking
これは『無矛盾を目指す』上での
「一階述語論理などの設計思想」の話で
（より厳密には数学全体に向けられた思想）
\begin{array}{lcl} 仮説構成 && こうであるはず \\ \\ 矛盾発見 && 規則の組み合わせで矛盾が構成できる \\ \\ 矛盾除去 && 発見された矛盾が導かれないようにする \\ \\ 新仮説誕生 && その時点で矛盾の無い仮説が得られる \end{array}
この「矛盾修正」から導かれたのが
\begin{array}{lcl} 矛盾が証明される &\to_*& 矛盾する \\ \\ 矛盾が証明されない &\to_* & 矛盾の排除成功 \end{array}
『現代の数学』になります。
（つまり『発見された矛盾が導かれない仮説』が現代数学）
非証明と前提の追加
以上のことから分かるように
「公理の振る舞い」や「矛盾排除」から
\begin{array}{lcc} Γから矛盾φが導かれない \\ \\ ￢φを追加してもΓが導けるものは変わらない \\ \\ \\ Γから真偽不明φが導かれない \\ \\ ￢φを追加してもΓが導けるものは変わらない \end{array}
『非証明 φ の否定』の「追加」は正当化されます。
（完全性定理ではこの観察から得られた事実を使う）
真確定と証明可能の接続
「完全性定理」の概観は
\begin{array}{lcc} Γ\vDash φ &\Longleftrightarrow& Γによりφが確定で真になる \\ \\ && \Downarrow \\ \\ Γ \vdash φ &\Longleftrightarrow& Γからφが導かれる \end{array}
こんな感じなんですが
\begin{array}{ccc} Γ\vDash φ &\Longleftrightarrow& Γによりφが確定で真になる \end{array}
まだ肝心のこれについては
あまり厳密には定義されていません。
（自然言語定義自体は上記のものと考えて良い）
\begin{array}{lcl} M\vDash φ &\Longleftrightarrow& モデルM上でφは真確定 \\ \\ M\vDash Γ &\Longleftrightarrow& モデルM上でΓの各論理式は真確定 \end{array}
なのでこの定義に沿う形で
「 Γ\vDash φ 」はきちんと定義する必要があります。
完全性定理の前提部分
なんとなくわかるとは思いますが
\begin{array}{ccc} Γ\vDash φ &\Longleftrightarrow& Γによりφが確定で真になる \end{array}
これは「省略表現」だと考えると整合的です。
（ M\vDash Γ の定義と同様であるとすると整合する）
というのも
「モデル上のシンプルな定義」を考えるなら
（より正確には『厳密な意味』を考えるなら）
\begin{array}{ccc} \left. \begin{array}{lcc} M\vDash Γ \\ \\ M\vDash φ \end{array} \right\} &\to_* & Γ\vDash φ \end{array}
「右の記号 \vDash 」は
『左側の Γ？φ の ？ 』を表現してるはずなので
\begin{array}{ccc} Γ⊨φ && M⊨Γ & M\vDash φ \\ \\ 真確定 && Mの実在不明 & Mの実在不明 && 非同値 \\ \\ 真確定 && ？ & 真確定 && 非同値 \\ \\ 真確定 && 真確定 & ？ && 非同値 \\ \\ 真確定 && 真確定 & 真確定 && 同値 \end{array}
これを踏まえた上で
『モデル M の実在を切り離して考える』と
\begin{array}{ccc} Γは確定でφを真とする \\ \\ \Updownarrow \\ \\ Γの各論理式が全て真確定のモデル上ではφも真確定 \end{array}
このように定義すれば
「記号が表現したい感覚」にきちんと整合します。
（ M\vDash Γ と Γ\vDash φ が真であれば M\vDash φ とできる）
真確定の対称的表現
この定義が定まることにより
「１つでも真確定ではない」という形で
\begin{array}{lcl} M\not\vDash φ &\Longleftrightarrow& M上でφは真確定ではない \\ \\ M\not\vDash Γ &\Longleftrightarrow& M上でΓの各論理式は真確定ではない \end{array}
「非証明可能 \not\vdash 」のように
（非証明と同様に単純な否定にはならない）
\begin{array}{c} Γ\not\vDash φ \\ \\ \Updownarrow \\ \\ Γは確定でφを真にしない \\ \\ \Updownarrow \\ \\ Γの各論理式が真確定のモデル上でφは真確定ではない \end{array}
これはこのように定義できます。
（真確定ではないは「矛盾か有限推論未発見」で定義可能）
正しさの種類
↑ の話の補足として
\begin{array}{ccc} 正しさ & \left\{ \begin{array}{lcl} 主観的正しさ && 主観 \\ \\ 証明的正しさ && 客観に近い主観 \\ \\ 客観的正しさ && 真理 \end{array} \right. \end{array}
実は「完全性定理」の中では
『正しさ』という概念には厳密な定義が与えられていて
（「厳密な意味での正しさ」は主観的正しさに該当する）
\begin{array}{ccc} 直感的正しさ &>& 厳密な正しさ &>& 証明的正しさ \end{array}
『厳密な意味での正しさ』と
『証明的な意味での正しさ』が
\begin{array}{ccc} 完全性定理の真 & \left\{ \begin{array}{lcl} 厳密な意味 &←_*& 証明で定義 \\ \\ 証明的意味 &←_*& 健全性定理 \end{array} \right. \end{array}
この「完全性定理で扱う正しさ」の中身になります。
（つまり正しさの意味が客観寄りに限定されている）
まとめると
\begin{array}{lcl} 証明への要請 &\to_* & 健全性定理で定義 \\ \\ 厳密な正しさへの要請 &\to_* & 証明的正しさで定義 \end{array}
「完全性定理」が果たす役割は
『厳密な意味での正しさ』の「定義」です。
（つまり全ての正しさではなく客観に近いものだけを扱う）
矛盾修正過程と定義接続
以上を踏まえた上での
「完全性定理の中核」となる ↓ については
\begin{array}{lcl} 正しい&なら & 証明できなければならない \\ \\ 証明されない & なら & 正しくならない \end{array}
「矛盾修正過程」の観察から
『正しい』の意味を限定する形で
（定理を矛盾修正の手順で再解釈する）
\begin{array}{ccc} 厳密に正しい &⇒& 矛盾でも有限推論未発見でもない \\ \\ 直感 && 証明 \end{array}
「自然言語定義接続」により
（厳密な正しさを証明的正しさで定義し接続する）
\begin{array}{ccc} Γ\vDash φ ⇒ Γ\vdash φ \\ \\ \Updownarrow \\ \\ φが正しいならφは証明できる \\ \\ \textcolor{pink}{\Uparrow} \\ \\ φが矛盾や有限推論未発見でないならφは証明できる \\ \\ \textcolor{pink}{\Uparrow} \\ \\ φが証明されなくなればφは矛盾か有限推論未発見 \\ \\ \textcolor{pink}{\Uparrow} \\ \\ φが証明されないならφは正しくならない \\ \\ \Updownarrow \\ \\ Γ\not\vdash φ ⇒ Γ\not\vDash φ \end{array}
このような形で言い換えることができます。
（これでほぼ答えだがまだ『モデルの存在』が不明）
言い換えの必要性
記号の定義から分かるように
\begin{array}{ccc} Γ\vDash φ &\Longleftrightarrow& Γによりφが確定で真になる \end{array}
これは『かなり抽象的』な主張です。
（記号の定義の時点では正しさに制限が無い）
実際に観察される「矛盾修正過程」から
\begin{array}{ccc} モデル上で正しい &\Longleftrightarrow& \left\{ \begin{array}{lcc} 矛盾ではない \\ \\ 有限推論未発見ではない \end{array} \right. \end{array}
この関係を得ることは可能ですが
（特に矛盾は証明されないようにして解消する）
\begin{array}{ccc} Γ\vDash φ &\to_*& ？ \end{array}
この関係から ↑ の「正しさの定義」は出てきません。
（この定義が主張するのはあくまで Γ と φ の関係）
まとめると
\begin{array}{ccc} Γ\vDash φ && 正しい &\overset{？}{\to}& 証明 \end{array}
ここからは考察が進まないのに対し
（正しさの範囲が広すぎるので証明と接続できない）
\begin{array}{ccc} 矛盾修正過程 &\to_*& 数学上の正しさとは \end{array}
『証明側から』なら考察が進んだ結果
\begin{array}{ccl} Γ\vDash φ ⇒ Γ\vdash φ && 正しいとは？ \\ \\ Γ\not\vdash φ ⇒ Γ\not\vDash φ && 正しさを証明範囲へ \end{array}
この形に変形されたというのがこの言い換えの動機です。
（ Γ\vDash φ から直接導けるならそれが望ましい）
非証明とモデル生成
↑ まで整備できれば
\begin{array}{ccc} \Bigl( Γ\not\vdash φ ⇒ Γ\not\vDash φ \Bigr) &\Longrightarrow& \Bigl( Γ\vDash φ ⇒ Γ\vdash φ \Bigr) \end{array}
後は『 ↑ の左側を成立させるモデルの存在』さえわかれば
「完全性定理」が成立するための条件は揃うので
\begin{array}{ccc} Γ \not\vdash φ &\Longleftrightarrow& Γからφが導かれない \end{array}
『モデルの生成過程』における「公理観察」から
（公理を選んで推論規則を適用して無矛盾の確認をする）
\begin{array}{lcc} 前提 && Γ\not\vdash φ \\ \\ && \Downarrow \\ \\ 具体化 && Γ\not\vdash φ であり Γ\not\vdash \bot でもある \\ \\ &&\Downarrow \\ \\ 追加規則 && Γに\lnot φ を追加しても無矛盾である \\ \\ &&\Downarrow \\ \\ 着地 && Γに\lnot φを加えたモデルを生成できる \end{array}
「矛盾排除」の手順を参考にする形で
『モデルの存在』をこのような形で導出します。
（証明で許すべき操作のみでモデルの存在は示される）
モデルの存在と定義接続
以上の前提整備により得られる結果として
\begin{array}{ccc} M \vDash \lnot φ &⇒& M \not\vDash φ \\ \\ \lnot φは真 && φは偽 \end{array}
「モデル M 上では」『真偽が確定する』ことから
（この M は Γ,\lnot φ を真確定とする無矛盾なモデル）
\begin{array}{ccc} Γ\not\vdash φ && Γから φ は導かれない \\ \\ && \Downarrow \\ \\ M \not\vDash φ && ￢φが真確定のモデルが存在する \\ \\ && \Downarrow \\ \\ Γ\not\vDash φ && M\vDash Γ であり M\not\vDash φ となるモデルが存在する \end{array}
こうなると言えるので
\begin{array}{ccc} Γ\not\vdash φ &⇒& Γ \not\vDash φ \end{array}
結果、これが成立し
（成り立つモデルが実在する）
\begin{array}{ccc} Γ\not\vdash φ & ⇒ & Γ \not\vDash φ \\ \\ & \Downarrow \\ \\ Γ\vDash φ & ⇒ & Γ\vdash φ \end{array}
「完全性定理」は示されることになります。
（上側と全体が真なので下の真が保証される）