(01)
多くの古典論理の恒真式は直観主義論理には証明できない。排中律 P∨~Pだけでなく、二重否定除去 ~~P→P や、
パースの法則 ((P→Q)→P)→P などがその例である。
(ウィキペディア)
然るに、
(02)
「真理値表(Truth table)」により、
①((真→真)→真)→真
②((真→偽)→真)→真
③((偽→真)→偽)→偽
④((偽→偽)→偽)→偽
に於いて、
① は「真」であり、
② も「真」であり、
③ も「真」であり、
④ も「真」である。
cf.
「恒真式(トートロジー)」。
従って、
(02)により、
(03)
①((P→真)→P)→P
②((P→偽)→P)→P
に於いて、
① は「真」であり、
② も「真」である。
従って、
(01)(03)により、
(04)
①((P→Q)→P)→P
①((PならばQ)ならばP)ならばPである。
といふ「パースの法則」は、
①((Pならば、Qであらうと、なからうと)Pなので)Pである。
といふことに、他ならない。
従って、
(05)
①((P→Q)→P)→P
①((PならばQ)ならばP)ならばPである。
①((Pならば、Qであらうと、なからうと)Pなので)Pである。
といふ「パースの法則」は、「当り前」のことを、述べてゐるに過ぎない。
然るに、
(06)
「真理値表(Truth table)」によらず、
「命題計算(propositional calculus)」によって、例へば、
「P→P(PならばPである)」といふ「同一律」が「恒真式(トートロジー)」である。
といふことを示したいのであれば、、
1(1)P A
(2)P→P 11CP
に於ける、
(2)P→P 11CP
のやうに、
(#)結論 ##CP
を得た際に、
(#)の「左側」が「空欄」であるやうに、すれば良い。
然るに、
(07)
1 (1) (P→Q)→P A
2 (2) ~P∨Q A
2 (3) P→Q 2含意の定義
12 (4) P 13MPP
1 (5) (~P∨Q)→P 24CP
1 (6)~(~P∨Q)∨P 5含意の定義
7 (7)~(~P∨Q) A
7 (8) P&~Q 7ド・モルガンの法則
7 (9) P 8&E
ア(ア) P A
1 (イ) P 679アア∨E
(ウ)((P→Q)→P)→P 1イCP
従って、
(05)(06)(07)により、
(08)
① P→P
②((P→Q)→P)→P
に於いて、
①「同一律」は、 「恒真式(トートロジー)」であって、
②「パースの法則」も「恒真式(トートロジー)」である。
然るに、
(09)
1 (1) (P→Q)→P A
2 (2) ~P∨Q A
2 (3) P→Q 2含意の定義
12 (4) P 13MPP
1 (5) (~P∨Q)→P 24CP
1 (6)~(~P∨Q)∨P 5含意の定義
7 (7)~(~P∨Q) A
7 (8) P&~Q 7ド・モルガンの法則
7 (9) P 8&E
ア(ア) P A
1 (イ) P 679アア∨E
(ウ)((P→Q)→P)→P 1イCP
に於いて、
2 (3) P→Q 2含意の定義
1 (6)~(~P∨Q)∨P 5含意の定義
7 (8) P&~Q 7ド・モルガンの法則
を用ひない場合は、「数学の定理の証明の過程で、他の定理を、証明する」やうなものなので、その分、「証明(10)」のやうに、「証明が長くなる」。
(10)
1 (1) (P→ Q)→P A
2 (2) ~P∨ Q A
3 (3) P&~Q A
4 (4) ~P A
3 (5) P 3&E
34 (6) ~P&~P 45&I
4 (7) ~(P&~Q) 36RAA
8 (8) Q A
3 (9) ~Q 3&E
3 8 (ア) Q&~Q 89&I
8 (イ) ~(P&~Q) 3アRAA
2 (ウ) ~(P&~Q) 2478イ∨EI
エ (エ) P A
オ (オ) ~Q A
エオ (カ) P&~Q エオ&I
2 エオ (キ)~(P&~Q)&(P&~Q) ウカ&I
2 エ (ク) ~~Q オキRAA
2 エ (ケ) Q クDN
2 (コ) P→ Q エケCP
12 (サ) P 1コMPP
1 (シ) (~P∨Q)→ P 23CP
ス (ス) (~P∨Q)&~P A
ス (セ) (~P∨Q) ス&E
1 ス (ソ) P シセMPP
ス (タ) ~P ス&E
1 ス (チ) P&~P ソタ&I
1 (ツ) ~~P シチRAA
1 (テ) P ツDN
1 (ト) ~(~P∨Q)∨P テ∨I
ナ (ナ) ~(~P∨Q) A
ニ (ニ) ~P A
ニ (ヌ) ~P∨Q 二∨I
ナ二 (ネ)~(~P∨Q)&(~P&Q) ナニ&I
ナ (ノ) ~~P 二RAA
ナ (ハ) P ノDN
マ(マ) P A
1 (ヤ) P トナハママ∨I
(イ)((P→Q)→P)→P 1ヤCP
然るに、
(10)により、
(11)
(イ)((P→Q)→P)→P 1ヤCP
といふ「結論(パースの法則)」を得る「過程」で、
2 エ (ク) ~~Q オキRAA
2 エ (ケ) Q クDN
1 (ツ) ~~P シチRAA
1 (テ) P ツDN
ナ (ノ) ~~P 二RAA
ナ (ハ) P ノDN
といふ「具合」に、「計3回、DN(二重否定除去)」を用ひてゐる。
然るに、
(01)により、
(12)
もう一度、確認すると、
直観主義論理では、「二重否定除去 ~~P→P」や、「パースの法則 ((P→Q)→P)→P」などが「証明」出来ない。
従って、
(11)(12)により、
(13)
(イ)((P→Q)→P)→P 1ヤCP
といふ「結論(パースの法則)」を得る「過程」で、
2 エ (ク) ~~Q オキRAA
2 エ (ケ) Q クDN
1 (ツ) ~~P シチRAA
1 (テ) P ツDN
ナ (ノ) ~~P 二RAA
ナ (ハ) P ノDN
といふ「具合」に、「計3回、DN(二重否定除去)」を用ひてゐるが、
直観主義論理では、固より「DN(二重否定除去)」そのものを「認めない」。
従って、
(09)~(13)により、
(14)
直観主義論理では、「DN(二重否定除去)」そのものを「認めない」が故に、
1 (1) (P→Q)→P A
2 (2) ~P∨Q A
2 (3) P→Q 2含意の定義(二重否定除去に、依存する。)
12 (4) P 13MPP
1 (5) (~P∨Q)→P 24CP
1 (6)~(~P∨Q)∨P 5含意の定義(二重否定除去に、依存する。)
7 (7)~(~P∨Q) A
7 (8) P&~Q 7ド・モルガンの法則(二重否定除去に、依存する。)
7 (9) P 8&E
ア(ア) P A
1 (イ) P 679アア∨E
(ウ)((P→Q)→P)→P 1イCP
といふ「(パースの法則の)証明」を、「直観主義論理」は認めない。
といふ、ことになる。
然るに、
(15)
(ⅱ)
1 (1) P→ Q A
2 (2) ~Q A
3(3) P A
1 3(4) Q 13MPP
123(5) ~Q&Q 24&I
12 (6)~P 35RAA
1 (7)~Q→~P 26CP
(ⅲ)
1 (1) ~Q→~P A
2 (2) P A
3(3) ~Q A
1 3(4) ~P 13MPP
123(5) P&~P 24&I
12 (6)~~Q 35RAA
12 (7) Q 6DN
1 (8) P→ Q 27CP
従って、
(15)により、
(16)
② P→ Q(Pであるならば、Qである。)
③ ~Q→~P(Qでないならば、Pでない。)
に於いて、
②=③ は「対偶(Contraposition)」である。
然るに、
(17)
(ⅲ)
1 (1) ~Q→~P A
2 (2) P A
3(3) ~Q A
1 3(4) ~P 13MPP
123(5) P&~P 24&I
12 (6)~~Q 35RAA
12 (7) Q 6DN
1 (8) P→ Q 27CP
の場合は、
12 (6)~~Q 35RAA
12 (7) Q 6DN
に於いて、「DN(二重否定除去)」を、用ひてゐる。
従って、
(14)~(17)により、
(18)
①((P→Q)→P)→P といふ「パースの法則」。
②((P→Q)⇔(~Q→~P))といふ「対偶」。
に於いて、「直観主義論理」は、
① だけでなく、
② も「認めない」。
といふ、ことになる。
然るに、
(19)
①((P→Q)→P)→P
①((PならばQ)ならばP)ならばPである。
①((Pならば、Qであらうと、なからうと)Pなので)Pである。
といふ「どうでも良い法則」は、ともかく、
②((P→Q)⇔(~Q→~P))
②((PであるならばQである)と(QでないならばPでない)とは、同じことである。)
といふ「対偶」をも認めない「直観主義論理」は、「あまりにも、変な論理である」。
といふ風しか、思へない。
従って、
(01)~(19)により、
(20)
多くの古典論理の恒真式は直観主義論理には証明できない。排中律 P∨~Pだけでなく、二重否定除去 ~~P→P や、
パースの法則 ((P→Q)→P)→P などがその例である。
といふ「説明」は、『私には、全く、理解できない所の、謎』である。