命題論理における形式的演繹体系
要約：この授業では、形式的演繹体系について再検討します。これらの体系が、異なる論理式の間に存在しうる関係を解明するためにどのように用いられるか、そして証明を構成するための基本要素——言語、公理、推論規則——について説明します。ルカシェビッチの公理が紹介され、命題計算における推論の原動力としてモーダス・ポネンスが解説されます。さらに、推論・定理・前提という概念にも触れ、演繹体系における証明の実行方法が示されます。
学習目標：
- 理解する：命題論理における形式的演繹体系の概念を。
- 識別する：形式的演繹体系の基本構成要素を。
- 把握する：命題計算におけるルカシェビッチの公理を。
- 理解する：モーダス・ポネンスが命題計算の推論エンジンであることを。
- 理解する：形式的演繹体系における証明の実行方法と、前提・推論・定理の違いを。
- 理解する：公理スキームと推論規則を通じて、いかにして演繹が生成されるかを。
- 認識する：論理が表現間の関係を接続し、自然言語の表現へ置き換える能力を。
内容目次：
形式的演繹体系とは何か？
命題論理におけるルカシェビッチの公理
モーダス・ポネンス：命題計算の推論エンジン
推論・定理・前提
命題論理における証明はどのように実行されるか？
証明された同値概念
（メタ）演繹定理
演繹定理の逆
表現に関する演繹と、演繹に関する演繹
単調性の規則
演繹体系と命題論理に関する総括と考察
論理学の学習において、私たちは転換点に到達しました。ここから命題論理の演繹体系の検討が始まります。ここでは、これまで学んだ内容が実践的に機能し始め、論理の真の精神が現れます。なぜなら、証明の本質を探求するからです。この段階では、すでに論理式の書き方や命題論理の概要を理解していることが前提です。もし完全に理解できていない場合は、この授業の前に行われた講義を見直すことをお勧めします。
この準備が整った後、次に進むべきは、命題論理の表現がどのように相互に関係して演繹を構成するのかを検討することです。その関係を構築するための仕組みが形式的演繹体系なのです。
形式的演繹体系とは何か？
形式的演繹体系、または演繹計算体系には、以下の3つの基本的構成要素があります：
- 形式言語。
- 公理スキーム。
- 基本的な推論規則。
形式言語に関してはすでに学習済みです。これからは、公理スキームと基本推論規則について導入していきます。
命題計算の演繹体系を構築するにあたり、ルカシェビッチの公理を出発点とし、基本的な推論規則としてモーダス・ポネンスを使用します。
命題論理におけるルカシェビッチの公理
もし \alpha, \beta および \gamma が命題計算の式であるならば、 以下の式は命題計算の公理である：
| [A1] | (\alpha \rightarrow (\beta \rightarrow \alpha)) |
| [A2] | ((\alpha \rightarrow (\beta \rightarrow \gamma))\rightarrow ((\alpha\rightarrow \beta)\rightarrow(\alpha \rightarrow \gamma))) |
| [A3] | ((\neg\beta \rightarrow \neg\alpha)\rightarrow(\alpha\rightarrow \beta)) |
モーダス・ポネンス：命題計算の推論エンジン
\alpha と \beta が命題計算における有効な式であるとする。 そのとき、モーダス・ポネンスは、\alpha および (\alpha \rightarrow \beta) から \beta を導出できると規定する。この推論形式は次のように表される：
| (1) | \alpha | ; 前提 |
| (2) | (\alpha \rightarrow \beta) | ; 前提 |
| (3) | \beta | ; MP(1,2) |
ここでは、ステップ (1) と (2) の間でモーダス・ポネンスを「MP(1,2)」と略記して表現しており、全体の要約は次の記法で示される：
したがって、 \{\alpha, (\alpha \rightarrow \beta)\}\vdash \beta
まもなく、ルカシェビッチの公理とモーダス・ポネンスから、命題計算のすべての演繹技法を構築できることが分かるでしょう。これらは日常的推論の基本規則を要約し、古典論理の基礎をなすものです。
推論、定理、および前提
命題論理の演繹体系では、推論（あるいは演繹）が実行されます。これらは、一連の式の列であり、各式は前提であるか、ルカシェビッチの公理とモーダス・ポネンスのみを用いて前提から導かれる式である必要があります。定理とは、前提なしで得られる演繹の結果です。前提とは、公理ではなく、公理からも導かれない任意の式のことを指します。一般的に、前提の集合を \Gamma、そこから導かれる式を \alpha とするとき、次のように記述します：「\Gamma \vdash \alpha」そして、以下のように言います：
\Gamma から \alpha が導かれる
\Gamma が空集合である場合、「\emptyset\vdash \alpha」とは書かず、「 \vdash \alpha 」と書きます。これは「\alpha は定理である」と読みます。この定理の表記法は、公理の表記にも拡張でき、\alpha、\beta、\gamma が式であるならば、ルカシェビッチの公理は次のように表されます：
| [A1] | \vdash (\alpha \rightarrow (\beta \rightarrow \alpha)) |
| [A2] | \vdash((\alpha \rightarrow (\beta \rightarrow \gamma))\rightarrow ((\alpha\rightarrow \beta)\rightarrow(\alpha \rightarrow \gamma))) |
| [A3] | \vdash((\neg\beta \rightarrow \neg\alpha)\rightarrow(\alpha\rightarrow \alpha)) |
このことから、公理はそれ自体で明白な命題である、定理は空から導かれる式である、あるいは公理と定理は命題計算における特性である、と言われるのです。
命題論理における証明はどのように実行されるか？
ここから理論的な話を離れ、実践に入ります。証明の実行方法については、多くのことを語ることができます。しかし、演繹体系や命題論理についてどれほど優れた説明がなされ、理解されていたとしても、それだけで証明を実行するために必要な能力が自動的に身につくわけではありません。そのため、証明のやり方を教えるには、まず簡単な定理の証明を確認することが有効です。
定理
\alpha が命題論理の式であるならば、次が成り立ちます：
\vdash (\alpha\rightarrow \alpha)
証明
| (1) | (\alpha\rightarrow ( \alpha \rightarrow \alpha)) | ; A1 |
| (2) | (\alpha\rightarrow ((\alpha\rightarrow \alpha)\rightarrow\alpha)) | ; A1 |
| (3) | ( (\alpha\rightarrow((\alpha\rightarrow\alpha)\rightarrow\alpha)) \rightarrow ((\alpha\rightarrow (\alpha\rightarrow\alpha))\rightarrow( \alpha\rightarrow \alpha))) | ; A2 |
| (4) | ((\alpha\rightarrow (\alpha\rightarrow\alpha))\rightarrow( \alpha\rightarrow \alpha)) | ; MP(2,3) |
| (5) | ( \alpha\rightarrow \alpha) | ; MP(1,5) |
したがって、 \vdash (\alpha\rightarrow\alpha)
証明終わり。
見ての通り、演繹体系および命題論理において証明は決して自明なものではありませんが、一度構築されれば、それを再現するのは容易です。
さて、これらの技法を使って本格的に演繹を行う前に、まずはそれを効果的に行うために非常に有用となるいくつかの性質や定義を紹介します。というのも、もしこれらだけに頼って推論しようとすると、深刻な問題に直面することになるからです。
証明された同値の概念
\alpha と \beta が任意の式であり、次の両方が成り立つとき：\{\alpha\}\vdash \beta かつ \{\beta\} \vdash \alpha、このとき \alpha と \beta は**証明において同値**であると言い、次のように記述されます：\alpha \dashv \vdash \beta。これは次のように記号的に要約されます：
\left(\{\alpha\}\vdash\beta \wedge \{\beta\}\vdash\alpha \right) \Leftrightarrow \left(\alpha\dashv\vdash\beta\right)
これは次のように読みます： \alpha から \beta が導かれ、\beta から \alpha が導かれる、**その場合に限り**、\alpha と \beta は証明において同値である。
これは命題論理におけるメタ性質のひとつです。
（メタ）演繹定理
\alpha および \beta が命題計算における式であり、 \Gamma が前提の集合であるとする。そのとき、\Gamma \cup \{\alpha\} から \beta が導かれるならば、\Gamma から (\alpha \rightarrow \beta) が導かれる。これは次のように記号で表されます：
\left(\Gamma \cup \{\alpha\}\vdash \beta \right) \Rightarrow \left( \Gamma\vdash(\alpha\rightarrow\beta)\right)
証明：
\Gamma \cup \{\alpha\}\vdash \beta が成り立つためには、次のような形の演繹が存在する必要があります：
| (1) | \gamma_1 | ; \Gamma の前提1 |
| \vdots | \vdots | |
| (n) | \gamma_n | ; \Gamma の前提n |
| (n+1) | \overline{\gamma}_1 | ; 前のいずれかの行とのモーダス・ポネンス |
| \vdots | \vdots | |
| (n+m) | \overline{\gamma}_m | ; 前のいずれかの行とのモーダス・ポネンス |
| (n+m+1) | \alpha | ; 前提 |
| (n+m+2) | \beta | ; モーダス・ポネンス (n+m+1, それ以前のステップのいずれか) |
したがって、 \Gamma\cup\{\alpha\} \vdash \beta
このことが可能であるためには、式 \gamma_1, \cdots \gamma_n,\overline{\gamma_1},\cdots,\overline{\gamma_m} の少なくとも1つが (\alpha\rightarrow \beta) の形である必要があります。しかし、これらの行はすべて \Gamma の要素およびルカシェビッチの公理のみを用いて導かれているため、\Gamma\vdash (\alpha \rightarrow \beta) が成り立つことになります。よって、定理が証明されたことになります。
証明終わり。
演繹定理の逆
\left(\Gamma\vdash(\alpha \rightarrow \beta)\right) \Rightarrow \left( \Gamma \cup \{\alpha\}\vdash \beta \right)
証明：
もし \Gamma\vdash (\alpha\rightarrow \beta) が成り立つならば、次のような形の演繹が存在します：
| (1) | \gamma_1 | ; \Gamma の前提1 |
| \vdots | \vdots | |
| (n) | \gamma_n | ; \Gamma の前提n |
| (n+1) | (\alpha \rightarrow \beta) | ; モーダス・ポネンス（上のどこかの行の組から） |
この推論に \alpha を追加の前提として加えると、次のような行が得られます：
| (n+2) | \alpha | ; 追加の前提 |
| (n+3) | \beta | ; MP(n+1,n+2) |
したがって、 \Gamma \cup \{\alpha\} \vdash \beta
これが証明すべきことであった。
式に関する演繹と、演繹に関する演繹
先に示した \vdash (\alpha\rightarrow \alpha) という結果に至る証明は、「式に基づく演繹」の一例です。なぜなら各ステップが具体的な式を含んでいるからです。同様に、「演繹に基づく演繹」も構成可能であり、その場合、各ステップはそれ自体が一つの演繹となります。実際には、両者は類似した手続きで行われますが、後者では演繹定理とその逆を活用できるため、推論技法に大きな柔軟性がもたらされます。これを確認するために、もう一度 \vdash (\alpha \rightarrow \alpha) を証明してみましょう。ただし、今度は式の列ではなく、演繹の列として行います。その一例は以下の通りです：
| (1) | \vdash (\alpha \rightarrow (\alpha \rightarrow \alpha)) | ; A1 |
| (2) | \{\alpha\}\vdash ( \alpha \rightarrow \alpha) | ; RTD(1) |
| (3) | \{\alpha\}\cup \{\alpha\}\vdash \alpha | ; RTD(2) |
| (4) | \{\alpha\}\vdash \alpha | ; 注意：\{\alpha\}\cup\{\alpha\}=\{\alpha\} |
| (5) | \vdash (\alpha\rightarrow \alpha) | ; TD(4) |
この推論は、以前に行ったものよりも短くはありませんが、より容易に構築できます。なぜなら、演繹定理、その逆、および公理スキーム A1 のみを用いているからです。
一見すると、この展開ではルカシェビッチの公理のうち1つしか使用しておらず、他の公理やモーダス・ポネンスをまったく使っていないように思えます。では、この推論方法によって他の公理やモーダス・ポネンスを忘れてしまってもよいのでしょうか？答えは「はい」と「いいえ」の両方です。一方で、明示的に使用しないため、使用していないかのように扱うことは可能です。しかし他方で、演繹定理およびその逆は、まさにルカシェビッチの公理とモーダス・ポネンスから導かれる結果であるため、それらを使用することは、暗黙のうちにこれらの構成要素を使用していることになるのです。
単調性の規則
\tau が定理であるとすると、 任意の式 \beta に対して次が成り立ちます：
\{\beta\}\vdash\tau
これは非常に簡単に証明できる規則です。なぜなら \tau が定理であるということは、\vdash \tau が成り立つ、すなわち、前提を加えることなく \tau に到達する推論が存在するということです。したがって、空集合に式 \beta を追加しても、結論には影響を与えません。
これと類似の結果として、次のことも言えます。もし前提の集合 \Gamma から \gamma が導かれるならば、
\Gamma\cup\{\alpha\}\vdash\gamma
が成り立ちます。ここで \alpha は任意の式です。
演繹体系と命題論理に関する総括と考察
命題論理の言語に推論規則と基本式を与えると： すなわち、モーダス・ポネンスとルカシェビッチの公理を与えると、それは「演繹機械」を構築し、動力源を与えてその機械を稼働させるのと同じことになります。ここから自然に、すべての基本的な演繹規則が現れ始めます。これらについては、次回以降の講義で順に検討していきます。
もう一つ重要な点として、命題論理の式は、以前学習した2つの記号の言語におけるメタ表現であるということです。これらのメタ表現の強みは、メタ変項に任意の式を代入して、その構造を満たす新たな式を構築できる点にあります。命題論理の言語に公理スキームと推論規則を導入することによって、命題論理の演繹体系が構築され、表現を結びつける推論が可能になります。その結果として、無限に多くの推論を含むことができる演繹スキームが得られます。なぜなら、任意のメタ変項を任意の式で置き換えることによって、それらすべての演繹を生成できるからです。論理の真の力が発揮されるのは、私たちがこの2記号言語の式だけでなく、それを自然言語の表現に置き換えたときに何が起こるのかを観察し始めたときなのです。