|| 証明できないやつがいる感じ
「証明と公理の観察」から得られた成果
スポンサーリンク
目次
証明観察「不完全性定理を示す実際に起きること」
公理「定義からして証明が必要無いもの」
定義「公理と同様に数理の根底に来るもの」
生成規則「無限に長い証明文を作ることが可能」
非有界「後者が定義されると有限の範囲に収まらない」
無限後退「証明の前件にもまた根拠となる前件が必要」
不完全性定理「どうやっても証明できないやつは残る」
無限排除「証明可能という述語の定義段階で無限を排除」
定義分離「主張であるかどうかの判定で証明と分離可能」
定義層分類「モデル層と構文層と論理メタ層に分かれる」
公理不完全性定理「定理が主張するものとして公理が実在」
一般不完全性定理「公理だけじゃないかもしれない」
証明観察
「不完全性定理」の主張は
\begin{array}{lcl} 公理 &\to& 証明される場合は同一律 \\ \\ 定義 &\to& この根拠も更に定義できる \end{array}
実は直感的には明らかで
\begin{array}{lcl} 生成規則 &\to & 有限個の記号で表現できる文だけじゃない？ \\ \\ 自己参照 &\to& \cdots \vdash 公理\vdash 公理 \vdash 公理 \vdash 公理 \\ \\ 無限後退 &\to& \cdots ⇔ 定義群C ⇔ 定義群B ⇔ 定義A \end{array}
『これは証明できないはず』という観察結果を
ただ厳密に述べただけに過ぎません。
不完全性定理 Incomplete
|| 明らかに証明できないものがあるよね
『証明の定義整備』から導かれる「証明不可」
\begin{array}{lcl} 発想源事実 && 公理も定義も無限記述も証明できない \\ \\ 証明予想概観 && 公理の存在を外すことはできそうにない \\ \\ \\ 形式証明概観 && 公理の振る舞いを証明不可と結びつける \\ \\ 形式証明構成 && 公理を抽象化し範囲を広げる \end{array}
この定理の証明の概観はこんな感じです。
（これで形式的にまとまったものが定理の証明文）
証明への願望的要請
これは昔の話になりますが
\begin{array}{lcl} 正しいもの &\to& 証明できる \\ \\ 全ての正しいもの &\to& 証明できるはず \end{array}
「形式証明」において
『その時代の人類』はこのように想定していました。
（この根拠は完全性定理という形で存在していた）
\begin{array}{lcl} 科学的事実 &\to& 原子の存在 \\ \\ 公理の自己参照 &\to& 底があるはず \\ \\ 定義の無限後退 &\to & これも底があるはず \end{array}
残念なことに
\begin{array}{ccc} 原子の存在 &\to& 素粒子の存在 &\to& 観測限界実体 \end{array}
実態とは異なるわけですが
『必ず有限の証明が存在する』と思われていて
「証明できないもの」は『無い』と考えられていました。
全てが証明可能という背理法の仮定
↑ に由来するのがこの仮定で
\begin{array}{lcl} 願望的要請仮定 && 全て証明できるはず \\ \\ 例外正当化試行 && 公理や定義もいけるはず \\ \\ 仮定検証準備 && 証明の形式から前提を整備 \end{array}
これが「否定される」というのが
『不完全性定理』の内容になります。
概観と中身の補強
以上の「感覚層」の話から
\begin{array}{lcl} 証明の概観 && 証明できないやつがある？ \\ \\ 背理法の仮定 && 全て証明可能であって欲しい \end{array}
「証明の概観」と「背理法の仮定」が得られたので
\begin{array}{lcl} 最小単位 && 公理とか証明文とか \\ \\ 生成規則 && 許されるべき証明の操作とか \\ \\ 証明の全体像 && 証明文として認められるもの全て \end{array}
次は『証明の全景』を得るために
↑ の話を形式に落とし込んでいきます。
健全性定理による構成的定義の導出
詳細は長くなるので結論だけ。
\begin{array}{lcl} 証明の構成 & \left\{ \begin{array}{lcl} 最小単位 &\to& 論理公理 \\ \\ 生成規則 &\to& \mathrm{Modus} \,\, \mathrm{Ponens} \end{array} \right. \end{array}
「不完全性定理」におけるこの部分は
「健全性定理」が導いた『証明の構成的定義』であり
\begin{array}{ccc} 健全性定理 & \left\{ \begin{array}{lcl} \mathrm{Hilbert} && 不完全性定理の前 \\ \\ \mathrm{Gentzen} && 不完全性定理の後 \end{array} \right. \end{array}
時系列としては
「 \mathrm{Hilbert} 健全性定理の成果」がこの定理の基礎になります。
（この部分の詳細は健全性定理の記事で行います）
\mathrm{Gentzen} 健全性定理での翻訳
「構文」と「集合」の分離ができるため
念のため補足しておくと
\begin{array}{ccc} \mathrm{Gentzen}の定義 & \left\{ \begin{array}{lcl} 最小単位 &\to& 真仮定論理式記号 \\ \\ 生成規則 &\to& 各記号規則 \end{array} \right. \end{array}
「 \mathrm{Gentzen} 健全性定理」におけるこれらは
このような形で定義されます。
補足しておくと
\begin{array}{ccc} 矛盾 & \left\{ \begin{array}{lcl} 文法エラー &\to& 許されない記号操作 \\ \\ 文エラー &\to& 論理式の真偽が合わない \end{array} \right. \end{array}
「 \mathrm{Gentzen} の証明」では
『矛盾』という概念はこのように分離されています。
（構文レベルでは集合モデル内の矛盾が無視される）
集合モデル範囲外における全
「不完全性定理」は『集合モデル外』の話なので
（集合という実体が存在するモデルの外の話）
\begin{array}{lcl} 全ての証明文 &\to& 定義できない \\ \\ 証明文の性質 &\to& 要請として定義できる \end{array}
厳密には『全て』という表現は扱えません。
（集合内でしか「全て」は厳密に定義できない）
\begin{array}{ccc} pは証明文 &⇒& pは有限記述可能 \end{array}
しかし『対象が持つ性質』は定義でき
（１つを述語というフィルターに通すことは可能）
\begin{array}{ccc} pは有限記述不可または不明 &⇒& pは証明文ではない \end{array}
この時点で『無限個の記号文』は自動的に排除されます。
（有限性要請により「定義」と「公理」に候補が絞られる）
メタ記号の意味
念のため確認しておくと
この記事で一部扱う ↓ の記号は
\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}{lcl} 集合モデル内の全 &\to& モデルの範囲内 \\ \\ 構文レベルの全 &\to& 記号の有限記述範囲 \\ \\ 論理メタレベルの全 &\to& 確認ができる範囲 \\ \\ メタレベルの全 &\to& 無制限の全 \end{array}
これは恣意的な制限ではなく
『メタレベルにおける必然』です。
\begin{array}{ccc} 無制限の全 & \left\{ \begin{array}{lcl} 実体の存在が不明なもの \\ \\ 形式化が可能か不明なもの \\ \\ 将来的に実現されるもの \end{array} \right. \end{array}
『確認可能性』の観点から
「全」はメタレベルにおいて全容の把握が不可能
\begin{array}{ccc} 存在しない &\to& 全が広過ぎて確認が不可能 \end{array}
同様に、この確認も不可能で
（典型的な悪魔の証明の型）
結果、『確認可能性』の観点から
\begin{array}{ccc} 存在する &\to& 1つでも実体が確認されれば良い \end{array}
メタレベルではこの表現だけが許されることになります。
（より厳密には『論理であるならば』という要請の元では）
メタレベルにおける要請と構成
「要請的定義のみ許される」というのも同様
\begin{array}{lcl} 要請的定義 &\to& xは性質Pを満たす \\ \\ 構成的定義 &\to& 定義対象AをBであるとする \end{array}
とても単純な話で
\begin{array}{lcl} 集合モデル内 &\to& 集合という実体が使える \\ \\ 集合モデル外 &\to& 集合という実体は存在しない \end{array}
『構成的な定義を行う』場合
「定義に必要な実体が無い」なら
（構文レベルでは「記号」が実体となる）
\begin{array}{ll} メタレベル & 初期値は空集合とする &判定不能 \\ \\ 集合モデル内 &初期値は空集合とする & 判定可能 \end{array}
当然、それを定義することはできません。
（要請的定義は実体の有無を問わない）
定義は証明ではない
以上を踏まえて
『定義』は「文」であり「根本原理」ですが
\begin{array}{lcl} 論理式 &\to& AはBである & 断言 \\ \\ 定義 &\to& AをBとする & 宣言 \end{array}
『定義』は「決めるという宣言」であるため
（真偽を問われる断言と文の型が不一致）
\begin{array}{lcl} pは証明文 &\Rightarrow& pは主張である \\ \\ qは主張ではないか判別不能 &\Rightarrow& qは証明文ではない \end{array}
『証明として導かれる論理式』の定義を満たしません。
（定義の役割はそれがどんなものか『説明』すること）
公理は例外として残る
以上の結果から
「証明文の要請」を満たすものとして
\begin{array}{ccc} 公理仮定 & \left\{ \begin{array}{lcl} 証明されない &\to& 不完全性定理の成立 \\ \\ 証明されるはず &\to& ここの検証が必要 \end{array} \right. \end{array}
『公理』だけが残りこのように仮定されるため
\begin{array}{ccc} 公理の定義により公理は証明できない \\ \\ \Downarrow \\ \\ 公理は証明可能ではない \\ \\ \Downarrow \\ \\ 証明できるという仮説は棄却される \end{array}
この結果として
「不完全性定理（具体的）」は示されることになります。
（公理という証明できないものが存在する）
定義層
『公理の定義』が曖昧なので
「どの定義か」について整理しておくと
\begin{array}{lcl} 集合モデル層 && あらゆる実体がある \\ \\ 構文モデル層 && 記号のみが実体で述語も限られる \\ \\ 論理メタ層 && 確認可能性が要請される範囲 \\ \\ メタ層 && なんでも許される \end{array}
『定義に使われている述語』の中でも
「確認可能である」という『述語』は最上位にあり
\begin{array}{lcl} 直感表現 && 人間が確認可能 \\ \\ 数理表現 && 人間が数えられる個数の記号で記述が可能 \end{array}
『メタ層への要請』である「確認可能」は
『正確には』このような形で定義されています。
（ここの正確性は読み取りによる主観依存性が低いこと）
論理であるという要請
先に語ったように
これらは恣意的な定義ではなく
厳然たる「論理に対する要請」であり
\begin{array}{lcl} メタ層 &\to& 論理メタ層 \\ \\ 無制限 &\to& 一部に制限 \end{array}
「論理である」ためには
『確認可能性』が必須になります。
（メタ層を「確認できるものだけ」に制限する）
\begin{array}{lcl} 全て &\to& 無制限だと何が入るか不明 \\ \\ 存在しない &\to & 典型的な悪魔の証明になる \end{array}
『確認できない定義』は
「あったとしても分からない」ので。
（全ての情報を私たちは認識できない）
確認可能性と有限性
↑ で述べたように
\begin{array}{lcl} 直感表現 && 人間が確認可能 \\ \\ 数理表現 && 人間が数えられる個数の記号で記述が可能 \end{array}
『メタ層への最上位の要請』はこうなっていますが
（有限性という数的感覚は最上位の定義になる）
\begin{array}{lcl} 最低限の要請 & \left\{ \begin{array}{lcl} 確認可能 \\ \\ 有限記述可能 \end{array} \right. \end{array}
これは何が優勢というわけではなく
『同じ感覚』に対する「表現方法が異なる」だけです。
\begin{array}{lcl} 短いフレーズ &\to& 確認可能が優勢 \\ \\ 解釈が割れない &\to& 有限記述可能が優勢 \end{array}
区別の必要性は「評価軸」に依存します。
（この辺りはもう完全に主観依存）
公理不完全性定理
以上の整理から分かる通り
\begin{array}{lcl} 公理 & \left\{ \begin{array}{lcl} メタ層で定義済み &\to & 有限記述可能 \\ \\ 明らかに正しい &\to& 真と仮定されている \\ \\ 証明できない &\to& 推論未発見 \end{array} \right. \end{array}
『公理』への要請はこのようになっており
（上位の要請は再記述しても意味は変わらない）
\begin{array}{lcl} 公理 & \left\{ \begin{array}{lcl} メタ層要請 && 有限記述可能 \\ \\ 論理メタ層要請 && 現時点推論未発見 \\ \\ 構文モデル層要請 && 真仮定論理式記号 \\ \\ 集合モデル層要請 && 真 \end{array} \right. \end{array}
各階層でこのような縛りを受けるため
（この概念は層の位置で意味が変化する）
\begin{array}{ccc} 公理である &\Longrightarrow& 有限推論未発見である \end{array}
「構文モデル層」で公理に課された縛りと
\begin{array}{lcl} 矛盾する &\Longrightarrow&証明できない \\ \\ 現時点で推論が未発見 &\Longrightarrow& 証明できない \end{array}
「証明できない」の定義から
（これの詳細は完全性定理の記事で）
\begin{array}{ccc} Aは公理である \\ \\ \Downarrow \\ \\ Aは有限の推論が現時点で発見されていない \\ \\ \Downarrow \\ \\ Aは証明できない \\ \\ \Downarrow \\ \\ Aは証明可能ではない \\ \\ \Downarrow \\ \\ Aは証明できるという仮定は否定される \end{array}
定義接続の結果として
「不完全性定理」は証明されます。
（厳密には定理が主張する実体の存在が証明される）
一般不完全性定理
「 \mathrm{Gödel} の不完全性定理」で出てくる
『 \mathrm{Gödel} 文』という概念は
\begin{array}{lcl} Aは公理 &\Longrightarrow& Aは有限推論未発見 \\ \\ Gは\mathrm{Gödel}文 &\Longleftrightarrow& Gは有限推論未発見 \end{array}
この『証明できない』の本質になる
『公理が持つ性質の一部』を抽出したもので
（元のものは層の混線により不適切な定義になっている）
\begin{array}{ccc} Gは\mathrm{Gödel}文 &\Longrightarrow& Gは証明できない \end{array}
必然的に「証明できない」ものになります。
（そうなるように創られたんだから当然）
結果として
\begin{array}{ccc} 公理である &\Longrightarrow& \mathrm{Gödel}文である \end{array}
「公理」よりも広い範囲をカバーできるようになった
（証明できないものが公理だけだとは限らないという感覚）
\begin{array}{ccc} Gは\mathrm{Gödel}文である \\ \\ \Updownarrow \\ \\ Gは有限の推論が現時点で発見されていない \\ \\ \Downarrow \\ \\ Gは証明できない \\ \\ \Downarrow \\ \\ Gは証明可能ではない \\ \\ \Downarrow \\ \\ Gは証明できるという仮定は否定される \end{array}
「 \mathrm{Gödel} 文」を採用したこの形が
『一般の不完全性定理』の主張になります。