(01)
困難さの第二の理由には、自然演繹には「仮定の解消」(最初に仮定しておいて、あとでなかったことにする)という手続きがあり、それがなかなか理解しづらいことです。自然演繹は、「仮定の解消」のおかげで公理なしに演繹システムになり得ており、その意味で「仮定の解消」は自然演繹の本質だと言っても過言ではありません(小島寛之、証明と論理に強くなる、2017年、144頁)。
従って、
(01)により、
(02)
自然演繹は、その「本質(仮定の解消)」が分かりにくい(?)。
然るに、
(03)
(ⅰ)
① 1 (1) P→Q 仮定(A)
② 2(2) P 仮定(A)
③ 12(3) Q 12前件肯定(MPP)
④ 1 (4) P→Q 23仮定の解消(CP)
⑤ (5)(P→Q)→(P→Q) 14仮定の解消(CP)
然るに、
(04)
① 1 (1)に於ける、
① 1 といふのは、具体的には、(P→Q) といふ「仮定」であって、
② 2(2)に於ける、
② 2 といふのは、具体的には、(P) といふ「仮定」であって、
③ 12(3)に於ける、
③ 12 といふのは、具体的には、(P→Q,P)といふ「仮定」である。
④ 1 (4)に於ける、
④ 1 といふのは、具体的には、(P→Q) といふ「仮定」である。
従って、
(03)(04)により、
(05)
(ⅰ)
① 1 (1) P→Q 仮定(A)
② 2(2) P 仮定(A)
③ 12(3) Q 12前件肯定(MPP)
④ 1 (4) P→Q 23仮定の解消(CP)
⑤ (5)(P→Q)→(P→Q) 14仮定の解消(CP)
といふ「計算」は、
① P→Q (1) P→Q 仮定(A)
② P (2) P 仮定(A)
③ P→Q,P(3) Q 12前件肯定(MPP)
④ P→Q (4) P→Q 23仮定の解消(CP)
⑤ (5)(P→Q)→(P→Q) 14仮定の解消(CP)
といふ「計算」に、「等しい」。
然るに、
(06)
① P→Q (1) P→Q 仮定(A)
② P (2) P 仮定(A)
③ P→Q,P(3) Q 12前件肯定(MPP)
④ P→Q (4) P→Q 23仮定の解消(CP)
⑤ (5)(P→Q)→(P→Q) 14仮定の解消(CP)
といふ「計算」の「各行」を、「連式(Sequents)」で表すと、
① P→Q ├ P→Q
② P ├ P
③ P→Q,P├ Q
④ P→Q ├ P→Q
⑤ ├ (P→Q)→(P→Q)
といふ「式」になる。
然るに、
(07)
「・・・・・という仮定が与えられるならば、・・・・・と正しく結論することができる」という煩雑な表現の略記法があれば好都合であろう。このためわたしは、論理学の文献のなかでしばしば、しかし誤解を招きやすい仕方で、断定記号(assertion-sign)、
├
を導入する。これは「故に」(therefore)と読むのが便利であろう。
(E.J.レモン、竹尾治一郎・浅野楢英 訳、論理学入門、16頁)
従って、
(06)(07)により、
(08)
① P→Q ├ P→Q
② P ├ P
③ P→Q,P├ Q
④ P→Q ├ P→Q
⑤ ├ (P→Q)→(P→Q)
といふ「連式」は、「日本語」で言ふと、
① PであるならばQである。 ので、PであるならばQである。
② Pである。 ので、Pである。
③ PであるならばQであって、Pである。ので、 Qである。
④ PであるならばQである。 ので、PであるならばQである。
⑤ ので、PであるならばQである。ならば、PであるならばQである。
といふ「意味」になる。
従って、
(05)(08)により、
(09)
(ⅰ)
① 1 (1)P→Q 仮定(A)
② 2(2)P 仮定(A)
③ 12(3) Q 12前件肯定(MPP)
④ 1 (4)P→Q 23仮定の解消(CP)
に於ける、
④ 1 (4)P→Q 23仮定の解消(CP)
といふ「行」を、仮に、
④ 12(4)P→Q 23仮定の解消(CP)
といふ風に、書くならば、
④ PであるならばQである。 ので、PであるならばQである。
といふ「意味」ではなく、
④ PであるならばQであって、Pである。ので、PであるならばQである。
といふ「意味」になる。
然るに、
(10)
④ PであるならばQであって、Pである。ので、・・・・。
といふのであれば、
③ PであるならばQであって、Pである。ので、Qである。
といふ、ことになる。
然るに、
(08)(09)(10)により、
(11)
③ PであるならばQであって、Pである。ので、 Qである。
④ PであるならばQである。 ので、PであるならばQである。
といふ「日本語の意味」を、「区別」した上で、「連式」で表すとしたら、
③ P→Q,P├ Q
④ P→Q,P├ P→Q
ではなく、
③ P→Q,P├ Q
④ P→Q ├ P→Q
といふ風に、書かざるを得ない。
然るに、
(03)(04)により、
(12)
もう一度、確認すると、
③ 12(3) Q 12前件肯定(MPP)
④ 1 (4)P→Q 23仮定の解消(CP)
に於いて、
③ 12(3)に於ける、
③ 12 といふのは、具体的には、(P→Q,P)といふ「仮定」である。
④ 1 (4)に於ける、
④ 1 といふのは、具体的には、(P→Q) といふ「仮定」である。
従って、
(06)(11)(12)により、
(13)
その「連式」が、
③ P→Q,P├ Q
④ P→Q ├ P→Q
である以上、その「計算」は、
③ 12(3) Q 12前件肯定(MPP)
④ 1 (4)P→Q 23仮定の解消(CP)
といふ風に、書かざるを得ない。
然るに、
(01)(12)(13)により、
(14)
③ 12(3) Q 12前件肯定(MPP)
④ 1 (4)P→Q 23仮定の解消(CP)
に於いて、
③ 12(3) から、
④ 1 (4) に変はる。
といふことは、
③ 12(3)には有った、
③ 2 といふ「仮定」が除かれて、
④ 1 (4)に変はった。
といふことに、他ならず、このことを称して、小島寛之先生は、
自然演繹には「仮定の解消」(最初に仮定しておいて、あとでなかったことにする)という手続きがあり、それがなかなか理解しづらいことです。
といふ風に、述べてゐる。
然るに、
(15)
④「風邪を引いた」ので、「会社を休む」。
と言へるのであれば、
⑤「風邪を引いた」ならば「会社を休む」。
といふことが、言へなければならない。
従って、
(15)により、
(16)
④「Pである」ので、「Qである」。
と言へるのであれば、
⑤「Pである」ならば「Qである」。
といふことが、言へなければならない。
従って、
(16)により、
(17)
④「PであるならばQである。」ので、「PであるならばQである。」
と言へるのであれば、
⑤「PであるならばQである。」ならば「PであるならばQである。」
といふことが、言へなければならない。
従って、
(17)により、
(18)
④「PであるならばQである。」ので、「PであるならばQである。」
⑤「PであるならばQである。」ならば「PであるならばQである。」
に於いて、
④ から、
⑤ を「演繹」することは、「妥当」である。
従って、
(05)(08)(18)により、
(19)
④ 1(4) P→Q 23仮定の解消(CP)
⑤ (5) (P→Q)→(P→Q) 14仮定の解消(CP)
④ P→Q├ P→Q
⑤ ├ (P→Q)→(P→Q)
④「PであるならばQである。」ので、「PであるならばQである。」
⑤「PであるならばQである。」ならば「PであるならばQである。」
に於いて、
④ から、
⑤ を「演繹」することは、「妥当」である。
然るに、
(20)
⑤(5)(P→Q)→(P→Q) 14仮定の解消(CP)
⑤ ├ (P→Q)→(P→Q)
⑤「PであるならばQである。」ならば「PであるならばQである。」
に於いて、
(P→Q)=P
といふ「代入(Substitutuion)」を行ふと、
⑤(5)P→P 14仮定の解消(CP)
⑤ ├ P→P
⑤「Pである。」ならば「Pである。」
となって、この「命題」は「同一律(tautology、同義語反復)」である。
従って、
(20)により、
(21)
⑤(5)(P→Q)→(P→Q) 14仮定の解消(CP)
⑤ ├ (P→Q)→(P→Q)
⑤「PであるならばQである。」ならば「PであるならばQである。」
といふ「式」は、
⑤(5)P→P 14仮定の解消(CP)
⑤ ├ P→P
⑤「Pである。」ならば「Pである。」
とふ「同一律」に対する、「代入例(Substitution instance)」である。
然るに、
(22)
⑤「同一律(PならばPである)」は、「恒に、真」である。
然るに、
(23)
⑤「恒に真(tautology)」であるといふことは、「特定の仮定」に「依存」することなく、「恒に真(本当)である」。
といふことである。
従って、
(22)(23)により、
(24)
⑤「同一律(PならばPである)」は、「特定の仮定」に「依存」することなく、「恒に真(本当)である」。
従って、
(21)(24)により、
(25)
⑤(5)P→P 14仮定の解消(CP)
⑤ ├ P→P
⑤「Pである。」ならば「Pである。」
とふ「同一律」に対する、「代入例(Substitution instance)」である、
⑤(5)(P→Q)→(P→Q) 14仮定の解消(CP)
⑤ ├ (P→Q)→(P→Q)
⑤「PであるならばQである。」ならば「PであるならばQである。」
といふ「式」は、「特定の仮定」に「依存」することなく、「恒に真(本当)である」。
然るに、
(26)
①「風邪を引いた」ので、「会社を休む」。
⑤「風邪を引いた」ならば「会社を休む」。
に於いて、
① であれば、「已に、風邪を、引いてゐる (已然形)」。
⑤ であれば、「未だ、風邪は、引いてゐない(未然形)」。
従って、
(26)により、
(27)
①「風邪を引いた」ので、「会社を休む」。
⑤「風邪を引いた」ならば「会社を休む」。
に於いて、
①=⑤ ではない。
従って、
(27)により、
(28)
① 1(1) P→Q 仮定(A)
① P→Q├ P→Q
①「PであるならばQである。」ので、「PであるならばQである。」
⑤ (5) (P→Q)→(P→Q) 14仮定の解消(CP)
⑤ ├ (P→Q)→(P→Q)
⑤「PであるならばQである。」ならば「PであるならばQである。」
に於いても、
①=⑤ ではない。
従って、
(19)(25)(28)により、
(29)
① 1(1) P→Q 仮定(A)
① P→Q├ P→Q
①「PであるならばQである。」ので、「PであるならばQである。」
⑤ (5) (P→Q)→(P→Q) 14仮定の解消(CP)
⑤ ├ (P→Q)→(P→Q)
⑤「PであるならばQである。」ならば「PであるならばQである。」
に於いて、
⑤は① から、「演繹」出来、
①=⑤ では、決してなく、尚且つ、
⑤ は、「特定の仮定」に「依存」することなく、「恒に真(本当)である」。
従って、
(03)(04)(29)により、
(30)
(ⅰ)
① 1 (1) P→Q 仮定(A)
② 2(2) P 仮定(A)
③ 12(3) Q 12前件肯定(MPP)
④ 1 (4) P→Q 23仮定の解消(CP)
⑤ (5)(P→Q)→(P→Q) 14仮定の解消(CP)
といふ「計算」の「最後の行(同一律)」である、
⑤ (5)(P→Q)→(P→Q) 14仮定の解消(CP)
に於いて、
⑤ と、(5)の間に、「仮定」があってはならない。
従って、
(30)により、
(31)
④ 1 (4) P→Q 23仮定の解消(CP)
⑤ (5)(P→Q)→(P→Q) 14仮定の解消(CP)
に於いて、
④ 1 (4)に有った、
④ 1 といふ「仮定」が除かれて、
⑤ (5)に変はることなる。
然るに、
(32)
② P&Q≡Pであって、Qである。
から、
② P ≡Pである。
② Q≡Qである。
を「演繹」することは、「妥当」である。
然るに、
(33)
② P&Q→P≡PであってQである。ならば、Pである。
② P&Q→Q≡PであってQである。ならば、Qである。
は、「特定の仮定」に「依存」することなく、「恒に真(本当)である」。
然るに、
(34)
(ⅱ)
1(1)P&Q 仮定
1(2)P 1連言除去
(3)P&Q→P 12仮定の解消(CP)
(ⅱ)
1(1)P&Q 仮定
1(2)P 1連言除去
(3)P&Q→Q 12仮定の解消(CP)
従って、
(33)(34)により、
(35)
② P&Q→P≡PであってQである。ならば、Pである。
② P&Q→Q≡PであってQである。ならば、Qである。
といふ「恒真式(トートロジー)」は、
② 仮定の解消(CP)
② 仮定の解消(CP)
によって、「証明」されて、その結果として、「仮定」の数が「0個」である。
然るに、
(36)
(ⅱ)
1(1)P&Q 仮定
1(2)P 1連言除去
(3)P&Q→P 12仮定の解消(CP)
といふ「計算」は、
(1)で、「P&Q」 を「仮定」したら、
(2)で、「P 」 が得られたので、「仮定(1)」を解消してを、
(3)で、「P&Q→P」を得た。
といふ、「意味」である。
然るに、
(37)
興味のある定理の大ていのものは、事実上CPを適用することによって導かれる。たとえば、
Most theorems of intrest are obtained in fact by application of CP. For example:
38 ├ P→P(連式29を参照)
1(1)P A
(2)P→P 1,1 CP
(E.J.レモン、竹尾治一郎・浅野楢英 訳、論理学入門、64頁と、原文)
29 P├ P
1(1)P A
これ以上短い連式は証明できないし、またその証明は可能な最も短い証明である。
No shorter sequent than this can be proved, and its proof is the shortest possible proof.
(E.J.レモン、竹尾治一郎・浅野楢英 訳、論理学入門、44頁と、原文)
従って、
(36)(37)により、
(38)
1(1)P A
(2)P→P 1,1 CP
といふ「計算」は、
(1)で、「P」 を「仮定」したら、
(1)で、「P」 が得られたので、「仮定(1)」を解消して、
(2)で、「P→P」を得た。
といふ、「意味」である。
cf.
従って、
(39)
自然演繹では、「P→P(PならばPなり)」といふ「同一律(law of identity)」を、「仮定の解消(CP)」といふ「規則」を用ひて、「証明」出来る。
従って、
(39)により、
(40)
普通に考えると、素朴な恒真式(トートロジー)である、
P→P(PならばP)
とか、
あるいは、
P∨~P
などいつでも使える出発点(公理)として準備したほうがいいのではないか、と思うでしょう。しかし、そんな必要はないのです。なぜなら、どちらの恒真式も自然演繹で演繹できてしまうのです(小島寛之、証明と論理に強くなる、2017年、141頁)。といふ、ことになる。
cf.
―「排中律」の証明 ―
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∨~P 5∨I
1 (7) ~(P∨~P)&
(P∨~P) 16&I
1 (8)~~(P∨~P) 17RAA
(9) P∨~P 8DN
然るに、
(41)
パースの法則(パースのほうそく)は哲学者であり論理学者であるチャールズ・サンダース・パースにちなむ論理学における法則である。彼の最初の命題論理の公理化において、この法則を公理に採用した。この公理は、含意と呼ばれるただひとつの結合子を持つ体系における排中律であると考えることもできる。
命題計算では、パースの法則は((P→Q)→P)→P のことを言う(ウィキペディア)。
然るに、
(42)
1 (1) P A
(2) P→P 11CP(同一律)
(3) ~P∨P 2含意の定義(であって、排中律)
4 (4) ~P A
4 (5) ~P∨Q 4∨I
4 (6) P→Q 4含意の定義
4 (7) (P→Q)&~P 46&I
4 (8)~(~(P→Q)∨ P) 7ド・モルガンの法則
9 (9) (P→Q)→ P A
9 (ア) ~(P→Q)∨ P 9含意の定義
49 (イ)~(~(P→Q)∨ P)&
(~(P→Q)∨ P) 8ア&I
4 (ウ) ~((P→Q)→ P) 9イRAA
4 (エ) ~((P→Q)→ P)∨P ウ∨I
オ(オ) P A
オ(カ) ~((P→Q)→ P)∨P オ∨I
(キ) ~((P→Q)→ P)∨P 34エオカ∨E
(ク) ((P→Q)→ P)→P キ含意の定義
(〃) ((PならばQ)ならばPならば)Pである。
然るに、
(43)
(ⅰ)P→Q├ ~P∨Q
1 (1) P→Q A
2 (2) ~(~P∨Q) A
3(3) ~P A
3(4) ~P∨Q 3∨I
23(5) ~(~P∨Q)&
(~P∨Q) 24&I
2 (6) ~~P 35RAA
2 (7) P 6DN
12 (8) Q 17MPP
12 (9) ~P∨Q 8∨I
12 (ア) ~(~P∨Q)&
(~P∨Q) 29&I
1 (イ)~~(~P∨Q) 2アRAA
1 (ウ) ~P∨Q イDN
(ⅱ)~P∨Q├ P→Q
1 (1) ~P∨ Q A
2 (2) P&~Q A
3 (3) ~P A
2 (4) P 2&E
23 (5) ~P& P 34&I
3 (6)~(P&~Q) 25RAA
7 (7) Q A
2 (8) ~Q A
2 7 (9) Q&~Q 78&I
7 (ア)~(P&~Q) 29RAA
1 (イ)~(P&~Q) 1367ア∨E
ウ (ウ) P A
エ(エ) ~Q A
ウエ(オ) P&~Q エオ&I
1 ウエ(カ)~(P&~Q)&
(P&~Q) イオ&I
1 ウ (キ) ~~Q 7カRAA
1 ウ (ク) Q キDN
1 (ケ) P→ Q ウクCP
(ⅲ)P&~Q├ ~(~P∨Q)
1 (1) P&~Q A
2 (2) ~P∨ Q A
1 (3) P 1&E
4 (4) ~P A
1 4 (5) P&~P 34&I
4 (6) ~(P&~Q) 15RAA
1 (7) ~Q 1&E
8(8) Q A
1 8(9) ~Q&Q 78&I
8(ア) ~(P&~Q) 19RAA
2 (イ) ~(P&~Q) 2468ア∨I
12 (ウ) (P&~Q)&
~(P&~Q) 1イ&I
1 (エ)~(~P∨ Q) 2ウRAA
(ⅳ)~(~P∨Q)├ P&~Q
1 (1)~(~P∨Q) A
2 (2) ~P A
2 (3) ~P∨Q 2∨I
12 (4)~(~P∨Q)&
(~P∨Q) 13&I
1 (5) ~~P 24RAA
1 (6) P 5DN
7(7) Q A
7(8) ~P∨Q 7∨I
1 7(9)~(~P∨Q)&
(~P∨Q) 13&I
1 (ア) ~Q 79RAA
1 (イ) P&~Q 6ア&I
従って、
(43)により、
(44)
(ⅰ)P→ Q ┤├ ~P∨ Q
(ⅲ)P&~Q ┤├ ~(~P∨Q)
すなはち、「含意の定義」と「ド・モルガンの法則」は、「導出可能(deriable)」である。
然るに、
(45)
連式に対して10個の原始的規則のみを用いて証明が見出されるならば、その連式を、簡単な言いかたをとって、導出可能(deriable)であるとよぶことにしよう。―中略、―
メタ定理1:すべての導出可能な連式は、トートロジーである。
(E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳、1973年、97頁)
従って、
(41)(42)(45)により、
(46)
((P→Q)→P)→P≡((PならばQ)ならばP)ならばP。
といふ「公理(パースの法則)」は、「自然演繹によって、導出可能(deriable)」である。
従って、
(40)(46)により、
(47)
「自然演繹」は、
P→ P(同一律)
P∨~P(排中律)
((P→Q)→P)→P(パースの法則)
等を、「公理(Axioms)」とする「必要」が、無い。
(48)
(a)「E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳」では、「仮定の解消」ではなく、「条件的証明(CP)」を適用する際の、「取り除かれた仮定(discharged assumption)」といる「言ひ方」がされてゐる。
(b)今書いた、「取り除かれた仮定」に関する「説明」は、私はさう考へるといふことであって、E.J.レモン先生が、そのやうに述べてゐる、といふわけではない。
(c)「最初に仮定しておいて、あとでなかったことにする。」といふ点では、「背理法(RAA)」、並びに、「選言除去(∨E)」もさうである。
(d)私自身が考へる、「自然演繹」に於ける、「最も重要な規則」は、「選言導入(∨I)」である。