論理体系の解剖-1.3- ゲンツェン流とヒルベルト流

共通参考文献はこちら
前回の続き

　さて妥当と考えられる推論法則で、あらゆる推論を行うのに十分と考えられる推論法則一式(one set !!)の例として、ゲンツェン流の自然推論または自然演繹と呼ばれる体系の推論規則を挙げます。これらの推論規則は○○導入(Induction)および○○除去(Elimination)と呼ばれる対として整理されていますが[w-2]、Ref-4では○○Ｉおよび○○Ｅと表記しているだけでした。なお記号「⊥」は「矛盾」を意味します。高崎金久[京都大学]のサイトの解説がわかりやすいでしょう。

　→導入)　　[Ａ |--- Ｂ] |--- Ａ→Ｂ
　→除去)　　Ａ、Ａ→Ｂ |--- Ｂ　　　別名：三段論法、正格法(modus ponens)

　∧導入)　　Ａ、Ｂ |--- Ａ∧Ｂ　　　別名：∧の定義
　∧除去-a)　Ａ∧Ｂ |--- Ａ
　∧除去-b)　Ａ∧Ｂ |--- Ｂ

　∨導入-a)　Ａ |--- Ａ∨Ｂ　　　別名：∨の定義(a,b合わせて)
　∨導入-b)　Ｂ |--- Ａ∨Ｂ　　　別名：∨の定義(a,b合わせて)
　∨除去)　　Ａ∨Ｂ、[Ａ |--- Ｃ]、[Ｂ |--- Ｃ] |--- Ｃ　　別名：場合分け論法、選言三段論法

　￢導入)　　[Ａ |--- ⊥] |--- ￢Ａ
　￢除去)　　Ａ、￢Ａ |--- ⊥　　　別名：矛盾の定義
　⊥、矛盾)　⊥ |--- Ａ
　排中律) 　 |--- Ａ∨￢Ａ　

　　以下、ｘは束縛された変数、ａは束縛されていない自由変数、ｔは対象式
　∀導入)　　Ａ(ａ) |--- ∀ｘＡ(ｘ)　　　別名：一般化[Ref-1 p169]
　∀除去)　　∀ｘＡ(ｘ) |--- Ａ(ｔ)　　　別名：変数の特殊化[Ref-1 p168]
　∃導入)　　Ａ(ｔ) |--- ∃ｘＡ(ｘ)
　∃除去)　　∃ｘＡ(ｘ)、[Ａ(ａ) |--- Ｃ] |--- Ｃ

　ここで、導入と分類された推論規則は、「証明列における事実から論理記号を定義している」という見方もできます。除去は「基本的論理式から何が推論されるのかを示している」という見方もできます。すると「→導入」「→除去」「∧導入」「∧除去」「∨導入」の妥当性は、各論理記号の意味からして明らかでしょう。

　前回述べたように「Ａ |--- Ｂ」と「Ａ→Ｂ」とは対応しますから、上記の推論規則は公理として表すこともできます。推論規則としては例えば→導入と→除去を残せば十分です。→導入があれば、ある推論法則(規則も含む)から対応する定理(公理も含む)が導けますし、→除去があれば、ある定理から対応する推論法則の成立がわかるからです。

　また→導入と→除去のうち１つだけを残すこともできます。例えばヒルベルト流と呼ばれる体系では次の推論規則と公理を使います。

　推論規則１)[→除去]　Ａ、Ａ→Ｂ |--- Ｂ　　　
　推論規則２)[∀導入]　Ａ |--- ∀ｘＡ　　　

　命題公理１)[→導入]　Ｂ→(Ａ→Ｂ)　
　命題公理２)　(Ａ→(Ｂ→Ｃ))→((Ａ→Ｂ)→(Ａ→Ｃ))　　別名：→の分配法則
　命題公理３)　(￢Ｂ→￢Ａ)→(Ａ→Ｂ)　　別名：対偶
　述語公理１)[∀除去]　∀ｘＦ(ｘ)→Ｆ(ｔ)
　述語公理２)　∀ｘ(Ａ→Ｆ(ｘ))→(Ａ→∀ｘＦ(ｘ))

