共通参考文献はこちら
前回の続き
さて妥当と考えられる推論法則で、あらゆる推論を行うのに十分と考えられる推論法則一式(one set !!)の例として、ゲンツェン流の自然推論または自然演繹と呼ばれる体系の推論規則を挙げます。これらの推論規則は○○導入(Induction)および○○除去(Elimination)と呼ばれる対として整理されていますが[w-2]、Ref-4では○○Iおよび○○Eと表記しているだけでした。なお記号「⊥」は「矛盾」を意味します。高崎金久[京都大学]のサイトの解説がわかりやすいでしょう。
→導入) [A |--- B] |--- A→B
→除去) A、A→B |--- B 別名:三段論法、正格法(modus ponens)
∧導入) A、B |--- A∧B 別名:∧の定義
∧除去-a) A∧B |--- A
∧除去-b) A∧B |--- B
∨導入-a) A |--- A∨B 別名:∨の定義(a,b合わせて)
∨導入-b) B |--- A∨B 別名:∨の定義(a,b合わせて)
∨除去) A∨B、[A |--- C]、[B |--- C] |--- C 別名:場合分け論法、選言三段論法
¬導入) [A |--- ⊥] |--- ¬A
¬除去) A、¬A |--- ⊥ 別名:矛盾の定義
⊥、矛盾) ⊥ |--- A
排中律) |--- A∨¬A
以下、xは束縛された変数、aは束縛されていない自由変数、tは対象式
∀導入) A(a) |--- ∀xA(x) 別名:一般化[Ref-1 p169]
∀除去) ∀xA(x) |--- A(t) 別名:変数の特殊化[Ref-1 p168]
∃導入) A(t) |--- ∃xA(x)
∃除去) ∃xA(x)、[A(a) |--- C] |--- C
ここで、導入と分類された推論規則は、「証明列における事実から論理記号を定義している」という見方もできます。除去は「基本的論理式から何が推論されるのかを示している」という見方もできます。すると「→導入」「→除去」「∧導入」「∧除去」「∨導入」の妥当性は、各論理記号の意味からして明らかでしょう。
前回述べたように「A |--- B」と「A→B」とは対応しますから、上記の推論規則は公理として表すこともできます。推論規則としては例えば→導入と→除去を残せば十分です。→導入があれば、ある推論法則(規則も含む)から対応する定理(公理も含む)が導けますし、→除去があれば、ある定理から対応する推論法則の成立がわかるからです。
また→導入と→除去のうち1つだけを残すこともできます。例えばヒルベルト流と呼ばれる体系では次の推論規則と公理を使います。
推論規則1)[→除去] A、A→B |--- B
推論規則2)[∀導入] A |--- ∀xA
命題公理1)[→導入] B→(A→B)
命題公理2) (A→(B→C))→((A→B)→(A→C)) 別名:→の分配法則
命題公理3) (¬B→¬A)→(A→B) 別名:対偶
述語公理1)[∀除去] ∀xF(x)→F(t)
述語公理2) ∀x(A→F(x))→(A→∀xF(x))
命題公理1が→導入の替わりになるのですが、それは次のようにわかります。
1) A ∵前提
2) A |--- B ∵前提
3) B |--- (A→B) ∵命題公理1と正格法から
4) A→B ∵1、3、正格法
こうしてヒルベルト流の体系でも、ある推論法則(規則も含む)から対応する定理(公理も含む)が導け、ある定理から対応する推論法則の成立が導けます。
ヒルベルト流の体系はゲンツェン流に比べると随分と数が少なく見えますが、その主な理由は∧,∨,∃,⊥を使っていない事です。実はこれらは→,¬,∀を使った論理式の略記記号と定義しています。
A∨B ≡ ¬A→B ≡ ¬B→A
A∧B ≡ ¬(A→¬B) ≡ ¬(B→¬A)
∃xA(x) ≡ ¬(∀x¬A(x))
⊥≡A∧¬A
実のところ∧と∨の後半は対偶になっています。そしてこの略記を使うということは、∧,∨,∃,を導入したうえで以下の公理を設定することと同じことです。
A∨B ⇔ ¬A→B
A∧B ⇔ ¬(A→¬B)
∃xA(x) ⇔ ¬(∀x¬A(x))
¬(A∧¬A)
つまり、ヒルベルト流とゲンツェン流とでは基本的な公理と推論規則の合計数は見た目ほどは違っていないということになります。
ゲンツェン流に戻って、∀除去と∃導入の対象項を示す変数tについては前回述べました。∀導入と∃除去には変数aが登場します。Ref-4の方式では束縛されていない自由変数と束縛されている自由変数とで別の種類の記号を使って両者を区別していて、このような表記になります。区別しないならば、aの替わりにyなどxと同種類の自由変数記号を使うことになるでしょう。ただ、束縛されているかいないかという違いが大事です。さて一見すると「A(a)が成立する」ことも「∀xA(x)が成立する」ことも同じことを意味するように見えますが、何か違いがあるのでしょうか?
A(a)は自由変数aに任意の対象を当てはめることができるものです。つまり「A(a)が成立する」ということは、「A(0)が成立する」「A(1)が成立する」・・・、ということを意味していると考えられます。すなわち「∀導入」は体系がω無矛盾[*1]だと言っている、とも言えるかも知れません。まあ常識的には、「A(0)が成立する」「A(1)が成立する」・・・、として全対象について「A(a)が成立する」という状況を記述するのが∀xA(x)の定義と考えられますね。
さてまたくどい解説をしますと、「∀導入」の前提である「A(a)[が成立する]」という命題は「任意の対象tを選んでaに代入すると、いつでもA(t)」という意味で、「∃導入」の前提である「A(t)[が成立する]」とは決定的に異なります。この違いを明確に示すのは、論理式だけでは無理ですね[*2]。論理式の記号の解説が必要です。
次に∃除去は、「任意の対象であるaについてA(a)→Cならば、∃xA(x)からCが推論できる」という意味になります。いくらA(a)→Cであっても、肝心のA(x)となる対象xが存在しなければ、Cは推論できないのです。
次回に続く
--------------------
*1 ゲーデルの定理-1.3- 第一不完全性定理と全てのカラス参照
*2 論理体系の解剖-1.1-のくどい解説も参照。
前回の続き
さて妥当と考えられる推論法則で、あらゆる推論を行うのに十分と考えられる推論法則一式(one set !!)の例として、ゲンツェン流の自然推論または自然演繹と呼ばれる体系の推論規則を挙げます。これらの推論規則は○○導入(Induction)および○○除去(Elimination)と呼ばれる対として整理されていますが[w-2]、Ref-4では○○Iおよび○○Eと表記しているだけでした。なお記号「⊥」は「矛盾」を意味します。高崎金久[京都大学]のサイトの解説がわかりやすいでしょう。
→導入) [A |--- B] |--- A→B
→除去) A、A→B |--- B 別名:三段論法、正格法(modus ponens)
∧導入) A、B |--- A∧B 別名:∧の定義
∧除去-a) A∧B |--- A
∧除去-b) A∧B |--- B
∨導入-a) A |--- A∨B 別名:∨の定義(a,b合わせて)
∨導入-b) B |--- A∨B 別名:∨の定義(a,b合わせて)
∨除去) A∨B、[A |--- C]、[B |--- C] |--- C 別名:場合分け論法、選言三段論法
¬導入) [A |--- ⊥] |--- ¬A
¬除去) A、¬A |--- ⊥ 別名:矛盾の定義
⊥、矛盾) ⊥ |--- A
排中律) |--- A∨¬A
以下、xは束縛された変数、aは束縛されていない自由変数、tは対象式
∀導入) A(a) |--- ∀xA(x) 別名:一般化[Ref-1 p169]
∀除去) ∀xA(x) |--- A(t) 別名:変数の特殊化[Ref-1 p168]
∃導入) A(t) |--- ∃xA(x)
∃除去) ∃xA(x)、[A(a) |--- C] |--- C
ここで、導入と分類された推論規則は、「証明列における事実から論理記号を定義している」という見方もできます。除去は「基本的論理式から何が推論されるのかを示している」という見方もできます。すると「→導入」「→除去」「∧導入」「∧除去」「∨導入」の妥当性は、各論理記号の意味からして明らかでしょう。
前回述べたように「A |--- B」と「A→B」とは対応しますから、上記の推論規則は公理として表すこともできます。推論規則としては例えば→導入と→除去を残せば十分です。→導入があれば、ある推論法則(規則も含む)から対応する定理(公理も含む)が導けますし、→除去があれば、ある定理から対応する推論法則の成立がわかるからです。
また→導入と→除去のうち1つだけを残すこともできます。例えばヒルベルト流と呼ばれる体系では次の推論規則と公理を使います。
推論規則1)[→除去] A、A→B |--- B
推論規則2)[∀導入] A |--- ∀xA
命題公理1)[→導入] B→(A→B)
命題公理2) (A→(B→C))→((A→B)→(A→C)) 別名:→の分配法則
命題公理3) (¬B→¬A)→(A→B) 別名:対偶
述語公理1)[∀除去] ∀xF(x)→F(t)
述語公理2) ∀x(A→F(x))→(A→∀xF(x))
命題公理1が→導入の替わりになるのですが、それは次のようにわかります。
1) A ∵前提
2) A |--- B ∵前提
3) B |--- (A→B) ∵命題公理1と正格法から
4) A→B ∵1、3、正格法
こうしてヒルベルト流の体系でも、ある推論法則(規則も含む)から対応する定理(公理も含む)が導け、ある定理から対応する推論法則の成立が導けます。
ヒルベルト流の体系はゲンツェン流に比べると随分と数が少なく見えますが、その主な理由は∧,∨,∃,⊥を使っていない事です。実はこれらは→,¬,∀を使った論理式の略記記号と定義しています。
A∨B ≡ ¬A→B ≡ ¬B→A
A∧B ≡ ¬(A→¬B) ≡ ¬(B→¬A)
∃xA(x) ≡ ¬(∀x¬A(x))
⊥≡A∧¬A
実のところ∧と∨の後半は対偶になっています。そしてこの略記を使うということは、∧,∨,∃,を導入したうえで以下の公理を設定することと同じことです。
A∨B ⇔ ¬A→B
A∧B ⇔ ¬(A→¬B)
∃xA(x) ⇔ ¬(∀x¬A(x))
¬(A∧¬A)
つまり、ヒルベルト流とゲンツェン流とでは基本的な公理と推論規則の合計数は見た目ほどは違っていないということになります。
ゲンツェン流に戻って、∀除去と∃導入の対象項を示す変数tについては前回述べました。∀導入と∃除去には変数aが登場します。Ref-4の方式では束縛されていない自由変数と束縛されている自由変数とで別の種類の記号を使って両者を区別していて、このような表記になります。区別しないならば、aの替わりにyなどxと同種類の自由変数記号を使うことになるでしょう。ただ、束縛されているかいないかという違いが大事です。さて一見すると「A(a)が成立する」ことも「∀xA(x)が成立する」ことも同じことを意味するように見えますが、何か違いがあるのでしょうか?
A(a)は自由変数aに任意の対象を当てはめることができるものです。つまり「A(a)が成立する」ということは、「A(0)が成立する」「A(1)が成立する」・・・、ということを意味していると考えられます。すなわち「∀導入」は体系がω無矛盾[*1]だと言っている、とも言えるかも知れません。まあ常識的には、「A(0)が成立する」「A(1)が成立する」・・・、として全対象について「A(a)が成立する」という状況を記述するのが∀xA(x)の定義と考えられますね。
さてまたくどい解説をしますと、「∀導入」の前提である「A(a)[が成立する]」という命題は「任意の対象tを選んでaに代入すると、いつでもA(t)」という意味で、「∃導入」の前提である「A(t)[が成立する]」とは決定的に異なります。この違いを明確に示すのは、論理式だけでは無理ですね[*2]。論理式の記号の解説が必要です。
次に∃除去は、「任意の対象であるaについてA(a)→Cならば、∃xA(x)からCが推論できる」という意味になります。いくらA(a)→Cであっても、肝心のA(x)となる対象xが存在しなければ、Cは推論できないのです。
次回に続く
--------------------
*1 ゲーデルの定理-1.3- 第一不完全性定理と全てのカラス参照
*2 論理体系の解剖-1.1-のくどい解説も参照。
※コメント投稿者のブログIDはブログ作成者のみに通知されます