命題論理の自然演繹　[数学についてのwebノート]

命題論理の自然演繹　：　トピック一覧　　

・自然演繹で認められた操作　
・命題論理の自然演繹：推論規則公理一覧・推論規則公理の必要最小限のセット　　　
　・推論規則：⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨除去則・￢導入則・￢除去則（￢の定義）　
　　　　　　　背理法・二重否定除去律・矛盾除去
　・公理　　：排中律　
　・定理一覧　：
　・派生推論規則一覧　

　※命題論理構文論関連ページ：命題論理の構文論　　　
　※命題論理関連ページ：命題論理の論理式 /命題論理の意味論[真理値/真理関数/真理値表/論理式の真理値の決定原理/真理値分析/恒真式・恒偽式 ] 　　
　※論理関連ページ：論理記号　
　*　論理目次/総目次/更新履歴　

※述語論理の場合は、林晋,鹿島亮を参照。

命題論理の形式的体系：ゲンツェンの自然演繹

【認められる記号】

　「自然演繹」という「命題論理の形式的体系」において使用が認められている記号は、下記のみ。
　命題記号、論理記号、⋏（矛盾）

【認められる表現】

　「自然演繹」という「命題論理の形式的体系」において使用が認められている表現は、下記のみ。
　論理式、⋏（矛盾）

【認められた操作】

　「自然演繹」という「命題論理の形式的体系」において認められている操作は、下記のみ。

　(1)公理書き出し
　　　　公理を新たに書き出す操作。

　(2)仮定書き出し
　　　　任意の論理式、⋏（矛盾）を、《仮定》として新たに書き出す操作。
　　　　* あれ？矛盾を自分で仮定したらまずいのかな？
　　　　　　推論規則にしたがって矛盾に書き換えるだけ？
　　　　→いや、前原先生、p.59で、矛盾を仮定しておられる。
　　　　　[∨導入則・￢導入則・￢除去則・￢￢除去則のみを用いた【矛盾に関する規則】の導出]。

　(3)推論規則による書き換え
　　　　・推論規則のいずれかを使って、
　　　　　すでに書き出された論理式、⋏（矛盾）を、
　　　　　新たな論理式、⋏（矛盾）へ書き換える操作。

　　　　・ただし、その際、使った推論規則の指示にしたがって、《仮定》を落とすか、引き継ぐかすること。
　　　　　　　[野矢『論理学』1-2-3-公理系のサンプル2(p.61)]　　

【推論規則・公理一覧】　　

【推論規則：⇒導入】　

	[A] ： B
		(⇒-導入)
	A⇒B

　*　どういうこと？→ ⇒導入則

【推論規則：⇒除去】　

	A　A⇒B
		(⇒-除去)
	B

　*　どういうこと？→ ⇒除去則　

【推論規則：∧導入】　

	A　　　B
		(∧導入)
	A∧B

　*　どういうこと？→ ∧導入則

【推論規則：∧除去】

(1)　

A∧B
	(∧除去)
A

(2)　

A∧B
	(∧除去)
B

　*　どういうこと？→ ∧除去則　

【推論規則：∨導入】

(1)

A
	(∨導入)
A∨B

(2)　

B
	(∨導入)
A∨B

　*　どういうこと？→ ∨導入則

【推論規則：∨除去】

A∨B	[A] ： C	[B] ： C
			(∨除去)
C

　*　どういうこと？→ ∨除去則　

