自然演繹法

人間は,考え,思考することによって,様々な事象の間にある関係を理解し,世界の在りようを識ることができる。論理は,そのように思考することの一番基本にある体系である。

論理学は,そのような論理を扱う学問であり,合理的な思考のパターンやルールを見つけて,それを定式化することを研究する。

論理学の中で,もっとも熱心に取り上げられ,検討されてきた推論は,演繹的推論である。演繹的推論とは,前提が正しければ,そこから導かれる結論は必ず正しい推論のことを言う。このような推論を,妥当な推論と呼ぶ。

例えば,P→Q(PならばQ)とPを前提(Prem)として,P∧Qを結論とする推論は,妥当な推論である。

P→Q	Prem
P	Prem
────────
P∧Q	結論

では,どのようにしたら,ある前提からある結論を導く推論の妥当性を証明することができるであろうか。そのような方法の1つに,自然演繹法がある。自然演繹法は,我々が日頃行っている思考と直感的な一致性が高く,人間の形式的推論をモデル化した体系と考えることができる。

推論規則

自然演繹法では,前提となる命題から,定められた推論規則を用いて,次々に新しい命題を導いてゆく。ある命題に推論規則を適用して別の命題を導くことを,導出と言う。前提が正しければ,推論規則によって導出命題も正しい。従って,ある推論が妥当であることを証明するためには,与えられた前提に対して,推論規則を用いて次々と命題を生成してゆき,最終的に結論に一致する命題を導けばよい。


攻略法

推論規則は,前提から結論に向かって,いわば前向きに適用されてゆく。一方で,ある命題を導きたい時に,その前段階としてその命題を導くための前段階の命題を考えることができる。これは,ある目標に到達するために,その副目標を設定することを意味する。推論規則が前向きに適用されるのに対して,このような副目標の設定は,結論から前提に向かって,すなわち後ろ向きに設定される。このような副目標の設定を行うのが,攻略法である。


単純な問題は,攻略法を用いず,推論規則を前向きに適用してゆくだけで解ける。しかし,複雑な問題になると,後ろ向きに副目標を設定して,まずはその副目標となる命題を導出するところまで前向き推論を進める,すなわち,推論規則を適用してゆくといったように,前提から結論の間に中間的な副目標を設定して,導出の橋渡しをしてゆく必要が出てくる。

論理結合子

命題は,アルファベット1文字を使って現す。2つの命題を,以下で述べる論理結合子を使って,より複雑な命題を作ることができる。前述の“P→Q”という命題は,PとQという2つの命題を,→という論理結合子を使ってつなげた命題である。

基本となる論理結合子は,以下の4種類がある。

∧	論理積	かつ
∨	論理和	または
¬	¬	でない
→	含意	ならば

導出過程(副証明なし)

導出とは,それぞれの論理結合子を,はずしたり,加えたりして,新しい命題を生成してゆくことである。はずしかた,加え方の規則が,推論規則となる。それぞれの論理結合子に対して,基本的に導入と除去という2つの推論規則がある。

ここで,まずは,以下の推論規則を確認いただきたい。

∧除去
∧導入
∨除去
∨導入
→除去
¬除去

基本的には,それぞれの推論規則に対応するような形で,後ろ向きに副目標を設定する攻略法がある。

例えば,前述の以下の推論は,→除去と∧導入という2つの推論規則を使用することで,2段階の導出で証明することができる。

P→Q	Prem
P	Prem
────────
Q	2つの前提に→除去(→elim)を適用
P∧Q	Pという前提とQという導出命題に∧導入(∧intro)を適用

■演習■ ではここで,実際に学習支援システムを使った演習に取り組もう。

導出過程(副証明あり)

残りの2つの推論規則は,副証明と共に用いられる。

→導入
¬導入

副証明とは,ある前提(Prem)を仮定することにより,推論を進める方法である。仮定される前提は,もともとの前提とは独立に設定されるので,その命題が正しいことは保証されない。従って,仮定された前提に基づき導出された命題もまた,正しいことが保証されない。これらのいわばグレーの命題は,正しいことが保証されている命題群とは別に扱わなければならない。

正しいことが保証されている命題群からなる証明系列を主証明と呼び,それに対して,仮定を前提とした正しいことが保証されなくなった命題群を含む証明系列を,主証明に対する副証明と呼ぶ。


導出の記述において,副証明は主証明と区別するために,右にインデントをかけて記述される。


→導入

副証明は仮定された前提(Prem)から始まり,仮定は,必ず副目標と共に設定される。例えば,P→Qという命題を導出したい時に,副証明の中でPを仮定し,Qを副目標に設定する。

	P	Prem

	Q	副目標
──────
P→Q

副証明の中で,副目標として設定されたQが導出されれば,前提としてのP,そこから導出されたQをもって,主証明にP→Qを戻すことができる。この場合,P→Qは,正しいことが保証された命題である。

¬導入

同じように,¬導入を考えてみよう。¬導入は,一般に背理法と呼ばれる推論である。

例えば,Pが仮定された副証明の中で,矛盾(⊥)が生じたら,主証明に¬Pを返しても良い。この場合,¬Pは正しいことが保証された命題である。

	P	Prem

	⊥	副目標
──────
¬P

矛盾は,⊥導入という特殊な推論規則によって導出される。具体的には,ある命題Q(この命題は,論理結合子で接続された命題でもかまわない)と,その否定,¬Qが同時に副証明の中に出てきたら,そこから矛盾,⊥が導かれる。

	Q	
	¬Q
──────
	⊥	⊥導入

背理法という論法がある。あることを証明したいために,そのことの否定を仮定して矛盾が導かれたら,そのことが証明されたとする論理である。背理法は,この自然演繹の枠組みでは,以下のように扱われる。

例えば,Pを証明したい時には,次のような形に持ち込む。

	¬P	Prem

	⊥	副目標
──────
¬¬P      副目標
P

ReitとRepetition

最後に,ReitとRepetitionという2つの推論規則を確認しておこう。

Reitに関しては,主証明から副証明,副証明からさらにその副証明へ命題を送ることはできるが,逆は行えないので,注意が必要である。


■演習■ ではここで,実際に学習支援システムを使った演習に取り組もう。