(01)
パースの法則:((A→B)→A)→A
直観主義論理NJに、パースの法則を公理図式として加えると古典論理になるという話を聞いたので少し考えた。たしかに、((A→⊥)→A)→A を前提することで、((A→⊥)→⊥)→A が導出できるっぽい。つまり、二重否定除去が導出できるから、これで古典になる。
(パースの法則 - Skinerrian's blog)
然るに、
(02)
私の論理学のレベルは、「直観主義論理NJに、パースの法則を公理図式として加えると古典論理になる。」といふことを考へるまでには、至っていません。
然るに、
(03)
44├ ~P∨P
1 (1) ~(~P∨P) A
2(2) ~P A
2(3) ~P∨P 2∨I
12(4) ~(~P∨P)&
(~P∨P) 13&I
1 (5) ~~P 24RAA
1 (6) P 5DN
1 (7) ~P∨P 6∨I
1 (8) ~(~P∨P)&
(~P∨P) 17&I
(9)~~(~P∨P) 18RAA
(ア) ~P∨P 9DN
(E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳、1973年、66頁改)
然るに、
(04)
系Ⅰ:任意の連式は、それがトートロジー的であるときまたそのときに限って導出可能である。
(E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳、1973年、114頁)
従って、
(03)(04)により、
(05)
①├ ~P∨P
といふ「排中律」は、「恒真式(トートロジー)」である。
然るに、
(06)
(1) ~P∨P TI(排中律)
2 (2) ~P A
2 (3) ~P∨Q 2∨I
2 (4) P→Q 3含意の定義
2 (5) (P→Q)&~P 24&I
2 (6)~(~(P→Q)∨ P) 5ド・モルガンの法則
7 (7) (P→Q)→ P A
7 (8) ~(P→Q)∨ P 7含意の定義
27 (9)~(~(P→Q)∨ P)&
(~(P→Q)∨ P) 68&I
2 (ア) ~((P→Q)→ P) 79RAA
2 (イ) ~((P→Q)→ P)∨P ア∨I
ウ(ウ) P A
ウ(エ) ~((P→Q)→ P)∨P ウ∨I
(オ) ~((P→Q)→ P)∨P 12イウエ∨E
(カ) ((P→Q)→ P)→P オ含意の定義
従って、
(05)(06)により、
(07)
①├ ~P∨P
②├ ((P→Q)→P)→P
に於いて、
① が「恒真式(トートロジー)」であるが故に、
② も「恒真式(トートロジー)」である。
従って、
(01)(07)により、
(08)
①「排中律」 が「恒真式(トートロジー)」であるが故に、
②「パースの法則」も「恒真式(トートロジー)」である。
といふ、ことになる。
然るに、
(09)
古典論理(こてんろんり, 英: classical logic)は形式論理の部類で、最も研究され最も広く使われている論理である。標準論理(英: standard logic)とも呼ばれる(ウィキペディア)。
従って、
(10)
私が知ってゐる「論理学(E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳)」は、「古典論理(標準論理)」であるに、違ひない。
従って、
(06)(10)により、
(11)
②├ ((P→Q)→P)→P≡((PであるならばQである)ならばPである)ならばPである。
といふ「定理(Theorem)」である所の「パースの法則」は、「古典論理(標準論理)」に属してゐる。
(12)
>直観主義論理NJに、パースの法則を公理図式として加えると古典論理になる。
といふことは、
古典論理から、パースの法則を公理図式から除くと、直観主義論理NJになる。
といふ、「意味」なのだろうか(?)。
(13)
「命題計算」は、多分、「詰将棋」に似てゐます。
(1) ~P∨P TI(排中律)
2 (2) ~P A
2 (3) ~P∨Q 2∨I
2 (4) P→Q 3含意の定義
2 (5) (P→Q)&~P 24&I
といふ「5手」に、気付くことが出来れば、後は、
2 (6)~(~(P→Q)∨ P) 5ド・モルガンの法則
7 (7) (P→Q)→ P A
7 (8) ~(P→Q)∨ P 7含意の定義
27 (9)~(~(P→Q)∨ P)&
(~(P→Q)∨ P) 68&I
2 (ア) ~((P→Q)→ P) 79RAA
2 (イ) ~((P→Q)→ P)∨P ア∨I
ウ(ウ) P A
ウ(エ) ~((P→Q)→ P)∨P ウ∨I
(オ) ~((P→Q)→ P)∨P 12イウエ∨E
(カ) ((P→Q)→ P)→P オ含意の定義
といふ「やり方」が、「見えて来ます」。
令和02年02月23日、毛利太。
0 件のコメント:
コメントを投稿