証明論 Proof Theory


|| 人間がなんかを推測するときの考え方

この領域では主に『論証』についていろいろします。

なので『論証』についての知識が必要です。

スポンサーリンク





目次


証明「論証を使って正しいってことを示すこと」

   証明可能性「証明できるかどうかっていう性質」

   公理系「公理を元にしていろいろ作れるシステム」


形式的証明「妥当な決まりだけで証明するやり方」

   定理「公理と定義と妥当な推論から正しいと分かるもの」


主要な性質

   完全性「正しいなら証明できるという性質」

   健全性「証明できるなら正しいという性質」








端的に言うと「論証」を「形式的」にする感じです。

「あやふやな部分」を全てカットした感じになります。

なので『統語論・構文論 Syntax』的な感覚が強い分野です。




『統語論』っていうのは、要は「形式(決まり)」ですね。

数学ですから「決まったやり方」で『証明』したいわけです。

なので「材料」「やり方」なんかを全部決めちゃってます。






証明 Proof


|| なんか割と使われる言葉

これは「妥当」な「論証」のことです。

形式」的であることも条件の一つにあります。



要するに「正しい推測のやり方」みたいなもの。




そんな「証明」には、

形式的証明」と「形式的証明」という区分があります。




形式的証明』というのは、

要は「機械的」に確認できる「証明」のことを指します。

つまるところ「数学で扱う証明」のことですね。




形式的証明』は「見慣れた証明」のことです。

なんとなく形式はありますが、文章にして好きに書いてる感じ。

これを「形式的証明に翻訳できる」なら『正しい証明』になります。






ちなみに学校で見られる「証明」は「形式的証明」です。

論証の知識も無いまま扱うので、土台はふわふわしてます。

正解したいなら、ともかく言われた通りにしとけばいい感じ。






感覚はなんとなく分かったかと思うので、

とりあえず内訳(具体的なもの)を見ていきましょうか。






証明可能性 Provable


|| 意訳すると、証明できんのか?って感じ

読んだままですね。「証明」が「可能」かについてです。

記述や確認をしますから『有限』であることが条件にあります。




これを説明するためには、

論理公理」と「推論規則」を知らなければなりません。




論理公理」は知らないと分かりにくいです。(別記事)

けっこう多いので、覚えるのに苦労します。

なので「直感的に正しい論理式」くらいに思っておきましょう。



推論規則」も別記事で扱います。(結構多い)

これはそのまま「推論」をする上での「規則」と思ってOKです。

「~なら~だ」をする上でこれはOK、みたいな。




これらを踏まえた上で、厳密な定義について見てみます。






証明可能性の定義


「ある論理式 φ (結論)」が、

「論理式の集合 Γ (証明で使う文)」から「証明可能」である。





この意味は↓になります。



Γ の論理式」と「論理公理」に、

「推論規則」を『有限』回数だけ適用すれば、

「論理式 φ 」が得られる。






より厳密な定義を示すには「推論規則」の知識が必要です。

厳密なものは↓の「形式的証明」で扱います。







公理系 Axiomatic System


|| 公理が基盤にあるシステム

ざっと言うと「公理」を元にした「システム」です。

「公理」からなにもかも導ける感じ。




構造は↓みたいな感じ。



・記号(アルファベットとか数字)

公理(なにがなんでも正しいやつ)

代入規則(変数に、定数やら変数やら関数をぶち込むときの決まり)

推論規則(公理から別の論理式を導くときの決まり)



これを総称して「公理系」と言います。

「公理で全部片づけたいシステム」って覚えときゃ良いです。

あんま見る単語じゃないんで、意味さえ分かってれば。







形式的証明 Formal Proof


|| 数学でいうところの証明はこやつ

要はそのまま「確実に正しい証明」のことです。



この性質上、こいつは「再帰理論」にずぶずぶです。

首くらいまでは浸かってるかもしれません。




ともかく厳密な定義について見ていきましょう。

例によって、いつもの「再帰的定義」です。



ともかく最初に「証明によって得られる論理式」を「 φ 」とします。

そして『証明全体』となる「論理式の集合」を「 Γ 」としましょうか。



次に「形式的証明」を示す全文、つまり「論理式」の塊を用意します。

それを並べたやつは「 φ_1,φ_2,...,φ_n 」です。



それと一応これも定義しておきます。

「自然数だ」ってことと「大小関係」です。

あんま気にしなくて良いですが、念のため。

i,j,k,n∈\mathbb{N},\,\,\,i,j<k≦n




ここまで、用意したものを要約すると、

「結論」と「前提」と「文章のナンバー」です。

結論と前提を一括りにすれば「論理式」になります。