【文献】
　・前原昭二『記号論理入門』2章演繹：述語論理全般のなかに埋め込まれている。
　　　§1.→について(pp.37-41):導入則・除去則はp.40;
　　　§2.∧について(pp.41-43):導入則・除去則はp.42;
　　　§3.∨について(pp.43-43):導入則・除去則はp.43;　
　　　§4.￢について(pp.45-46):導入則・除去則はp.45;　.45-46):導入則・除去則はp.45;　
　　　§7.矛盾について(pp.53-56):「⋏に関する推論規則：はp.56;
　　　§8.排中律について(pp.56-59):公理「排中律」p.52;排中律の代わりに二重否定の除去則でもよい。(pp.52- 59)　
　・高崎『数理論理学入門』VI. 論理の形式化　1. 形式化の考え方;III. VII. 自然演繹（その１）1. 命題論理の形式化（NK,NJ）
　・戸田山『論理学をつくる』9.1自然演繹法をつくる (pp.214-223);9.2他の結合子のための推論規則(pp.223-233);9.3矛盾記号を導入したほうがよいかも(pp.233- 235)：命題論理の範囲で。
　・鹿島『数理論理学』2章自然演繹-2.2導出図-図2.2 自然演繹の推論規則一覧(p.29)　:述語論理全般のなかに埋め込まれている。
　・野矢『論理学』1 -2-2命題論理の完全な公理系の例(pp.65 -66):一つの意味論に対して、複数の公理系をつくれる。
　　　　　　　　　　1-2-2-公理系のサンプル1(pp.58-60);1-2-3-公理系LP2(p.71): ヒルベルト流
　　　　　　　　　　1-2-3-公理系のサンプル2(pp.60-65);1-2-3公理系LP(pp.66 -71)　:ゲンツェン流　
　・野矢『入門！論理学』第5章命題論理のやりかた(pp.139-192).
　　　　　　　　　　　　　　　「標準的な命題論理の体系」(p.146).
　　　　　　　　　　　　　　　「自然演繹」（p.188）
　・戸次『数理論理学』7.2一階命題論理の体系SK(pp.150 -154):ヒルベルト流
　　　　　　　　　　　　8章自然演繹(pp.174-189):ゲンツェン流　
　・清水『記号論理学』§3.4ゲンツェン流の公理系L_G:(pp.93-95)
　・van Dalen,Logic and Structure(3rd ed.) 1.4Natural Deduction(pp.29-39):∨がない;1.6The Missing Connectives(pp.48-53)∨が入る

【推論規則：￢導入】 　　

	[A] ： ⋏
		(￢導入)
	￢A

　*　どういうこと？→ ￢導入則

【推論規則：￢除去】

	A ￢A
		(￢除去)
	⋏

　*　どういうこと？→ ￢除去則　

【推論規則：背理法】 　　　　

	[￢A] ： ⋏
		(背理法)
	A

　*　どういうこと？→ 背理法　

【推論規則：二重否定除去律】

	￢￢A
		(二重否定除去律)
	A

　*　どういうこと？→ 二重否定除去律　　

【推論規則： ⋏　】 　　　　

	⋏

	A

　*　どういうこと？→【推論規則⋏】

【公理：排中律】

　　　　A∨￢A　

　*　どういうこと？→ 排中律　　
　*　使用例は？→対偶律(2)証明(step07)
　

→　命題論理の自然演繹　：トピック一覧　
→　命題論理のシンタックス　：トピック一覧
→　総目次　　

【命題論理における自然演繹の推論規則・公理の最小限のセット】 　

1. 上記リストアップした「命題論理における自然演繹の推論規則・公理」は、必要最小限のセットではない。冗長な項目も含んでいる。

2. では、冗長な項目を削ぎ落として、必要最小限の項目だけを集めると、どんなセットになるの？

　　コレデス！とセットを一つ提示できれば、話は速いのだけど、
　　事情はもっと複雑になっている。残念ながら。

　　実は、
　　命題論理における自然演繹の推論規則・公理の必要最小限のセットは、
　　唯一つ存在するのではなく、
　　数タイプ存在する。

　　そのうち、3タイプを列挙すると、

　　　【必要最小限のセット：type1】
　　　　　⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨ 除去則・￢導入則・￢除去則・背理法　　
　　　【必要最小限のセット：type2】
　　　　　⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨ 除去則・￢導入則・￢除去則・￢￢除去則
　　　【必要最小限のセット：type3】
　　　　　⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨ 除去則・￢導入則・￢除去則・矛盾に関する規則・排中律　

3.
　　・これら【必要最小限のセット】を見比べると、
　　　　全タイプに共通しているのは、
　　　　　⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨除去則・￢導入則・￢除去則

　　・この共通項目に背理法を付け足したのが【必要最小限のセット：type1】　
　　　この共通項目に￢￢除去則を付け足したのが【必要最小限のセット：type2】　
　　　この共通項目に矛盾に関する規則・排中律を付け足したのが【必要最小限のセット：type3】