　命題公理１が→導入の替わりになるのですが、それは次のようにわかります。
　1) Ａ 　　　∵前提
　2) Ａ |--- Ｂ　　　　∵前提
　3) Ｂ |--- (Ａ→Ｂ)　∵命題公理１と正格法から
　4) Ａ→Ｂ　　∵1、3、正格法

　こうしてヒルベルト流の体系でも、ある推論法則(規則も含む)から対応する定理(公理も含む)が導け、ある定理から対応する推論法則の成立が導けます。

　ヒルベルト流の体系はゲンツェン流に比べると随分と数が少なく見えますが、その主な理由は∧,∨,∃,⊥を使っていない事です。実はこれらは→,￢,∀を使った論理式の略記記号と定義しています。
　　　Ａ∨Ｂ ≡ ￢Ａ→Ｂ ≡ ￢Ｂ→Ａ
　　　Ａ∧Ｂ ≡ ￢(Ａ→￢Ｂ) ≡ ￢(Ｂ→￢Ａ)
　　　∃ｘＡ(ｘ) ≡ ￢(∀ｘ￢Ａ(ｘ))
　　　⊥≡Ａ∧￢Ａ

　実のところ∧と∨の後半は対偶になっています。そしてこの略記を使うということは、∧,∨,∃,を導入したうえで以下の公理を設定することと同じことです。
　　　Ａ∨Ｂ ⇔ ￢Ａ→Ｂ
　　　Ａ∧Ｂ ⇔ ￢(Ａ→￢Ｂ)
　　　∃ｘＡ(ｘ) ⇔ ￢(∀ｘ￢Ａ(ｘ))
　　　￢(Ａ∧￢Ａ)

　つまり、ヒルベルト流とゲンツェン流とでは基本的な公理と推論規則の合計数は見た目ほどは違っていないということになります。

　ゲンツェン流に戻って、∀除去と∃導入の対象項を示す変数ｔについては前回述べました。∀導入と∃除去には変数ａが登場します。Ref-4の方式では束縛されていない自由変数と束縛されている自由変数とで別の種類の記号を使って両者を区別していて、このような表記になります。区別しないならば、ａの替わりにｙなどｘと同種類の自由変数記号を使うことになるでしょう。ただ、束縛されているかいないかという違いが大事です。さて一見すると「Ａ(ａ)が成立する」ことも「∀ｘＡ(ｘ)が成立する」ことも同じことを意味するように見えますが、何か違いがあるのでしょうか？

　Ａ(ａ)は自由変数ａに任意の対象を当てはめることができるものです。つまり「Ａ(ａ)が成立する」ということは、「Ａ(０)が成立する」「Ａ(１)が成立する」・・・、ということを意味していると考えられます。すなわち「∀導入」は体系がω無矛盾[*1]だと言っている、とも言えるかも知れません。まあ常識的には、「Ａ(０)が成立する」「Ａ(１)が成立する」・・・、として全対象について「Ａ(ａ)が成立する」という状況を記述するのが∀ｘＡ(ｘ)の定義と考えられますね。

　さてまたくどい解説をしますと、「∀導入」の前提である「Ａ(ａ)[が成立する]」という命題は「任意の対象ｔを選んでａに代入すると、いつでもＡ(ｔ)」という意味で、「∃導入」の前提である「Ａ(ｔ)[が成立する]」とは決定的に異なります。この違いを明確に示すのは、論理式だけでは無理ですね[*2]。論理式の記号の解説が必要です。

　次に∃除去は、「任意の対象であるａについてＡ(ａ)→Ｃならば、∃ｘＡ(ｘ)からＣが推論できる」という意味になります。いくらＡ(ａ)→Ｃであっても、肝心のＡ(ｘ)となる対象ｘが存在しなければ、Ｃは推論できないのです。

次回に続く

－－－－－－－－－－－－－－－－－－－－
*1 ゲーデルの定理-1.3- 第一不完全性定理と全てのカラス参照
*2 論理体系の解剖-1.1-のくどい解説も参照。