|| 人間がなにかを推測するときの考え方
『論証』を数理に落とし込んだもの
スポンサーリンク
目次
生成「証明文の最小単位と作り方」
公理系「公理＋系（まとまり）という解釈が自然」
推論規則「人間が扱う推論の形（帰納と演繹）」
帰納「一部から全体を得る推論の感覚」
演繹「基礎から結論を得る推論の感覚」
判定「判定できる ⇔ 確認方法が存在する」
証明可能性「証明できるかどうかっていう性質」
定理「公理と妥当な推論から導けるもの」
要請「証明が持つべき性質」
完全性「正しいなら証明できるという性質」
健全性「証明できるなら正しいという性質」
形式的証明「証明文とは何かの厳密な要請的定義」
証明 Proof
これは「論証」についての話なので
まずこれについて確認しておくことを推奨します。
\begin{array}{c} \mathrm{and}&かつ&それに &&\to&& ∧ \\ \\ \mathrm{or}&または&もしくは &&\to&& ∨ \end{array}
話の内容はこんな感じなので
（数学では言語の本質を統一的に表現する）
\begin{array}{ccc} 一緒の感覚 &\overset{言語化}{\longrightarrow}& \left( \begin{array}{c} \mathrm{and} \\ \\ と \\ \\ かつ \\ \\ であり \\ \\ それに \\ \\ \vdots \end{array} \right) &\overset{形式化}{\longrightarrow}& ∧ \end{array}
「論証」について知らなくても
感覚的には理解できると思うんですけど
\begin{array}{lcl} 感覚層 && 直感的に感じる正しさ \\ \\ 言語層 && 感覚を大雑把に言語で表現 \\ \\ 形式層 && 言語の本質を統一的に表現 \end{array}
「言語化」「形式化」の層における
『厳密な意味』はよく分からないと思います。
\begin{array}{ccc} 証明論 & \left\{ \begin{array}{ll} 生成 & \left\{ \begin{array}{l} 公理系 \\ \\ 推論規則 \end{array} \right. \\ \\ \\ 判定 & \left\{ \begin{array}{l} 証明可能性 \\ \\ 定理 \end{array} \right. \\ \\ \\ 要請 & \left\{ \begin{array}{l} 完全性 \\ \\ 健全性 \end{array} \right. \end{array} \right. \end{array}
特に「公理系」と「健全性」は理解し辛いかと。
（感覚的には分かっても精密な理解は難しい）
生成 Unified Rule
|| 証明文の最小単位と作り方
\begin{array}{lcl} 公理系 && 証明の最小単位 \\ \\ 推論規則 && 証明文の作り方 \end{array}
「言語」を前提とする概念ですが
基本的にはこれらによって「証明」は形成されます。
公理系 Axiom Set
|| 公理の集まりを意味する用語
そのまま「公理」＋「系（集まり）」
\begin{array}{ccc} 公理系 & \left\{ \begin{array}{lcl} 古い意味 && 形式体系の定義 \\ \\ 自然な意味 && 公理の集まり \end{array} \right. \end{array}
多くの古い文献では
「形式体系の定義」を意味することがありますが
（公理化と形式化の区別が曖昧な時代の名残）
\begin{array}{llcl} 有限記号 & \mathrm{Alphabet} && a,b,x,y,+など \\ \\ 構文規則 & \mathrm{Formation}\,\,\mathrm{Rules} && 厳密な文法 \\ \\ 公理& \mathrm{Axioms} && 性質と存在の宣言 \\ \\ 推論規則 & \mathrm{Rules}\,\,\mathrm{of} \,\,\mathrm{Inference} && 演繹操作 \end{array}
これは「証明系」「証明体系」と呼ぶべきもので
「公理系」という単語とは意味が乖離しています。
（近年ではこの意味での使用は避けられている）
推論規則 Inference Rules
|| 全体の推測と積み上げのこと
「帰納（一部→全体）」と「演繹（基礎→結論）」
\begin{array}{ccc} 推論規則 & \left\{ \begin{array}{lcl} 帰納的推論 && 一部から全体を推測 \\ \\ 演繹的推論 && 一から積み上げていく \end{array} \right. \end{array}
より平易な表現に言い換えるなら
\begin{array}{ccc} 帰納 &\Longleftrightarrow& 全体推測 && 一部\to 全体 \\ \\ 演繹 &\Longleftrightarrow& 積上推測 && 基礎\to 結論 \end{array}
このように表現するのが適切だと言えます。
（数学的帰納法は厳密には演繹に含まれる）
妥当な推論規則
この「推論規則」の中でも
『ちゃんとした推論規則』のことを
\begin{array}{ccc} 妥当な推論規則 & \left\{ \begin{array}{lcccc} \mathrm{MP} && p,p\to q & ⇒ & q \\ \\ \mathrm{GEN} && A &⇒& \forall x \,\, A \end{array} \right. \end{array}
（ Modus Ponens と全称化の２つだけと思って良い）
ざっと補足しておくと
\begin{array}{ccl} \mathrm{MP} && pからqを導ける \\ \\ && pが真でp\to qも真ならqは真 \\ \\ \\ \mathrm{GEN} && 全てのxはAである \\ \\ && Aが真なら全てのxでAが成立する \end{array}
これらの意味はこんな感じです。
（詳細は推論規則の記事で）
判定 Decision
|| ～であるかどうかを確認すること
「こうである」の『真偽を得る手続き』
\begin{array}{lcrcr} 直感 && xを判定可能 &\Longleftrightarrow& xを確認する方法が存在 \\ \\ 形式 && 判定可能 &\Longleftrightarrow& 真偽出力確定手続きが存在 \end{array}
「性質」と呼ばれるものは
\begin{array}{lcl} AはBである &\to& 真かどうか確認する方法がある \\ \\ &\to& 判定ができる \end{array}
主にこの「判定」を軸に定められています。
（判定できないものは性質と呼べない）
証明可能性 Provable
|| 証明できるって厳密にはどういうこと？
「正しい手順で導ける論理式である」こと
\begin{array}{ccc} 証明可能である & \left\{ \begin{array}{ll} 論理式である \\ \\ 正しい手順で得られる \end{array} \right. \end{array}
「正しい手順」の正確な表現は
\begin{array}{l} 正しい手順 & \left\{ \begin{array}{l} 材料は有限個の論理式 \\ \\ 妥当な推論規則を有限回適用 \end{array} \right. \end{array}
こんな感じでちょっとややこしいですが
（より正確にはもっと堅苦しい）
\begin{array}{lcl} 証明可能？な結論 & ← & 論理式で表現できるか？ \\ \\ 証明可能？な結論 & ← & 正しい手順で導けるか？ \end{array}
言ってること自体はかなり直感的だと思います。
（正しい文と正しい推論で得られるかどうか）
証明可能性の厳密な定義
「ある論理式 φ （結論）」が
「論理式の集合 Γ 」から「証明可能」であるとは
\begin{array}{l} φは証明可能 &\Longleftrightarrow & φは\left\{ \begin{array}{lcc} Γと論理公理に \\ \\ 妥当な推論規則を \\ \\ 有限回適用すれば得られる \end{array} \right. \end{array}
厳密にはこのように定義されています。
（ φ がただの文なら論理式かどうかの判定が必要）
公理は無限個
「 Γ 」と「論理公理」を中身に持つ『材料』は
\begin{array}{ccc} 論理公理 &\to& 生成可能な全ての公理 \\ \\ Γ &\to& 定義次第 \end{array}
定義上は「有限個」とは限らず
（実際には無限個の中から有限個だけしか使えない）
\begin{array}{ccc} 最小単位になる材料 & \left\{ \begin{array}{lcc} 論理公理 \\ \\ 非論理公理 \end{array} \right. \end{array}
このようになっていて
「論理公理」は『全ての推論で正しい公理』を意味し
「非論理公理」は『特定の体系の公理』を意味しています。
定理 Theorem
|| 証明された論理式に何か特別な名前を
「証明」から得られた『結論部分』のこと
\begin{array}{cc} 前提 &\overset{←から→が導かれる}{\Longrightarrow}& 結論 \\ \\ Γ&⊢&φ \end{array}
記号ではこのように表現され
（ ⊢ は『導かれる』という述語の記号表現）
\begin{array}{ccc} φはΓの定理 &\Longleftrightarrow& φはΓから証明可能 \end{array}
「証明可能」によって厳密に定義されています。
（ Γ⊢φ の結論部分 φ が定理と呼ばれる）
証明文
↑ の「 Γ⊢φ 」は『述語』であり
\begin{array}{ccc} Γ⊢φ &\Longleftrightarrow& φはΓの定理である \end{array}
「証明文」とはまた異なる概念であるため
（証明を表現する文を意味するのは証明文）
\begin{array}{ccc} 証明文 &\Longleftrightarrow&前提と結論を表現する論理式の有限列 \end{array}
「証明文」とはまた別で定義されています。
（定理であるはその文の状態を意味する）
要請 Request
|| 証明そのものに求められること
「証明はこうあるべき」という要求
\begin{array}{lclcl} 無矛盾性 & &矛盾を導けない && 数学 \\ \\ 完全性 &&主張の真偽は必ずどちらか && 証明論 \\ \\ 健全性 &&導けるものはすべて真 && 証明とモデル \\ \\ 決定可能性 &&定理か否か判別可 && モデル理論 \\ \\ 公理化可能性 && 公理が機械的に生成可 && モデル理論 \end{array}
「メタ的な要請」にはこういうのがあって
（数学全体には無矛盾性が求められている）
\begin{array}{lclcl} 完全性 &&主張の真偽は必ずどちらか && 証明論 \\ \\ 健全性 &&導けるものはすべて真 && 証明とモデル \end{array}
「証明」にはこのような性質が求められています。
（これを満たさないものは証明とは言えない）
完全性 Completeness
|| 正しいならなんで正しいか説明できるはず
「正しい」なら「証明できる」っていう性質
\begin{array}{c} 正しいと感じる && {}&& 証明可能である \\ \\ Γ⊨A&&⇒&&Γ⊢A \end{array}
「明らかに正しそうな命題」（懸賞問題など）には
「必ずそれを証明する文が存在する」って話で
\begin{array}{ccc} 正しい &\to& 証明できるはず \end{array}
「証明」という手順には必ずこれが要求されます。
（一階述語論理の範囲では満たされる）
健全性 Soundness
|| 証明できるなら正しいと感じるはず
「証明できる」ならそいつは「正しいはず」
\begin{array}{c} Γ⊨A&&⇐&&Γ⊢A \end{array}
「正しいもの」を「正しい手順」で積み上げるなら
「正しいものができあがるはず」という性質で
\begin{array}{ccc} 変な公理 &\overset{正しい手順の証明}{\longrightarrow}& 変な定理 && × \end{array}
これを求めるから「おかしな公理」を排除できます。
（変な結論から前提の見直しに繋がったりする）
完全性と健全性の両立
「健全性」を意識しながら前提を整理すると
\begin{array}{c} Γ⊨A&&\Longleftrightarrow&&Γ⊢A \end{array}
「完全性」と「健全性」は自然と一致し
（完全性は確実に満たされるわけではない）
\begin{array}{ccc} 一階述語論理 &\Longrightarrow& \Bigl( Γ⊨A\Longleftrightarrow Γ⊢A \Bigr) \end{array}
現代数学ではその状態が基礎になっています。
（一致するシンプルな最大範囲が一階述語論理）
形式的証明 Formal Proof
|| 証明の厳密な意味
「手順が確立されてる証明」のこと
\begin{array}{lcc}\varphi_i&∈&\mathrm{Axiom} && 論理公理 \\ \\ φ_j&∈&Γ && 前提集合 \end{array}
「形式的証明（厳密な意味での証明）」は
\begin{array}{ccc} φ_1,φ_2,...,φ_k,...,φ_n &\in& \mathrm{WFF} \end{array}
「論理式 φ_k 」によって厳密に定義されていて
（この論理式の有限個の列から証明文は出力される）
\begin{array}{ccc} \mathrm{MP} && P,P\to Q &\Longrightarrow& Q \end{array}
これらを正当化する『関係』として
（ \mathrm{MP} は3変数の関係として定義されている）
\begin{array}{cccc} (P,P\to Q,Q)&∈&\mathrm{MP} && \mathrm{Modus \,\, Ponens} \\ \\ (\varphi_i,\varphi_j,\varphi_k)&∈&\mathrm{MP} \\ \\ \\ (A,\forall x \,\, A)&∈&\mathrm{GEN} && 全称化 \\ \\ (\varphi_i,\varphi_k)&∈&\mathrm{GEN} \end{array}
これらはこのように定められており
（論理公理と論理式の有限列を入力とし出力 Q がある）
\begin{array}{ccc} φ_n &=& φ && 結論 \end{array}
『結論部分』は「証明文の最後」に来ます。
（これにより証明文の中身が厳密に定義される）
証明文であることの確認順序
これはちょっとややこしいんですが
\begin{array}{ccc} 直感的証明文 &\to& 形式的証明文 \end{array}
大きな型としてはこのようになっています。
（つまり確認は形式化という翻訳作業になる）
\begin{array}{ccc} 入力 && 出力 \\ \\ \left( \begin{array}{lcc} 論理公理 & \mathrm{Axioms} \\ \\ 論理式の有限列 & Γ \\ \\ 妥当な推論規則 & \mathrm{MP},\mathrm{GEN} \end{array} \right) &\to& 形式的証明文 \end{array}
ここで出てくるこの形は
\begin{array}{ccc} 直感的証明 &\overset{入力側の材料で翻訳}{\longrightarrow}& 形式表現に寄る \\ \\ &\overset{入力側の材料で翻訳}{\longrightarrow}& 形式表現に寄る \\ \\ &\vdots \\ \\ &\overset{入力側の材料で翻訳}{\longrightarrow}& 形式的証明 \end{array}
『翻訳の確認』で必要になるもので
\begin{array}{ccc} 直感的証明文 &\overset{入力側の材料で翻訳}{\longrightarrow}& 形式的証明文 \end{array}
基本的な確認手順は
「証明文（直感的）からの逆算」になります。
（ ↑ は「形式的証明である」の述語の要件）
真偽判定の段階と理論
これもちょっとややこしい話ですが
\begin{array}{ccc} 数理モデル & \left\{ \begin{array}{l} 文が存在するか真偽が分かる \\ \\ 論理式の列かどうか真偽が分かる \\ \\ 構文規則に則っているか真偽が分かる \\ \\ 推論規則が正しく適用されたか分かる \end{array} \right. \end{array}
これらの位置付けは
「超数学レベルの暗黙の前提」になります。
（こういった前提は明らかであるため省略する）
その上での「形式的証明である」の判定は
\begin{array}{ccc} 理論 &\to& 要請的定義 \left\{ \begin{array}{lcc} 論理式はこういうもの \\ \\ 有限列とはこういうこと \\ \\ 論理公理はこういうもの \\ \\ 妥当な推論規則はこんな感じ \end{array} \right. \end{array}
『理論』の定義段階で定義されていて
\begin{array}{lcl} 数理モデル段階 && 明らかな前提 && メタレベル \\ \\ 理論の定義段階 && 記号操作のチェック && 構文レベル \\ \\ 局所モデル段階 && 記号の意味が定まる && 意味レベル \end{array}
『翻訳される証明文』に「必要な公理」を集めた
「局所的なモデル」を定義する前の段階に置かれています。
（理論を解釈することでモデルは定義される）
理論の要請的定義
これらは各々が独立して定義されているので
\begin{array}{lcl} 有限列 && カウントした個数で判断 \\ \\ 論理式 && 項とか変数とか関数とか \\ \\ 論理公理 && 明らかに真 \\ \\ 推論規則 && 洗練すると\mathrm{MP}と\mathrm{GEN}のみ \end{array}
別々の記事でそれぞれ解説しようと思います。