いずれにせよ「証明」とは「論理式の列(文章)」ですから、

ぜんぶ『「論理式いっぱい」だったら「論理式」ですよ』

みたいな形式になります。



これを実現するのが↓の定義になります。

用意したものも、ここで使うための単なる記号です。






結論部分の定義


これは宣言です。↓を宣言してます。

並んだ「論理式」の最後が「得た論理式」だよ。

こんだけです。



そんなわけで、その最後にある「論理式」が、

「証明によって得られる論理式」と同じだって宣言します。



φ=φ_n



「結論」部分の定義はこれで終わり。






前提部分の定義


さて、というわけでここからは「前提」についての話になります。

Γ 」の中身についての話です。

これは大きく分けて4つ。ちょっと多いですね。






1つは「証明」となる「論理式の塊」がそこに属してること。



φ_k∈Γ



単なる帰属関係の確認です。

これもまあ、当然の話ですね。






次に「論理式」はどういうものなのか。(規則)

これが3つに分けられます。ちょっと多いですが、単純。



1つは「 φ_k 」が「論理公理」だということ。

1つは「 φ_k 」が「 MP 導出によるもの」だということ。(演繹)

1つは「 φ_k 」が「 GEN 導出によるもの」だということ。(量化)




これだけです。

以上が「形式的証明」の厳密な定義となります。

MP 」と「 GEN 」の詳細は「推論規則」で。






定理 Theorem


|| 証明されたものになんか特別な名前を

これはまあ「証明全体」のことですね。

つまりは「証明可能」の元に存在する「証明」そのもののこと。




φ が、 Γ から証明可能である」と、

φ が、 Γ の定理である」は同じ意味です。




形式的には、こんな感じで書かれます。



Γ⊢φ



「前提」と「結論」のセットです。

「前提が成立」して、初めて「結論」は正しくなります。







完全性 Completeness


|| 正しいんなら、説明できるはず

「正しい」んなら「証明できる」んだぜ!って性質のことです。



これが保証されているということは、

「明らかに正しそうな命題」(ミレニアム懸賞問題など)には、

「必ずそれを証明する文が存在する」と言えるわけです。




形式的には、前提を「 Γ 」結論を「 A 」とすると、

[\,Γ⊨A\,]\,⇒\,[\,Γ⊢A\,] 」と書き表されます。

意味は「論理的主張が正しいなら、定理だよ!」です。



意訳は「正しいなら確実に説明できる」って感じ。

ただし懸賞問題なんかは誰も説明できてません。






健全性 Soundness


|| 健全って字面がなんか

「証明できる」んなら、そいつは「正しい」んだよ!

という感じの、当たり前に思える性質のこと(完全性の逆)




要は「証明可能なら、その論理的主張は正しいよ!」ってことです。

形式的には「 [\,Γ⊢A\,]\,⇒\,[\,Γ⊨A\,] 」と表せます。




要は「正しいことが説明できちゃうなら、そりゃ正しいよ」って感じ。

より厳密には「正しい」ものを『演繹』でだしたものは正しい、です。

正しいものを正しい手順で積み上げたら、正しいものができる感じ。






完全性と健全性


つまるところ「完全性」と「健全性」が満たされるとき、

[\,Γ⊨A\,]\,≡\,[\,Γ⊢A\,] 』となるわけです。




数学の言語である「一階述語論理」は、これ満たします。

そしてこれを満たすものは、基本的にはこれだけです。



だけ、というのは、他のものも結局これになることを言いたい感じ。

例えばプログラミング言語なんかはこれを参考に作られてます。




同様に形式体系の全ては、結局これに行き着きます。

というか、これが正しさを保証してるんです。

つまり『形式体系』の全ては「一階述語論理」の一部になります。




そしてその時だけ、

「正しい論理的主張」と「定理」が同じものだと見做せるわけです。




不思議な話で、全く違う「定義」のされ方をしたはずのものが、

なぜか、まったく同じものだと「証明」されてしまいます。

(「論理的主張」は感覚的なもので、「定理」は形式的なもの)




設計図が全く違うのに、同じものが出来上がった、みたいな。

多少狙ったとはいえ、なんかすごくないですか?



「正しさの追求」の成果なわけですよ、これは。

つまりただ「正しさ」を追い求めていたら、

『論理的主張と定理が同じと見做せる』ってなったわけです。



より厳密には「正しいことが確認できる」なら、

という前提が来るわけですが。




ともかく、これを面白いと思ってもらえたら嬉しいです。

数学はわりと不思議ワールドなんだということが伝われば。






最後に「一階述語論理」での、

健全性定理』『完全性定理』の『証明』は別項目で。