4.　命題論理における自然演繹の推論規則・公理の必要最小限のセットに何タイプもあるのは、ちょっぴり不思議。
　どういう事情があるの？

　　・共通項目に背理法を付け足して【必要最小限のセット：type1】をつくると、
　　　このなかの項目だけを組み合わせて、￢￢除去則、矛盾に関する規則・排中律をつくれてしまう(派生推論規則)。
　　　　　　　　　　 *　どうして　→　詳細　
　　　だから、【必要最小限のセット：type1】に、￢￢除去則、矛盾に関する規則・排中律を付け加えるのは冗長。
　　
　　・共通項目に￢￢除去則を付け足して【必要最小限のセット：type2】をつくると、
　　　このなかの項目だけを組み合わせて、背理法、矛盾に関する規則・排中律をつくれてしまう(派生推論規則)。
　　　　　　　　　　 *　どうして　→　詳細　
　　　だから、【必要最小限のセット：type2】に、背理法、矛盾に関する規則・排中律を付け加えるのは冗長。

　　・共通項目に矛盾に関する規則・排中律を付け足して【必要最小限のセット：type3】をつくると、
　　　このなかの項目だけを組み合わせて、背理法、￢￢除去則をつくれてしまう(派生推論規則)。
　　　　　　　　　　 *　どうして　→　詳細　
　　　だから、【必要最小限のセット：type3】に、背理法、￢￢除去則を付け加えるのは冗長。

　　要するに、

　　　共通項目のみをインストールした《論理システム》に対して、
　　　　　　背理法のみを追加インストール
　　　　　　￢￢除去則のみを追加インストール　
　　　　　　矛盾に関する規則・排中律のみを追加インストール
　　　のいずれをおこなっても、アップグレードされた《論理システム》は、同一機能を達成。
　　　
　　　だから、この同一機能を達成するために必要最小限のインストール項目を、冗長なくリストアップすると、
　　　　　　共通項目に加えて、背理法をインストール
　　　　　　共通項目に加えて、￢￢除去則を追加インストール
　　　　　　共通項目に加えて、矛盾に関する規則・排中律を追加インストール
　　　の三通り出てくる、

　　というだけの話。

【自然演繹における《公理》《定理》と《推論規則》《派生推論規則》の関係】
　・《推論規則》は、どれも、《公理》に書き換えられる。
　・《派生推論規則》は、どれも、《定理》に書き換えられる。
　・⇒を含む《公理》は、どれも、《推論規則》に書き換えられるが、
　　⇒を含まない《公理》（たとえば、排中律）は、どれも、《推論規則》に書き換えられない。
　・⇒を含む《定理》は、どれも、《派生推論規則》に書き換えられるが、
　　⇒を含まない《定理》は、どれも、《派生推論規則》に書き換えられない。

　・野矢『入門！論理学』「だけど、実は推論規則は私たちの体系ではぜんぶ論理命題として書き換えられるんですね。（逆はいえません。つまり、論理命題を推論規則の形に書き換えようとすると、うまくいかないものが出てきます。たとえば、排中律・・・）その理由は、条件法の導入則があるからです。…正確を期すためにもう一押ししておきます。逆に、「□ならば△」が論理命題だとすると、こんどは「ならば取り」（肯定式）に従って、□という前提から△が必ず導けることになります。ということは、「□ならば△」の形の論理命題であれば、「□→△」は推論規則になるわけです。」(第5章p.152-3).

　・野矢『論理学』1-2-3公理系LP-「定理から派生規則への読み換え」(p.69)　

【「自然演繹の推論規則・公理」の証明図】
　自然演繹の証明図の書き方には、大まかに分けて、二通りの流儀がある。採用する流儀で、テキストを分類すると、下記のようになる。
　(A)標準的な流儀(特に名称なし)を採用：
　　　・前原昭二『記号論理入門』
　　　・高崎『数理論理学入門』
　　　・鹿島『数理論理学』
　　　・戸次『数理論理学』　
　　　・van Dalen,Logic and Structure(3rd ed.) 1
　(B)フィッチ・スタイル：
　　　・戸田山『論理学をつくる』　
　　　・バーバイズ・エチメンディ『論理学の基礎と演習』　（フィッチスタイルの証明図作成ソフトが付録についてくる）
　(C)証明図をそもそも使わない：　
　　・野矢『論理学』
　　・野矢『入門！論理学』

