|| 人間がなんかを推測するときの考え方
この領域では主に『論証』についての話をします。
なので『論証』についての知識が必要です。
スポンサーリンク
目次
・証明「論証を使って正しいってことを示すこと」
証明可能性「証明できるかどうかっていう性質」
公理系「公理を元にしていろいろ作れるシステム」
・形式的証明「妥当な決まりだけで証明するやり方」
定理「公理と定義と妥当な推論から正しいと分かるもの」
・主要な性質
完全性「正しいなら証明できるという性質」
健全性「証明できるなら正しいという性質」
端的に言うなら、
「論証」を「形式的」にする。
「あやふやな部分」を全てカットして、
『正しいと分かる部分だけ』にする。
これが証明論の感覚です。
まあなので『統語論・構文論 Syntax』的な感覚が強く、
自然言語の自由度は取り除かれていて、
『証明』の「手順」は全て一定に。
紛れというものが一切生じない状態にされ、
全て「演繹」によって導けるよう整備されています。
ちなみに『統語論』ですが、
これは要は「一定のやり方（形式・決まり）」のことで、
\begin{array}{llllll} \displaystyle \mathrm{and}&かつ&それに &&\to&& ∧ \\ \\ \mathrm{or}&または&もしくは &&\to&& ∨ \end{array}
まあつまりはこんな感じのやつですね。
ただの用語なので覚えるしかないです。
証明 Proof
|| なんか割と使われる言葉
「妥当」な「論証」のこと。
「形式」的であることも条件の一つにあります。
まあ要するに「正しい推測のやり方」みたいなもので、
「公理・定義」「妥当な推論規則」→「定理」
こんな感じの手順のことを証明と言います。
大雑把な区分
「証明」には、
「形式的証明」「非形式的証明」っていう区分があります。
『形式的証明』というのは、
要は「機械的に確認できる証明」のことで、
いわゆる「証明が正しい」とされる根拠はこれ。
まあなので、この形式的証明に分解できない場合、
その証明は「正しいかどうかわからない」となるか、
「証明として不十分」とされます。
これに対し『非形式的証明』は、
要は「見慣れた証明」のことで、
なんとなくの形式で
それっぽく文章にして、好きに書いてる。
こういう「学校で扱ってきたような証明」
あるいは「人間にとって分かりやすい証明」を
『非形式的証明』と言います。
ちなみにこれは「形式的証明に翻訳できる」なら
『正しい証明』ということになるので、
「正しくない証明」というわけではありません。
ただ、学校で扱うような証明は基本的に不十分です。
「省かれ過ぎた前提」「証明されたとする根拠」など
抜けがあり過ぎるので、
解答の根拠は教科書的なものになります。
厳密に正しいかどうかは考慮されません。
証明可能性 Provable
|| 証明できるっていうのはこういうこと
読んだまま「証明」が「可能」かについて。
記述できる上で確認をするわけですから、
その「文の長さが『有限』である」こととか
「決まったルールの文である」ことなんかが条件に来ます。
でまあそんな感じなので、
これをちゃんと説明するためには
特に「論理公理」は知らないと分かりにくいです。
「推論規則」は字面でなんとなく分かりますが、
論理公理は何を指してるのかよく分かんないですし。
一応ざっと解説しておくと、
「直感的に正しい論理式」が『論理公理』
「推論をする上での規則」が『推論規則』です。
これらは「証明可能性の定義」に含まれるので、
覚えてないと証明を厳密に理解することができません。
証明可能性の定義
「ある論理式 φ （結論）」が、
「論理式の集合 Γ （証明で使う文）」から「証明可能」である。
これの意味は↓のように定義されています。
「 Γ の論理式」と「論理公理」に、
「推論規則」を『有限』回数だけ適用すれば、
「論理式 φ 」が得られる。
なんのこっちゃ分からんかもしれませんが、
要は「定理が得られる」って言ってる感じで、
↑のはその厳密な言い回しです。
公理系 Axiomatic System
|| 公理が基盤にあるシステム
「公理」を元にした「システム・構造」のこと。
『公理で全部説明できる』ように作られていて、
基本的に、↓みたいな構造を持っています。
・記号（アルファベットとか数字）
・公理（なにがなんでも正しいってことにする仮定）
・代入規則（変数に定数・関数をぶち込む時の決まり）
・推論規則（公理から別の論理式を導く時の決まり）
こういった構造を持つやつを、
総称して「公理系」と言います。
具体的には、
「ちゃんとした学問」
例えば「数学」「科学」やらがそうで、
「まともな学問」と呼べるものは
基本的にこれだと思ってればだいたい合ってます。
あんま見る単語じゃありませんが、
証明論の説明でたまに見るので覚えときましょう。
形式的証明 Formal Proof
|| 証明の厳密な意味
「手順が確立されてる証明」のこと。
要求されることが「有限」と密接に関わっているので、
こいつは「再帰理論」にずぶずぶです。
首くらいまでは浸かってるかもしれません。
厳密な定義
「証明によって得られる論理式」を「 φ 」
『証明全体』を構成する「論理式の集合」を「 Γ 」
「形式的証明」を示す全文（論理式の塊）
これを分解した『有限列』を↓みたいに書くとして、
\begin{array}{llllll} \displaystyle φ_1,φ_2,…,φ_n \end{array}
ついでに「自然数」を表す記号も
↓のように書くと決めておきます。
\begin{array}{llllll} \displaystyle i,j,k,n∈\mathbb{N}&&i,j＜k≦n \end{array}
以上、「証明文全体」「一部」「文章のナンバー」
この辺りの記号の設定ができたので、
以下、本題である
『証明の定義』の話をしていこうと思います。
・証明文全体の定義
並んだ「論理式」の最後 φ_n が「証明文」
つまり「証明によって得られる論理式 \varphi 」である
\begin{array}{llllll} φ&=&φ_n \end{array}
以上、こんだけ。
「AでBでCで・・・」だから「こうである」
これの『 「AでBでCで・・・」だから「こうである」 』
これが「結論（証明文）」って言ってるだけで、
それ以上の意味は無いので難しく考えないでください。
・構成要素（論理式）の定義
ここがちょっとややこしいですが、
基本的には「証明全体 Γ 」の中身についての話で、
\begin{array}{llllll} \displaystyle φ_k&∈&Γ \end{array}
まずこの部分についてはこう。
「証明全体」の中に『証明文の一部』が含まれる
これの「推論規則を考えない部分」の宣言がまず１つ。
以下、残りは「推論規則」によるもので、
\begin{array}{rllllll} \displaystyle \varphi_k&∈&\mathrm{Axiom} \\ \\ (\varphi_i,\varphi_j,\varphi_k)&∈&\mathrm{MP} \\ \\ (\varphi_i,\varphi_k)&∈&\mathrm{GEN} \end{array}
最も代表的な「一階述語論理」の場合では
まあだいたいこんな感じに定義されてますね。
基本、証明と言えばこれだと思ってOKです。
\begin{array}{rll} \displaystyle \varphi_k&∈&\mathrm{Axiom} \\ \\ \\ (\varphi_i,\cdots,\varphi_k)&∈&\mathrm{Inference \,\, Rule}_1 \\ \\ (\varphi_i,\varphi_j,\cdots,\varphi_k)&∈&\mathrm{Inference \,\, Rule}_2 \\ \\ &\vdots& \\ \\ (\varphi_i,\varphi_j,\cdots,\varphi_k)&∈&\mathrm{Inference \,\, Rule}_n \end{array}
より広い範囲を含むとするなら
まあこんな感じに書くべきなんでしょうけど。
補足
「 \mathrm{Axiom} 」は「論理公理」
「 \mathrm{MP} 」は「 \mathrm{Modus \,\, Ponens} 演繹」
「 \mathrm{GEN} 」は「 \mathrm{Generalization} 一般化（全称化）」
「 \mathrm{MP} 」「 \mathrm{GEN} 」の辺りが意味わからんと思いますが、
ちょっと長くなるので詳細は「推論規則」の記事で。
定理 Theorem
|| 証明文（論理式）になんか特別な名前を
「証明全体」から得られた『証明文』のこと。
\begin{array}{llllll} \displaystyle Γ&⊢&φ \end{array}
記号ではこんな感じで、
「 φ が Γ から証明可能である」
「 φ が Γ の定理である」
これにはこの２つの意味があります。
まあつまり、
「 \varphi が証明可能である」とは、
「 \varphi が定理である」ということと同義です。
完全性 Completeness
|| 正しいんならなんで正しいか説明できるはず
「正しい」んなら「証明できる」っていう性質のこと。
\begin{array}{lllllll} \displaystyle Γ⊨A&&⇒&&Γ⊢A \end{array}
これが保証されるってことは、
「明らかに正しそうな命題」（懸賞問題など）には
「必ずそれを証明する文が存在する」ってことで、
まあつまり、あらゆる未解決問題には、
「必ず証明文が存在する」んですよ。
この「完全性」っていう性質が保証されている
その場合に限る話ではありますし、
それを発見できるかどうかは別問題なんですが。
\begin{array}{lllllll} \displaystyle Γ⊨A&&⇒&&Γ⊢A \end{array}
ちなみにこの記号の意味は、
「論理的主張が正しいなら定理だよ」
「正しいなら確実に説明できるよ」みたいな感じです。
健全性 Soundness
|| 健全って字面がなんか
「証明できる」ならそいつは「正しい」
\begin{array}{llllllll} Γ⊨A&&⇐&&Γ⊢A \end{array}
この当たり前に思える性質のことを
「健全性」と言います（完全性の逆）
まあつまり
「証明可能なら論理的主張は正しいよ」ってことで、
この性質が保証されている場合
『公理・定義・妥当な推論規則』から
「論理的主張」は必ず構成することができます（演繹）
言い換えるなら、
「正しいもの」を「正しい手順」で積み上げる
すると「正しいもの」ができあがる、って感じでしょうか。
完全性と健全性
「完全性」と「健全性」が満たされるとき、
\begin{array}{lllllllllllll} \displaystyle Γ⊨A&&≡&&Γ⊢A \end{array}
まあつまり「一階述語論理の範囲」のものは、
このような性質を満たします。
というか、これを満たすのは基本的にこれだけ。
だけ、というのは、
他のものも結局これに行き着く感じで、
例えば「データべース」「プログラミング言語」
この辺りはこの範囲に収まるよう作られています。
なので全て 0,1 で表現可能な上に、
入力 → 処理 → 出力 の過程を全て追跡することが可能です。
余談
不思議な話で、
全く違う「定義」のされ方をしたはずのものが、
なぜかまったく同じものとして見做すことができてしまう。
\begin{array}{llllll} \displaystyle Γ⊨A&&≡&&Γ⊢A \end{array}
この点、ちょっとすごくないですか？
「論理的主張」は感覚的なもの
「定理」は形式的なもの
まあつまり設計図が全く違うのに、
なぜか同じものが出来上がった、みたいな。
多少狙っていた感があるのは否めませんが、
この部分、なんかすごくないですか？
いやだって、ここに行き着けたのは、
「正しさの追求」をし続けたからで、
それまでは両者共に同じではなく、
ただ『そうすると人間にとって最も都合が良いから』
結果として『論理的主張と定理が同じと見做せる』ようになった
\begin{array}{llllll} \displaystyle Γ⊨A&&≡&&Γ⊢A \end{array}
つまりこの等式は意図的に作り出されたわけではなく
正しさの追求から「結果的に得られた成果」で、
両者の一致は偶然なんです。
はい。とまあそんな感じなんですが、
どうでしょう、面白いと思ってもらえましたか？
少しでも面白いと思ってもらえたのなら
この記事を頑張って書いた甲斐があったって感じですね。
実はわりと「偶然」に満ちている
数学はそんな不思議ワールドなんだよ
この辺りのことが少しでも実感できたのであれば
筆者としては嬉しい限りです。
「一階述語論理」
『健全性定理』『完全性定理』の『証明』は別記事で