共通参考文献はこちら
前回の続き
論理体系には公理と定理、および推論規則と推論法則が存在します。公理は、無条件に真と決めた論理式です。定理は、公理からの証明列の結論として導かれる論理式です。推論法則は、論理式の並びである式列が正しい証明列になっていることを決める規則です。つまり正しい証明列とはそれを構成するすべての論理式が次のどれかに相当するものです。
・公理である。
・式列の中で前にある論理式のいくつかから推論法則により導かれている
推論規則は、無条件に成立すると決めた推論法則であり、推論規則からメタ数学的に成立が証明された推論法則だけを特に推論法則と呼んで、推論規則と区別する場合もあります。いわば推論規則は公理に当たり、推論法則は定理に当たります。
推論法則を記述するにはいくつかの方法があります。例として「→除去」と呼ばれる推論規則を取ります。これは、正格法(modus ponens)または単に三段論法と呼ばれる最も基本的な推論法則です。ヒルベルト流という体系では命題論理での推論規則としてはこれひとつだけを採用しているくらいに基本的なものです。
言語表現1) AとA→Bとから、Bが推論できる。
言語表現2) AでありA→Bであるならば、Bが推論できる。
推論図式[Ref-4 p50(3章)]
A A→B
-------
B
線形表現{推論形式[Ref-4 p50(3章)]} A、A→B |--- B
個人的には推論図式がわかりやすいとは思うのですが、行が増えてしまうので今後は線形表現で記することにします。この表現は細かい部分、例えば記号「|---」などでは本記事独自である点を御了解ください。ということで、前回の独断により選んだ妥当な推論法則もこの表記を使っています。
また反射律や排中律のように論理式(公理)として記述してあるものも、実は、「無前提でこれらの公理が推論できる」という推論法則として記述することができます。
|--- A→A 反射律
|--- A∨¬A 排中律
また「A≡B」で記述した「同値である」という意味は、「A |--- B」と「B |--- A」とが共に成り立つという意味ですから、結局、一つの論理体系というものは推論法則の集まりとして記述できることになります。では公理や定理はというと、これらは形式的な記号列であり、意味は持たなくても良いものと言えます[*1]。それに対して推論法則の方は、証明列の中の論理式の間の関係を規定するというメタ数学的な意味を持つものだと言えます。
ここで一転ですが、「A |--- B」という推論法則は「A→B」という論理式に対応させることができます。「A→B」という論理式は「A |--- B」という証明列における事実を記述した式だと言えます。すると推論規則は「○→×」という形の公理で代替することができます。ただし推論規則がひとつもないと証明ができませんが、それは実は「→除去」つまり「正格法(modus ponens)」がひとつあれば十分なのです。これひとつあれば、P→Qという公理から「P |--- Q」という推論法則が導けるのです。
メタ証明1.2-1
1) |--- P→Q ∵公理(公理が推論できるという推論規則)
2) P、P→Q |--- Q ∵PとQに正格法を適用
3) P |--- Q ∵証明列が存在する
最後の論理は少々飛んでいる気もしますが、次の式列が推論法則に沿っていることを言っています。
証明列1.2-1
1) P ∵仮定
2) P→Q ∵公理
3) Q ∵1と2から正格法により
くどく言えば、証明列1.2-1において「(公理「P→Q」のもとではいつでも)仮定PのもとではQが推論できる」という事実を、推論法則「P |--- Q」が成り立つ、と定義していると言えます。ここでPは仮定であって公理ではないので、証明列1.2-1は厳密には証明列ではありません。ただ、そもそも公理というものも仮定するものであり、形式的証明とはすべて「公理○○のもとで」という条件がつくもので、これは「仮定○○のもとで」という条件付きでの証明と本質的に(構造的に?形式的には?)違うものではありません。言ってみれば、証明列とは前提(通常は使用した公理)から結論が導けるという、ひとつの推論法則を示したものなのです。このあたりの事情は、前原の本[Ref-3,p13]では「成り立つことがわかる」と、さらっと流しています。
さらに別の点をくどく言えば、メタ証明1.2-1のステップ2と証明列1.2-1のステップ3での「P、P→Q |--- Q」が成立する理由は、正格法の推論規則「A、A→B |--- B」のAとBにはあらゆる論理式を当てはめて良いからです。これは命題変数A、Bを使った推論規則が実は、AとBにあらゆる論理式を当てはめた無限個の規則を表していることを意味します。しかし上記のPとQはそうではなく、ある特定の論理式を示しています。ここで公理と仮定した「P→Q」とは、何らかの特定な論理式、この公理系だけで成り立つものとした論理式です。以上の点は、公理の表記においても注意したい点です。
さてこのように、推論規則「正格法」のもとでは論理式「P→Q」は「P |--- Q」という論理体系における事実の表明になっています。しかし「P |--- Q」という事実から論理式「P→Q」が導けるとは限りません。つまり「P |--- Q」という論理体系世界の事実は、自動的に公理「P→Q」を生み出しはしません。ここでもし「→導入」という次の推論規則が定めてあれば、「P |--- Q」から「P→Q」がそのまま導けます。
→導入) [A |--- B] |--- A→B
さて紹介したような妥当な推論法則を全て導けるような公理系としてはゲンツェン流とヒルベルト流の2つが有名です。この2つはかなり対照的な体系ですが、次回に紹介します。
--------
*1) 特定の意味を持たないゆえに、どんな意味を当てはめることもできて、現実的などんなモデルにも適用できる一般性を持つということが、論理体系が広く役立つ理由のひとつである。
前回の続き
論理体系には公理と定理、および推論規則と推論法則が存在します。公理は、無条件に真と決めた論理式です。定理は、公理からの証明列の結論として導かれる論理式です。推論法則は、論理式の並びである式列が正しい証明列になっていることを決める規則です。つまり正しい証明列とはそれを構成するすべての論理式が次のどれかに相当するものです。
・公理である。
・式列の中で前にある論理式のいくつかから推論法則により導かれている
推論規則は、無条件に成立すると決めた推論法則であり、推論規則からメタ数学的に成立が証明された推論法則だけを特に推論法則と呼んで、推論規則と区別する場合もあります。いわば推論規則は公理に当たり、推論法則は定理に当たります。
推論法則を記述するにはいくつかの方法があります。例として「→除去」と呼ばれる推論規則を取ります。これは、正格法(modus ponens)または単に三段論法と呼ばれる最も基本的な推論法則です。ヒルベルト流という体系では命題論理での推論規則としてはこれひとつだけを採用しているくらいに基本的なものです。
言語表現1) AとA→Bとから、Bが推論できる。
言語表現2) AでありA→Bであるならば、Bが推論できる。
推論図式[Ref-4 p50(3章)]
A A→B
-------
B
線形表現{推論形式[Ref-4 p50(3章)]} A、A→B |--- B
個人的には推論図式がわかりやすいとは思うのですが、行が増えてしまうので今後は線形表現で記することにします。この表現は細かい部分、例えば記号「|---」などでは本記事独自である点を御了解ください。ということで、前回の独断により選んだ妥当な推論法則もこの表記を使っています。
また反射律や排中律のように論理式(公理)として記述してあるものも、実は、「無前提でこれらの公理が推論できる」という推論法則として記述することができます。
|--- A→A 反射律
|--- A∨¬A 排中律
また「A≡B」で記述した「同値である」という意味は、「A |--- B」と「B |--- A」とが共に成り立つという意味ですから、結局、一つの論理体系というものは推論法則の集まりとして記述できることになります。では公理や定理はというと、これらは形式的な記号列であり、意味は持たなくても良いものと言えます[*1]。それに対して推論法則の方は、証明列の中の論理式の間の関係を規定するというメタ数学的な意味を持つものだと言えます。
ここで一転ですが、「A |--- B」という推論法則は「A→B」という論理式に対応させることができます。「A→B」という論理式は「A |--- B」という証明列における事実を記述した式だと言えます。すると推論規則は「○→×」という形の公理で代替することができます。ただし推論規則がひとつもないと証明ができませんが、それは実は「→除去」つまり「正格法(modus ponens)」がひとつあれば十分なのです。これひとつあれば、P→Qという公理から「P |--- Q」という推論法則が導けるのです。
メタ証明1.2-1
1) |--- P→Q ∵公理(公理が推論できるという推論規則)
2) P、P→Q |--- Q ∵PとQに正格法を適用
3) P |--- Q ∵証明列が存在する
最後の論理は少々飛んでいる気もしますが、次の式列が推論法則に沿っていることを言っています。
証明列1.2-1
1) P ∵仮定
2) P→Q ∵公理
3) Q ∵1と2から正格法により
くどく言えば、証明列1.2-1において「(公理「P→Q」のもとではいつでも)仮定PのもとではQが推論できる」という事実を、推論法則「P |--- Q」が成り立つ、と定義していると言えます。ここでPは仮定であって公理ではないので、証明列1.2-1は厳密には証明列ではありません。ただ、そもそも公理というものも仮定するものであり、形式的証明とはすべて「公理○○のもとで」という条件がつくもので、これは「仮定○○のもとで」という条件付きでの証明と本質的に(構造的に?形式的には?)違うものではありません。言ってみれば、証明列とは前提(通常は使用した公理)から結論が導けるという、ひとつの推論法則を示したものなのです。このあたりの事情は、前原の本[Ref-3,p13]では「成り立つことがわかる」と、さらっと流しています。
さらに別の点をくどく言えば、メタ証明1.2-1のステップ2と証明列1.2-1のステップ3での「P、P→Q |--- Q」が成立する理由は、正格法の推論規則「A、A→B |--- B」のAとBにはあらゆる論理式を当てはめて良いからです。これは命題変数A、Bを使った推論規則が実は、AとBにあらゆる論理式を当てはめた無限個の規則を表していることを意味します。しかし上記のPとQはそうではなく、ある特定の論理式を示しています。ここで公理と仮定した「P→Q」とは、何らかの特定な論理式、この公理系だけで成り立つものとした論理式です。以上の点は、公理の表記においても注意したい点です。
さてこのように、推論規則「正格法」のもとでは論理式「P→Q」は「P |--- Q」という論理体系における事実の表明になっています。しかし「P |--- Q」という事実から論理式「P→Q」が導けるとは限りません。つまり「P |--- Q」という論理体系世界の事実は、自動的に公理「P→Q」を生み出しはしません。ここでもし「→導入」という次の推論規則が定めてあれば、「P |--- Q」から「P→Q」がそのまま導けます。
→導入) [A |--- B] |--- A→B
さて紹介したような妥当な推論法則を全て導けるような公理系としてはゲンツェン流とヒルベルト流の2つが有名です。この2つはかなり対照的な体系ですが、次回に紹介します。
--------
*1) 特定の意味を持たないゆえに、どんな意味を当てはめることもできて、現実的などんなモデルにも適用できる一般性を持つということが、論理体系が広く役立つ理由のひとつである。
※コメント投稿者のブログIDはブログ作成者のみに通知されます