(01)
ヒルベルトの演繹システムは、公理が多く、推論規則が少ないものです。そして、公理も、わけのわからない論理式となっています。例えば、
P→(Q→P)(Pならば(QならばP))
という論理式が公理として設定されています。つまり、この論理式を出発点として演繹を行って良い。ということです。多くの人は、この論理式の意味を飲みこめないでしょう。
(小島寛之、証明と論理に強くなる、2017年、136頁)
然るに、
(02)
次に、命題論理の自然演繹の「公理」です。面白いことに「公理」は一つもありません。ここに自然演繹の大きな特徴があります。「出発点とする公理が何もないのに、いったいどうやって演繹するんだ」という疑問が湧いてくるでしょう。
(小島寛之、証明と論理に強くなる、2017年、140頁)
(03)
自然演繹には「仮定の解消」(最初に仮定しておいて、あとでなかったことにする)という手続きがあり、それがなかなか理解しづらいことです。自然演繹は「仮定の解消」のおかげで公理なしに演繹システムとなり得ており、その意味で「仮定の解消」は自然演繹の本質だと言っても過言ではありません。
(小島寛之、証明と論理に強くなる、2017年、144頁)
然るに、
(04)
P→(Q→P)(Pならば(QならばP))
といふ「ヒルベルトの公理」に対する、「自然演繹」による「証明」は、次のやうになる。
(05)
(5)├ P→(Q→P)
1 (1) P 仮定
1 (2) P∨~Q 1∨導入
3 (3) P A
3 (4) ~Q∨ P 3∨導入
5 (5) ~Q A
5 (6) ~Q∨ P 5∨導入
1 (7) ~Q∨ P 23456∨除去
8 (8) Q&~P 仮定
9 (9) ~Q A
8 (ア) Q &除去
89 (イ) ~Q& Q 9ア&導入
9 (ウ)~(Q&~P) 8イ背理法
エ (エ) P 仮定
8 (オ) ~P 8&除去
8エ (カ) P&~P エオ&導入
エ (キ)~(Q&~P) 8カ背理法
1 (ク)~(Q&~P) 79ウエキ∨除去
ケ (ケ) Q 仮定
コ(コ) ~P 仮定
ケコ(サ) Q&~P ケコ&導入
1 ケコ(シ)~(Q&~P)&
(Q&~P) クサ&導入
1 ケ (ス) ~~P コシ背理法
1 ケ (セ) P ス二重否定
1 (ソ) Q→P ケセ条件法(仮定の解消)
(タ)P→(Q→P) 1ソ条件法(仮定の解消)
然るに、
(06)
① P├ P
② P→ P
といふ「式」は、それぞれ、
① Pだから、Pである。
② Pならば、Pである。
といふ、「意味」である。
cf.
同一律(law of identity)
然るに、
(07)
① Pだから、Pである。
② Pならば、Pである。
に於いて、
① であれば、 Pである。が、
② であっても、Pである。とは、限らない。
従って、
(06)(07)により、
(08)
① Pだから、Pである。
② Pならば、Pである。
に於いて、
① ≠ ② であって、
①=② ではない。
然るに、
(09)
① P├ P
② P→ P
に於いて、
① を、
② に、「書き換へ」ることを、「仮定の解消」といふ。
cf.
1(1)P 仮定
(2)P→P 11条件法
従って、
(10)
① P├(Q→P)
② P→(Q→P)
に於いて、
① を、
② に、「書き換へ」ることも、「仮定の解消」である。
然るに、
(05)により、
(11)
1 (1)P 仮定
1 (ソ) Q→P ケセ条件法(仮定の解消)
(タ)P→(Q→P) 1ソ条件法(仮定の解消)
であるものの、このことは、
① P├(Q→P):Pだから(QならばPである。)
② P→(Q→P):Pならば(QならばPである。)
に於いて、
① を、
② に、「書き換へ」ることに、相当する。
従って、
(01)(11)により、
(12)
① P├(Q→P):Pだから、QならばPである。
といふ「式」の、「仮定を解消」した「結果」が、
② P→(Q→P):Pならば、QならばPである。
といふ「ヒルベルトの公理」である。
然るに、
(13)
(a)
1 (1) Q→ P 仮定
2 (2) Q&~P 仮定
2 (3) Q 2&E
12 (4) P 13前件肯定
2 (5) ~P 2&除去
12 (6) P&~P 45&導入
1 (7)~(Q&~P) 26背理法
(b)
1 (1)~(Q&~P) 仮定
2 (2) Q 仮定
3(3) ~P 仮定
23(4) Q&~P 23&導入
123(5)~(Q&~P)&
(Q&~P) 14&導入
12 (6) ~~P 35背理法
12 (7) P 6二重否定
1 (8) Q→ P 27条件法
従って、
(13)により、
(14)
① ~(Q→~P)=QならばPである。
② ~(Q&~P)=QであってPでない。といふことはない。
に於いて、
①=② である。
然るに、
(15)
② QであってPでない。といふことはない。
といふのであれば、
② Qでない。
といふ場合については、何も、言ってゐない。
従って、
(14)(15)により、
(16)
① QならばPである。
といふのであれば、すなはち、
② QであってPでない。といふことはない。
といふのであれば、
② Qでない。
といふ場合については、
② Pである。
といふことを、「否定」しない。
従って、
(14)(15)(16)により、
(17)
① QならばPである。
といふ場合に、
① Qでない。
としても、
① Pでない。
といふことには、ならない。
従って、
(12)(17)により、
(18)
① P├ Q→P(Pだから、QならばPである。)
といふ「式」は、
① P├ Q→P(Pだから、Qであっても、Qでなくとも、Pである。)
といふ風に、「読むこと」が出来る。
従って、
(01)(18)により、
(19)
② Pならば、QならばPである。
といふ、「ヒルベルトの公理」は、
① Pだから、Qであっても、Qでなくとも、Pである。
としたら、
② Pならば、QならばPである。
といふ「意味」に、解することが出来る。
(20)
自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系 L は、証明の構文規則に関する次のような9つの基本的規則だけを持つ。
1.仮定の規則 "The Rule of Assumption"
2.モーダスポネンス "Modus Ponendo Ponens"
3.二重否定の規則 "The Rule of Double Negation"
4.条件付き証明の規則 "The Rule of Conditional Proof"
5.&-導入の規則 "The Rule of &-introduction"
6.&-除去の規則 "The Rule of &-elimination"
7.∨-導入の規則 "The Rule of ∨-introduction"
8.∨-除去の規則 "The Rule of ∨-elimination"
9.背理法 "Reductio Ad Absurdum"
(ウィキペディア)
然るに、
(21)
ジョン・レモンが開発した体系 L には、
3.否定否定式(MTT)
も、含まれてゐるため、実際には、「9つの基本的規則」ではなく、「10個の基本規則(The 10 primitive rules)」とするのが、正しい。
然るに、
(21)
(a)
1 (1) P→ Q A
2 (2) ~Q A
3(3) P A
1 3(4) Q 13MPP
123(5)~Q& Q 23&I
12 (6)~P 35RAA
1 (7)~Q→~P 26CP
(b)
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 67DN
1 (8) P→ Q 27CP
(22)
(a)
1 (1) P→ Q A
2 (2) ~Q A
3(3) P A
12 (4)~P 12MTT
123(5)~P& P 34&I
12 (6)~P 35RAA
1 (7)~Q→~P 26CP
(b)
1 (1) ~Q→~P A
2 (2) P A
2 (3) ~~P 2DN
4(4) ~Q A
12 (5)~~Q 13MTT
12 (6) Q 5DN
124(7) Q&~Q 46&I
12 (8)~~Q 47RAA
12 (9) Q 8DN
1 (ア) P→ Q 29CP
従って、
(21)(22)により、
(23)
MPPは、MTTに、「置き換へ」ることが出来、
MTTは、MPPに、「置き換へ」ることが出来る。
従って、
(23)により、
(24)
MTTは原始的規則と解される必要はなく、他の規則から導出される規則としてえられる(E.J.レモン著、竹尾治一郎・浅野楢英 訳、論理学初歩、78頁)し、MPPも、さうである。
然るに、
(25)
① 今日は水曜である。
② 今日は水曜であるか、明日は雨でない。
に於いて、
① が「本当(真)」ならば、
② も「本当(真)」である。
然るに、
(26)
① 今日は水曜である。従って、
② 今日は水曜であるか、明日は雨でない。
といふ「推論」を、「∨-導入の規則」といふ。
然るに、
(27)
「今日は水曜日である。従って、今日は水曜であるか、明日は雨でない。」
といふ「推論」を、「日常に於いて行ふ」ことは、「普通は、無い」。
然るに、
(05)により、
(28)
(5)├ P→(Q→P)
1 (1) P 仮定
1 (2) P∨~Q 1∨導入
3 (3) P A
3 (4) ~Q∨ P 3∨導入
5 (5) ~Q A
5 (6) ~Q∨ P 5∨導入
1 (7) ~Q∨ P 23456∨除去
8 (8) Q&~P 仮定
9 (9) ~Q A
8 (ア) Q &除去
89 (イ) ~Q& Q 9ア&導入
9 (ウ)~(Q&~P) 8イ背理法
エ (エ) P 仮定
8 (オ) ~P 8&除去
8エ (カ) P&~P エオ&導入
エ (キ)~(Q&~P) 8カ背理法
1 (ク)~(Q&~P) 79ウエキ∨除去
ケ (ケ) Q 仮定
コ(コ) ~P 仮定
ケコ(サ) Q&~P ケコ&導入
1 ケコ(シ)~(Q&~P)&
(Q&~P) クサ&導入
1 ケ (ス) ~~P コシ背理法
1 ケ (セ) P ス二重否定
1 (ソ) Q→P ケセ条件法(仮定の解消)
(タ)P→(Q→P) 1ソ条件法(仮定の解消)
であれば、
1 (2) P∨~Q 1∨導入
3 (4) ~Q∨ P 3∨導入
5 (6) ~Q∨ P 5∨導入
といふ「三つ」が、「∨-導入の規則」に、他ならない。
従って、
(01)(26)(28)により、
(29)
① 今日は水曜である。従って、
② 今日は水曜であるか、明日は雨でない。
といふやうな、「∨-導入の規則」を、認めないのであれば、
(タ)P→(Q→P) 1ソ条件法(仮定の解消)
といふ「結論」、すなはち、
P→(Q→P)(Pならば(QならばP))
といふ「ヒルベルトの公理」を、「自然演繹」では、「証明」出来ない。
といふ、ことになる。
従って、
(27)(28)(29)により、
(30)
「今日は水曜日である。従って、今日は水曜であるか、明日は雨でない。」
といふ「推論」は、「ナンセンス(無意味)」であるやうでゐて、それを認めない限り、
P→(Q→P)(Pならば(QならばP))
といふ「ヒルベルトの公理」を、「自然演繹」では、「証明」出来ない。
ヒルベルトの演繹システムは、公理が多く、推論規則が少ないものです。そして、公理も、わけのわからない論理式となっています。例えば、
P→(Q→P)(Pならば(QならばP))
という論理式が公理として設定されています。つまり、この論理式を出発点として演繹を行って良い。ということです。多くの人は、この論理式の意味を飲みこめないでしょう。
(小島寛之、証明と論理に強くなる、2017年、136頁)
然るに、
(02)
次に、命題論理の自然演繹の「公理」です。面白いことに「公理」は一つもありません。ここに自然演繹の大きな特徴があります。「出発点とする公理が何もないのに、いったいどうやって演繹するんだ」という疑問が湧いてくるでしょう。
(小島寛之、証明と論理に強くなる、2017年、140頁)
(03)
自然演繹には「仮定の解消」(最初に仮定しておいて、あとでなかったことにする)という手続きがあり、それがなかなか理解しづらいことです。自然演繹は「仮定の解消」のおかげで公理なしに演繹システムとなり得ており、その意味で「仮定の解消」は自然演繹の本質だと言っても過言ではありません。
(小島寛之、証明と論理に強くなる、2017年、144頁)
然るに、
(04)
P→(Q→P)(Pならば(QならばP))
といふ「ヒルベルトの公理」に対する、「自然演繹」による「証明」は、次のやうになる。
(05)
(5)├ P→(Q→P)
1 (1) P 仮定
1 (2) P∨~Q 1∨導入
3 (3) P A
3 (4) ~Q∨ P 3∨導入
5 (5) ~Q A
5 (6) ~Q∨ P 5∨導入
1 (7) ~Q∨ P 23456∨除去
8 (8) Q&~P 仮定
9 (9) ~Q A
8 (ア) Q &除去
89 (イ) ~Q& Q 9ア&導入
9 (ウ)~(Q&~P) 8イ背理法
エ (エ) P 仮定
8 (オ) ~P 8&除去
8エ (カ) P&~P エオ&導入
エ (キ)~(Q&~P) 8カ背理法
1 (ク)~(Q&~P) 79ウエキ∨除去
ケ (ケ) Q 仮定
コ(コ) ~P 仮定
ケコ(サ) Q&~P ケコ&導入
1 ケコ(シ)~(Q&~P)&
(Q&~P) クサ&導入
1 ケ (ス) ~~P コシ背理法
1 ケ (セ) P ス二重否定
1 (ソ) Q→P ケセ条件法(仮定の解消)
(タ)P→(Q→P) 1ソ条件法(仮定の解消)
然るに、
(06)
① P├ P
② P→ P
といふ「式」は、それぞれ、
① Pだから、Pである。
② Pならば、Pである。
といふ、「意味」である。
cf.
同一律(law of identity)
然るに、
(07)
① Pだから、Pである。
② Pならば、Pである。
に於いて、
① であれば、 Pである。が、
② であっても、Pである。とは、限らない。
従って、
(06)(07)により、
(08)
① Pだから、Pである。
② Pならば、Pである。
に於いて、
① ≠ ② であって、
①=② ではない。
然るに、
(09)
① P├ P
② P→ P
に於いて、
① を、
② に、「書き換へ」ることを、「仮定の解消」といふ。
cf.
1(1)P 仮定
(2)P→P 11条件法
従って、
(10)
① P├(Q→P)
② P→(Q→P)
に於いて、
① を、
② に、「書き換へ」ることも、「仮定の解消」である。
然るに、
(05)により、
(11)
1 (1)P 仮定
1 (ソ) Q→P ケセ条件法(仮定の解消)
(タ)P→(Q→P) 1ソ条件法(仮定の解消)
であるものの、このことは、
① P├(Q→P):Pだから(QならばPである。)
② P→(Q→P):Pならば(QならばPである。)
に於いて、
① を、
② に、「書き換へ」ることに、相当する。
従って、
(01)(11)により、
(12)
① P├(Q→P):Pだから、QならばPである。
といふ「式」の、「仮定を解消」した「結果」が、
② P→(Q→P):Pならば、QならばPである。
といふ「ヒルベルトの公理」である。
然るに、
(13)
(a)
1 (1) Q→ P 仮定
2 (2) Q&~P 仮定
2 (3) Q 2&E
12 (4) P 13前件肯定
2 (5) ~P 2&除去
12 (6) P&~P 45&導入
1 (7)~(Q&~P) 26背理法
(b)
1 (1)~(Q&~P) 仮定
2 (2) Q 仮定
3(3) ~P 仮定
23(4) Q&~P 23&導入
123(5)~(Q&~P)&
(Q&~P) 14&導入
12 (6) ~~P 35背理法
12 (7) P 6二重否定
1 (8) Q→ P 27条件法
従って、
(13)により、
(14)
① ~(Q→~P)=QならばPである。
② ~(Q&~P)=QであってPでない。といふことはない。
に於いて、
①=② である。
然るに、
(15)
② QであってPでない。といふことはない。
といふのであれば、
② Qでない。
といふ場合については、何も、言ってゐない。
従って、
(14)(15)により、
(16)
① QならばPである。
といふのであれば、すなはち、
② QであってPでない。といふことはない。
といふのであれば、
② Qでない。
といふ場合については、
② Pである。
といふことを、「否定」しない。
従って、
(14)(15)(16)により、
(17)
① QならばPである。
といふ場合に、
① Qでない。
としても、
① Pでない。
といふことには、ならない。
従って、
(12)(17)により、
(18)
① P├ Q→P(Pだから、QならばPである。)
といふ「式」は、
① P├ Q→P(Pだから、Qであっても、Qでなくとも、Pである。)
といふ風に、「読むこと」が出来る。
従って、
(01)(18)により、
(19)
② Pならば、QならばPである。
といふ、「ヒルベルトの公理」は、
① Pだから、Qであっても、Qでなくとも、Pである。
としたら、
② Pならば、QならばPである。
といふ「意味」に、解することが出来る。
(20)
自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系 L は、証明の構文規則に関する次のような9つの基本的規則だけを持つ。
1.仮定の規則 "The Rule of Assumption"
2.モーダスポネンス "Modus Ponendo Ponens"
3.二重否定の規則 "The Rule of Double Negation"
4.条件付き証明の規則 "The Rule of Conditional Proof"
5.&-導入の規則 "The Rule of &-introduction"
6.&-除去の規則 "The Rule of &-elimination"
7.∨-導入の規則 "The Rule of ∨-introduction"
8.∨-除去の規則 "The Rule of ∨-elimination"
9.背理法 "Reductio Ad Absurdum"
(ウィキペディア)
然るに、
(21)
ジョン・レモンが開発した体系 L には、
3.否定否定式(MTT)
も、含まれてゐるため、実際には、「9つの基本的規則」ではなく、「10個の基本規則(The 10 primitive rules)」とするのが、正しい。
然るに、
(21)
(a)
1 (1) P→ Q A
2 (2) ~Q A
3(3) P A
1 3(4) Q 13MPP
123(5)~Q& Q 23&I
12 (6)~P 35RAA
1 (7)~Q→~P 26CP
(b)
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 67DN
1 (8) P→ Q 27CP
(22)
(a)
1 (1) P→ Q A
2 (2) ~Q A
3(3) P A
12 (4)~P 12MTT
123(5)~P& P 34&I
12 (6)~P 35RAA
1 (7)~Q→~P 26CP
(b)
1 (1) ~Q→~P A
2 (2) P A
2 (3) ~~P 2DN
4(4) ~Q A
12 (5)~~Q 13MTT
12 (6) Q 5DN
124(7) Q&~Q 46&I
12 (8)~~Q 47RAA
12 (9) Q 8DN
1 (ア) P→ Q 29CP
従って、
(21)(22)により、
(23)
MPPは、MTTに、「置き換へ」ることが出来、
MTTは、MPPに、「置き換へ」ることが出来る。
従って、
(23)により、
(24)
MTTは原始的規則と解される必要はなく、他の規則から導出される規則としてえられる(E.J.レモン著、竹尾治一郎・浅野楢英 訳、論理学初歩、78頁)し、MPPも、さうである。
然るに、
(25)
① 今日は水曜である。
② 今日は水曜であるか、明日は雨でない。
に於いて、
① が「本当(真)」ならば、
② も「本当(真)」である。
然るに、
(26)
① 今日は水曜である。従って、
② 今日は水曜であるか、明日は雨でない。
といふ「推論」を、「∨-導入の規則」といふ。
然るに、
(27)
「今日は水曜日である。従って、今日は水曜であるか、明日は雨でない。」
といふ「推論」を、「日常に於いて行ふ」ことは、「普通は、無い」。
然るに、
(05)により、
(28)
(5)├ P→(Q→P)
1 (1) P 仮定
1 (2) P∨~Q 1∨導入
3 (3) P A
3 (4) ~Q∨ P 3∨導入
5 (5) ~Q A
5 (6) ~Q∨ P 5∨導入
1 (7) ~Q∨ P 23456∨除去
8 (8) Q&~P 仮定
9 (9) ~Q A
8 (ア) Q &除去
89 (イ) ~Q& Q 9ア&導入
9 (ウ)~(Q&~P) 8イ背理法
エ (エ) P 仮定
8 (オ) ~P 8&除去
8エ (カ) P&~P エオ&導入
エ (キ)~(Q&~P) 8カ背理法
1 (ク)~(Q&~P) 79ウエキ∨除去
ケ (ケ) Q 仮定
コ(コ) ~P 仮定
ケコ(サ) Q&~P ケコ&導入
1 ケコ(シ)~(Q&~P)&
(Q&~P) クサ&導入
1 ケ (ス) ~~P コシ背理法
1 ケ (セ) P ス二重否定
1 (ソ) Q→P ケセ条件法(仮定の解消)
(タ)P→(Q→P) 1ソ条件法(仮定の解消)
であれば、
1 (2) P∨~Q 1∨導入
3 (4) ~Q∨ P 3∨導入
5 (6) ~Q∨ P 5∨導入
といふ「三つ」が、「∨-導入の規則」に、他ならない。
従って、
(01)(26)(28)により、
(29)
① 今日は水曜である。従って、
② 今日は水曜であるか、明日は雨でない。
といふやうな、「∨-導入の規則」を、認めないのであれば、
(タ)P→(Q→P) 1ソ条件法(仮定の解消)
といふ「結論」、すなはち、
P→(Q→P)(Pならば(QならばP))
といふ「ヒルベルトの公理」を、「自然演繹」では、「証明」出来ない。
といふ、ことになる。
従って、
(27)(28)(29)により、
(30)
「今日は水曜日である。従って、今日は水曜であるか、明日は雨でない。」
といふ「推論」は、「ナンセンス(無意味)」であるやうでゐて、それを認めない限り、
P→(Q→P)(Pならば(QならばP))
といふ「ヒルベルトの公理」を、「自然演繹」では、「証明」出来ない。
※コメント投稿者のブログIDはブログ作成者のみに通知されます