命題論理のソースを表示

{{出典の明記|date=2014年3月3日 (月) 11:47 (UTC)}}
'''命題論理'''（{{読み|めいだいろんり、|}}{{lang-en-short|propositional logic}}）とは、[[数理論理学]]（[[記号論理学]]）の基礎的な一部門であり<ref>[https://kotobank.jp/word/%E5%91%BD%E9%A1%8C%E8%AB%96%E7%90%86-643103 命題論理] - [[大辞林]]/[[大辞泉]]/[[コトバンク]]</ref>、[[命題]]全体を1つの[[論理式 (数学)|記号に置き換え]]て単純化し、[[論理演算]]を表す記号（[[論理記号の一覧|論理記号]]・[[論理演算子]]）を用いて、その命題（記号）間の結合パターンを表現・研究・把握することを目的とした分野のこと。[[ブール論理]]は[[ブール代数]]で形式化され2値の意味論を与えられた命題論理とみることができる。

命題を1つの記号で大まかに置き換える命題論理に対して、命題の述語（P）と主語（S）を、[[関数 (数学)|関数]]のF(x)のように別記号で表現し、更に[[量化子]]で主語（S）の数・量・範囲もいくらか表現し分けることを可能にした、すなわちより詳細に命題の内部構造を表現できるようにしたものを、[[述語論理]]と呼ぶ。

== 概要 ==
命題論理の[[命題]]の取り扱いは普通、{{読み仮名|'''命題計算'''|めいだいけいさん}}<ref group="注釈">{{lang-en-short|propositional calculus}}</ref>、または{{読み仮名|'''文計算'''|ぶんけいさん}}<ref group="注釈">{{lang-en-short|sentential calculus}}</ref>と呼ぶ命題[[変数 (数学)|変数]]を[[原子式]]にするような形式的な推論の体系によってなされる。

命題論理において問題になるのは、個々の命題の「意味」よりも命題を「かつ」「ならば」などの[[論理演算|論理演算子]]で関係づけたときにどんな推論ができるか、ということである。命題論理と違い主に個々の命題の意味を扱うのは[[述語論理]]などである。

推論の性質をいかなる形に考えるかによって、[[直観主義論理]]的な命題論理をはじめ[[様相論理]]や[[相関論理]]などさまざまな命題論理が考えられるが、通常、単に命題論理と呼んだ場合には、{{読み仮名|古典命題論理|こてんめいだいろんり}}<ref group="注釈">{{lang-en-short|classical propositional logic}}</ref>を指す（[[古典論理]]）。従って、本項目では古典命題論理について主に解説することとする。

一般的にいえば、命題計算とは「文法的にきちんとした」統語的な表現（[[well-formed formula|整式]]）の[[集合]]、その表現のいくつかからなる[[集合|部分集合]]（[[公理]]の集合）、さらに加えて表現の空間上に[[二項関係]]を定義する変形規則の集合からなる形式的体系である。

普通、それぞれの表現が数学の表現として具体的に解釈されるとき、表現の変形規則が一定の意味同等性を保つように与えられる。特に表現が論理体系そのものとして解釈されるときには「意味同等性」が論理的同等性のことを指すように変形規則が与えられる。この設定のもとでは変形規則によって与えられた表現から論理的に等価な表現を導くことができる。こういった変形規則による別の表現の導出について、特別な例として表現を単純化すること、与えられた表現が前もって区別された特別な表現（普通、論理学の公理だと解釈される）のうちどれかと等価かどうか決定すること、などが問題にされる。

命題論理における''言語''は命題変数（命題をはめ込む枠）と文[[論理演算|演算子]]（結合子）からなっている。形式文法によって[[帰納的]]にその言語の表現や整式が、原子式や文演算子の一定の組みあわせとして定義される。公理の集合は空集合でも、空でない有限集合でも、可算無限集合でもいいし、あるいは[[公理図式]]によって与えられてもいい。加えて、意味論によって真かどうかの値付け（または解釈）が定められる。それによってどの整式が正しい、つまり[[定理]]であるかを決めることができるようになる。

以下では標準的な命題論理の大筋を解説する。しかしこの他にも、ほぼ等価ではあるが、言語を構成している演算子や変数が違ったり、あるいは公理や推論規則が違ったりして、ここで説明するものと見かけが異なる方法も存在する。

== 文法 ==
言語の構成要素は
# [[アルファベット]]の[[大文字]]は命題変数を表す。これらは[[原子論理式|原子式]]である。
# 以下の'''結合子'''（または[[論理演算子]]）を表す記号：「<math>\lnot</math>」([[否定]]) 「<math>\land</math>」([[論理積|連言]]) 「<math>\lor</math>」([[論理和|選言]]) 「<math>\rarr</math>」([[論理包含|含意]])。（「<math>P \rarr Q</math>」は「<math>\lnot P \lor Q</math>」と等価だ、などとしていくつかを他のものの短縮形だと見なしてこれより少ない演算子（と記号）でやることもできる。）電子メールなど使用できる文字が限られた環境では、論理的否定を表すのに[[チルダ]]「<code>~</code>」を用いたり、論理積を表すのに[[アンパサンド]]「<code>&amp;</code>」を用いたりといった記号の代用もよく見られる。
# 開き括弧 ( と閉じ括弧 )
整式の集合は以下の規則によって帰納的に定義される。
# 基本：アルファベットの大文字は整式
# 帰納節 I: もし <math>\phi</math> が整式なら <math>\lnot\phi</math> も整式
# 帰納節 II:  <math>\phi</math> と <math>\psi</math> が整式なら <math>(\phi\land\psi)</math> や <math>(\phi\lor\psi)</math>、<math>(\phi\rarr\psi)</math> も整式
# 閉節：これ以外は整式でない
これらを繰り返し適用することでより複雑な整式が作られる。例えば
#<math>A</math> は整式
#<math>\lnot A</math> は整式
#<math>B</math> は整式
#<math>(\lnot A\lor B)</math> は整式

== 計算 ==
命題論理は、主として整式同士の論理的関係性を示すために用いられる。このために、利用可能な（整式の）変形規則を使って、「証明」もしくは「展開」と呼ばれる手続きを行う。証明は、番号のついた複数の行からなる記述によって表現される。それぞれの行は、「根拠」もしくは「理由」をそえた、当該の整式を導き出すための単一の整式（論理式）とする。証明を行うために必要な仮定は、「前提」と注記し、証明のはじめの部分に置く。結論は最後の行に示す。すべての行の内容が、それ以前の行の内容に基づき、（整式の）変形規則を正しく適用して得られたものであるとき、証明が完了したとみなされる。（なお、[[タブローの方法]]という別の記述方法もある。）

=== 公理 ===
本節では簡単のため、公理を持たない、あるいは同じことだが[[空集合|空な]]公理集合を持つ[[自然演繹]]体系を使うことにする。

=== 推論規則 ===
ここでの命題計算では八つの推論規則を考える。これらの規則によって真だと仮定された式たちからほかの真な式を導くことができる。最初の六つは単に特定の整式をほかの整式から導けると述べている。一方で、最後の二つの前提では（まだ証明されていない）仮定を一時的に用いている。このことを指して、最初の六つの規則を非仮定的規則、最後の二つは仮定的規則であると言う。

;[[二重否定の除去]]<!-- Double negative elimination -->:整式 <math>\lnot\lnot\phi</math> からは <math>\phi</math> を推論できる。
;[[論理積の導入]]<!-- Conjunction introduction -->:整式 <math>\phi</math> と整式 <math>\psi</math> からは <math>(\phi \land \psi)</math> を推論できる。
;[[論理積の消去]]<!-- Conjunction elimination -->:整式 <math>\phi \land \psi</math> からは <math>\phi</math> と <math>\psi</math> を推論できる。
;[[論理和の導入]]<!-- Disjunction introduction -->:整式 <math>\phi</math> からは、どんな整式 <math>\psi</math> についても <math>(\phi\lor\psi)</math> と <math>(\psi\lor\phi)</math> を推論できる。
;[[論理和の消去]]<!-- Disjunction elimination -->: <math>(\phi\lor\psi)</math> と <math>(\phi\rarr\chi)</math>、<math>(\psi\rarr\chi)</math> というかたちの整式からは <math>\chi</math> を推論できる。
;[[モーダスポネンス]] ([[前件肯定]]式、肯定式とも。)<!-- Modus ponens -->: <math>\phi</math> と <math>(\phi\rarr\psi)</math> という形の整式からは <math>\psi</math> を推論できる。
;条件付き証明<!-- Conditional proof -->: <math>\phi</math> を仮定して整式 <math>\psi</math> が導かれたら <math>(\phi\rarr\psi)</math> を推論できる。
;[[背理法]]<!-- Reductio ad absurdum -->: <math>\phi</math> を仮定して <math>\psi</math> と <math>\lnot\psi</math> が導かれたら <math>\lnot\phi</math> を推論できる。

===証明の例===
* {{math|''A'' → ''A''}}を証明する。

* 下記にその証明の一例を挙げる（より厳密に証明しようとすればより多くのステップを要する）。

{| style="margin:auto;" class="wikitable"
|-
! colspan="3"| 証明の例
|-
! 行番号
! 整式
! 根拠
|-
| 1 || <math>A</math> || 前提
|-
| 2 || <math>A \lor A</math> || 1,論理和の導入
|-
| 3 || <math>(A \lor A) \land A</math> || 1,2,論理積の導入
|-
| 4 || <math>A</math> || 3,論理積の消去
|-
| 5 ||  <math>A \to A</math> || 1,4,条件付き証明
|}

== 規則の健全性と完全性 ==
個々に挙げられた規則の重要な性質は[[健全性]]と完全性である。直感的には、これらの規則は正しくしかも他に必要な規則はないということである。これは以下のようにして形式化される。

真理値の割り当てを、命題変数に対して'''真'''（<math>\top</math>）または'''偽'''（<math>\bot</math>）の値を対応させる関数だと考えることにする。形式的でない言い方をすれば、真理値の割り当てとは、特定の叙述が真になり他は偽になるような「おきうる事態」（またはありうる世界）についての説明だと理解できる。その「事態」においてそれぞれの式が正しくなるのはどんなときかを定めることで式の意味論が定式化できる。

真理値の割り当て<math>A</math>がどんなときに特定の整式を充足するか、ということを以下の規則によって定める。
*<math>A(P) = \top</math> であるとき、およびそのときに限って <math>A</math> は命題変数 <math>P</math> を充足する
*<math>A</math>が <math>\phi</math> を充足しないとき、およびそのときに限って <math>A</math> は <math>\lnot\phi</math> を充足する
*<math>A</math>が <math>\phi</math> と <math>\psi</math> を充足するとき、およびそのときに限って <math>A</math> は <math>(\phi \land \psi)</math> を充足する
*<math>A</math>が <math>\phi</math> か <math>\psi</math> の少なくともどちらかを充足するとき、およびそのときに限って <math>A</math> は <math>\phi \lor \psi</math> を充足する
*<math>A</math>が<math>\phi</math>を充足するのに <math>\psi</math> を充足しないということがないとき、およびそのときに限って <math>A</math> は <math>(\phi \rarr \psi)</math> を充足する
この定義によって式 <math>\phi</math> が特定の式の集合 <math>\mathbb{S}</math> から従うとはどういうことなのかを定式化できる。格式張らずにいえばこれは、<math>\mathbb{S}</math> の式が成り立っているようなすべての世界において <math>\phi</math> が成立していることだ、といえる。これは次のように形式化できる：<math>\mathbb{S}</math> の式をすべて充足するような真理値の割り当てが必ず <math>\phi</math> を充足するとき、整式 <math>\phi</math> は <math>\mathbb{S}</math> から意味論的に帰結する（または導かれる）、という。

最後に、統語的な帰結という関係を、<math>\phi</math> が上に挙げた推論規則に従って有限の段階で <math>\mathbb{S}</math> の式から導出されるとき、およびそのときに限って <math>\phi</math> は <math>\mathbb{S}</math> から統語的に帰結する、として定める。これによって推論規則の集合が健全だとか完全だとかいうのはどういうことなのかを定式化できる。
;健全性:もし <math>\phi</math> が整式の集合 <math>\mathbb{S}</math> から統語的に帰結するなら <math>\phi</math> は <math>\mathbb{S}</math> から意味論的に帰結する
;完全性:もし <math>\phi</math> が <math>\mathbb{S}</math> から意味論的に帰結するなら <math>\phi</math> は <math>\mathbb{S}</math> から統語的に帰結する
上記の自然命題論理の規則の集合についてはこれらが成り立っている。

== 別の論理計算の定式化 ==
文法と論理演算子のほとんどを公理によって定め、推論規則を一つだけしか持たないような、他の方式の命題計算を定義することもできる。
以下、<math>\phi</math>、<math>\chi</math>、<math>\psi</math> で整式を表すことにする。個々の整式自体はギリシャ文字を含まず、ローマ字と結合子と括弧のみからなっている。

=== 公理系1 ===
[[スティーブン・コール・クリーネ]]によって導入された体系<ref> S.C. Kleene, Introduction to Metamathematics, North Holland (1967). </ref>では11の公理と一つの推論規則が用いられる。
{|class=wikitable
!名前!!公理!!備考
|-
|{{lang|en|THEN}}-1||<math>\phi \rarr (\chi\rarr\phi)</math>||nowrap|含意の導入<ref group="注釈">{{lang-en-short|introduction of implication}}</ref>と一般的に呼ぶ
|-
|{{lang|en|THEN}}-2||<math>(\phi \rarr (\chi\rarr\psi)) \rarr ((\phi\rarr\chi) \rarr (\phi\rarr\psi))</math>||nowrap|「含意の推移性」に対応。フレーゲの三段論法<ref group="注釈">{{lang-en-short|Fregean syllogism}}</ref>と一般的に呼ぶ。
|-
|{{lang|en|AND}}-1||<math>\phi \land \chi \rarr \phi</math>||nowrap|「論理積の消去」に対応。単純化<ref group="注釈">{{lang-en-short|simplification}}</ref>と呼ぶ。
|-
|{{lang|en|AND}}-2||<math>\phi \land \chi \rarr \chi</math>||nowrap|「論理積の消去」に対応。
|-
|{{lang|en|AND}}-3||<math>\phi \rarr (\chi \rarr (\phi \land \chi))</math>||nowrap|「論理積の導入」に対応。
|-
|{{lang|en|OR}}-1||<math>\phi \rarr \phi \lor \chi</math>||nowrap|「論理和の導入」に対応。
|-
|{{lang|en|OR}}-2||<math>\chi \rarr \phi \lor \chi</math>||nowrap|「論理和の導入」に対応。
|-
|{{lang|en|OR}}-3||<math>(\phi\rarr\psi) \rarr ((\chi\rarr\psi) \rarr (\phi\lor\chi\rarr\psi))</math>||nowrap|
|-
|{{lang|en|NOT}}-1||<math>(\phi\rarr\chi) \rarr ((\phi\rarr\lnot\chi) \rarr \lnot\phi)</math>||nowrap|「背理法」に対応。
|-
|{{lang|en|NOT}}-2||<math>\phi \rarr (\lnot\phi\rarr\chi)</math>||nowrap|「{{lang|en|principle of explosion}} 矛盾からは何でも導出できる」。
|-
|{{lang|en|NOT}}-3||<math>\phi \lor \lnot\phi</math>||nowrap|「[[排中律]]」。
|}

*公理 {{lang|en|AND}}-1 と公理 {{lang|en|AND}}-2 の平行性は論理積の可換性を反映している。
*公理 {{lang|en|OR}}-1 と公理 {{lang|en|OR}}-2 の平行性は論理和の可換性を反映している。
*公理 {{lang|en|NOT}}-2 に何らかの制限を加えて論理体系を構成する方法は[[矛盾許容論理]]と呼ぶ。
*公理 {{lang|en|NOT}}-3 は命題式の意味論的値付けの可能性を反映している：式の真理値は真か偽のどちらかである。少なくとも古典的論理学においては第三の真理値という可能性は考慮されない。公理 {{lang|en|NOT}}-3 を認めないで論理体系を構成する方法は[[直観主義論理]]と呼ぶ。

推論規則は[[モーダスポネンス]]、つまり
:<math>\phi</math> と <math>(\phi \rarr \psi)</math> という形の整式からは <math>\psi</math> を推論できる
のみを規約する。上記の公理系とこの推論規則から[[#推論規則]]節で述べられたのと同じ演繹が可能になる。

=== 公理系2 ===
[[ダフィット・ヒルベルト]]によって定式化された公理系を以下に示す：

*<math>\phi \rarr (\chi \rarr \phi)</math>
*<math>(\phi \rarr (\chi \rarr \psi)) \rarr ((\phi \rarr \chi) \rarr (\phi \rarr \psi))</math>
*<math>(\lnot\psi \rarr \lnot\phi) \rarr (\phi \rarr \psi)</math>

を採用し、推論規則はモーダス・ポネンス、すなわち「<math>\phi</math> と <math>(\phi \rarr \psi)</math> から <math>\psi</math> を推論できる」のみを規約する。

この公理系においては、「<math>\phi\lor\psi</math>」、「<math>\phi\land\psi</math>」はそれぞれは「<math>\lnot\phi\rarr\psi</math>」、「<math>\lnot(\phi\rarr\lnot\psi)</math>」の略記とみなす。

=== 公理系3 ===
公理系2の、はじめの2つの公理を、以下の4つに置き換えたもの。
*<math>\phi \rarr (\chi \rarr \phi)</math>
*<math>(\chi \rarr (\chi \rarr \phi)) \rarr (\chi \rarr \phi)</math>
*<math>(\phi \rarr (\chi \rarr \psi)) \rarr (\chi \rarr (\phi \rarr \psi))</math>
*<math>(\chi \rarr \psi) \rarr ((\phi \rarr \chi) \rarr (\phi \rarr \psi))</math>
上の3つの公理は、[[シークエント計算]]における構造規則の弱化<ref group="注釈">{{lang-en-short|weakening}}</ref>、縮約<ref group="注釈">{{lang-en-short|contraction}}</ref>、転置<ref group="注釈">{{lang-en-short|permutation}}</ref>に対応する。

== 他の命題計算 ==

命題計算は、現在用いられている論理計算の中でも最も単純なものだと言える（[[アリストテレス]]の[[三段論法]]は、後述の述語論理に吸収されるため、現代論理学では取り扱われることは少ないが、命題計算とくらべて、言語表現を忠実に分析するという意味では、より素朴な考え方だとも言える。また、推論形式が限定されている点で、形式的にも一見単純である。ただし、現代論理の立場から省みると、そのような推論形式の制限は、かえって理論を複雑にする。また、文構造を主語と述語に分け、量化の概念を導入するなど、より精密だと言える。）。いくつかのやり方で命題計算を拡張することができる。

より複雑な論理計算を作り上げるうえで最も直接的な方法は、用いられる式についてより細かいことが言えるような規則を導入することである。命題論理の「原始的叙述」を[[項]]や[[変数 (数学)|変数]]、[[述語]]、[[量化子]]に分解することを考えると一階論理、または[[一階述語論理]]と呼び、命題論理の規則をすべて保ちながらさらに新しい規則を加えたものを得る。（例えば「すべての[[ネコ|猫]]は[[ほ乳類]]である」から「たまが猫なら、たまはほ乳類である」を推論できる、など。）

一階論理の道具立てを使うと、公理あるいは推論規則によって様々な理論を定式化し、論理計算として取り扱えるようになる。最も有名な例は[[算術]]だが、ほかにも[[集合論]]や[[メレオロジー]]が挙げられる。

[[様相論理]]は命題計算ではとらえきれないような様々な推論を可能にしている。様相論理では、例えば「<math>\rho</math> は必然的である<!-- necessarily <math>\rho</math> -->」から <math>\rho</math> を推論でき、<math>\rho</math> からは「<math>\rho</math> は可能である<!-- it is possible that <math>\rho</math> -->」が推論できる。

[[多値論理]]では文の真理値として真と偽以外のものも許容される。（例えば「真でもあり偽でもある」とか「真でも偽でもない」がよく追加される。また[[ファジィ論理]]では真と偽の間の無限にこまかい「真実である度合い」が導入される。）これらの論理学ではしばしば命題計算とは異なった計算手法が必要になる。

== 脚注 ==
{{脚注ヘルプ}}

===注釈===
{{Notelist}}
===出典===
<references/>

== 関連項目 ==
* [[演繹定理]]
* [[存在グラフ]]

== 外部リンク ==
* [https://informatics.sist.ac.jp/suganuma/kougi/other_lecture/SE/math/logic/logic.htm 記号論理学(静岡理工科大学 菅沼研究室)]

{{Mathematical logic}}

{{Normdaten}}
{{デフォルトソート:めいたいろんり}}
[[Category:命題論理|*]]
[[Category:数学に関する記事]]
[[Category:古典論理]]
[[Category:命題]]