【主要テキストの「自然演繹の推論規則・公理」】
　・前原『記号論理入門』：
　　【必要最小限のセットtype3】
　　　　　⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨除去則・￢導入則・矛盾に関する規則・排中律
　　　§7(p.53)：￢導入則と￢除去則は、￢の定義「￢Aとは『A⇒⋏』のこと」と同じこと。
　　　　　　　　￢導入則と￢除去則は、
　　　　　　　　　　　⇒導入則・⇒除去則と￢の定義「￢Aとは『A⇒⋏』のこと」を組み合わせたものにすぎない。
　　　§8：・二重否定除去法則の証明（￢除去則・矛盾に関する規則・排中律を使用）。(p.57)
　　　　　　・「二重否定の除去というものは、排中律と矛盾の公理の双方を合わせたものと同等ということになります」(p.59)
　　　　　　　　　　　・排中律を公理とせず、二重否定除去を推論規則としたときの、排中律の証明(p.58)
　　　　　　　　　　　・排中律を公理とせず、二重否定除去を推論規則としたときの、矛盾の公理の証明(pp.58-9)
　　　*
　　　　　

	￢￢A
		(￢￢除去)
	A

　　　　を推論規則としてもよいと指摘。(pp.52-59証明付)　　
　　　7章§2.4(p.125)「⋏や⋎という記号は、ある一つの命題変数Aを固定した上で、それぞれA∨￢AおよびA∧￢Aを表す略記号と考えるのであります。そのように考えてもよいという理由は、この§の3および1における排中律ならびに矛盾律によるのです。」

　・高崎『数理論理学入門』III. VII. 自然演繹（その１）1. 命題論理の形式化（NK,NJ）
　　　【必要最小限のセットtype3】
　　　　　　1.2-3 背理法・二重否定・排中律の関連。「背理法は￢導入と「二重否定除去」￢￢φ|-φを組み合わせたもの」
　　　　　　2.1[例4]で、二重否定除去則を演繹。2.2[例6]で背理法を演繹。

[A] ： ⋏
	(￢導入)
￢A

　・戸田山『論理学をつくる』9.1(pp.214-223);9.2(pp.223-233);9.3(pp.233-235)
　　　当初は、矛盾記号不使用の【￢導入則】を用いた【必要最小限のセットtype2】を提示。
　　　　　　　　「￢intoro: 導出DがAからの矛盾の導出を一項目として含んでいたら、否定AをDの一項目として書き加えてよい。(p.227)」
　　　9.3.2が、矛盾記号を導入し、【必要最小限のセットtype2】を提示(p.235)。
　　　　　　　「我々の￢introという規則を次の二つの規則に分けてしまう。￢introの代わりにこの二つの規則￢intro*と￢elim*を使うことにすれば、この演繹は右のようにとても簡単になる。」(p.234)
　　　　　　　　ここから、当初提示していたものも、【必要最小限のセットtype2】を意図していると理解できる。
　　　9.2.5は、【￢導入則】を用いた【必要最小限のセットtype2】において、排中律が定理になると指摘(p.232)。

　・鹿島『数理論理学』
　　　【必要最小限のセットtype1】+【矛盾に関する規則】
　　　　ないし、
　　　【必要最小限のセットtype3】－排中律＋背理法
　・戸次『数理論理学』定義8.19NKの推論規則(p.187)【必要最小限のセットtype1】
　　　　　　ただし、￢の定義「￢Aとは『A⇒⋏』のこと」。
　　　　　・定理8.22(p.187) で、【必要最小限のセットtype1】のなかで、「⋏に関する推論規則」が定理になると指摘。
　　　　　・練習問題8.21(p.187)で、【必要最小限のセットtype1】のなかで、排中律が定理になると指摘。
　　　　　・戸次の略記法：
　　　　　　　　EFQ：矛盾に関する規則[定義8.18NJの推論規則(p.186)]
　　　　　　　　DNE:自然演繹においては背理法[。定義8.19NKの推論規則(p.187)]。
　　　　　　　　　　　ヒルベルト流形式化においては、二重否定除去律「￢￢A⇒A」。[定義7.21]
　　　　　　　　RAA*：ヒルベルト流形式化において、背理法「(￢A⇒⋏)⇒A」を指す。　　　
　　　　　　　　　　　　ただし、ヒルベルト流形式化において、
　　　　　　　　　　　　　「(RAA*)と(DNE)は実は同一の論理式である。
　　　　　　　　　　　　　　　したがって二重否定除去律とは、ある種の背理法と考えることができる」[解説7.28]
　　　　　　　　　　　　　とある。
　　　　　　　　　　　　　また、定義8.20は、
　　　　　　　　　　　　　　NKの「(DNE)は…という一種の背理法であり、
　　　　　　　　　　　　　　ヒルベルト流証明論における(DNE)(RAA*)に相当するが、
　　　　　　　　　　　　　　　こちらも自然演繹では⇒を用いずに、推論規則として与えられる」と指摘。
　　　　　　　　LEM:排中律。自然演繹・ヒルベルト流共通。[p.170;187]　　　　　　　
　　　　　　　　HM:最小論理のヒルベルト流形式化。
　　　　　　　　HJ:直観主義論理のヒルベルト流形式化。
　　　　　　　　HK:古典論理のヒルベルト流形式化。
　　　　　　　　NM:最小論理の自然演繹による形式化。(⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨除去則・￢の定義)
　　　　　　　　NJ:直観主義論理の自然演繹による形式化。
　　　　　　　　NK:古典論理の自然演繹による形式化。
　　　　　・7.8古典論理の体系HK(pp.165-173):ヒルベルト流
　　　　　　　　　　　　　HK=HM+DNE二重否定除去律 = HM+EFQ矛盾に関する推論規則+LEM排中律(pp.172-3)
　　　　　・9.4HMとNMの等価性(pp.210-212):NM=HM;
　　　　　・9.5HJとNJ、HKとNKの等価性(p.213):HJ=NJ,HK=NK。
　　　　　　「定理9.3.1よりHJの(EFQ)とNJの(EFQ)は等価であり、また、HKの(DNE)とNKの(DNE)は等価であるため、いずれも自明である」
　　　　　・以上をあわせると、NK=NM+DNE背理法=NM+EFQ矛盾に関する推論規則+LEM排中律

　・van Dalen,Logic and Structure(3rd ed.) 1.4Natural Deduction(pp.29-39)
　　　【必要最小限のセットtype1】+【矛盾に関する規則】
　　　　　　ただし、￢の定義「￢Aとは『A⇒⋏』のこと」。
　　　　　
　・野矢は、矛盾記号の使用を回避しようとしているため、特異。￢除去則がなかったりする。　
　・野矢は、他のテキストで「￢導入則」と呼ばれる推論規則も「背理法」と呼んでいる。
　　　[『論理学』1-2-3-完全な公理系の例-派生規則(p .69)　　
　・野矢『論理学』　
　　【必要最小限のセットtype2】－【￢除去則】
　　　　　　矛盾記号を不使用。￢導入則で、矛盾記号を、D∧￢Dとする
　　　　　　「A⇒(D∧￢D)から￢Aを導出してよい」
　・野矢『入門！論理学』
　　【必要最小限のセットtype2】－【￢除去則】
　　　　　　￢導入則で矛盾記号使用。
　　　　　「A∨B　￢A」から「B」を導出する規則・「A∨B　￢B」から「A」を導出する規則と取替え可能な規則として∨除去則を提示。(証明は、p.160)
　*　この件について、前原7章§2.4(p.125)は、「⋏や⋎という記号は、ある一つの命題変数Aを固定した上で、それぞれA∨￢AおよびA∧￢Aを表す略記号と考えるのであります。そのように考えてもよいという理由は、この§の3および1における排中律ならびに矛盾律によるのです。」

・清水『記号論理学』p.94
　矛盾記号不使用。公理に、弱化規則[→戸次]とカット。

→　命題論理の自然演繹　：トピック一覧　
→　命題論理のシンタックス　：トピック一覧
→　総目次　　

命題論理の自然演繹 ： トピック一覧

命題論理の形式的体系：ゲンツェンの自然演繹

命題論理の自然演繹　：　トピック一覧　　