(01)
Most theorems of interest are obtained in fact by application of CP. For example:
興味のある定理の大ていのものは、事実上CPを適用することによって導かれる。たとえば、
38 ├ P→P
1(1)P A
(2)P→P 11CP
39 ├ P→~~P
1(1)P A
1(2)~~P 1DN
(3)P→~~P 12CP
40 ├ ~~P→P
1(1)~~P A
1(2) P 1DN
(3)~~P→P 12CP
41 ├ P&Q→P
1(1)P&Q A
1(2)P 1&E
(3)P&Q→P 12CP
(E.J.レモン著、竹尾治一郎・浅野楢英 訳、1973年、64頁改)
然るに、
(02)
(ⅰ)├ P→(Q→P)
1 (1) P A
1 (2) ~Q∨ P 1∨I
3 (3) Q&~P A
4 (4) ~Q A
3 (5) Q 3&E
34 (6) ~Q& Q 45&I
4 (7)~(Q&~P) 36RAA
8 (8) P A
3 (9) ~P 3&E
3 8 (ア) P&~P 89&I
8 (イ)~(Q&~P) 3アRAA
1 (ウ)~(Q&~P) 2478イ∨E
エ (エ) Q A
オ(オ) ~P A
エオ(カ) Q&~P エオ&I
1 エオ(キ)~(Q&~P)&
(Q&~P) ウカ&I
1 エ (ク) ~~P オキRAA
1 エ (ケ) P クDN
1 (コ) Q→P エケCP
(サ)P→(Q→P) 1コCP
(ⅱ)├ (P→Q)→((P→(Q→R))→(P→R))
1 (1) P→ Q A
2 (2) P→(Q→R) A
3(3) P A
1 3(4) Q 13MPP
23(5) Q→R 23MPP
123(6) R 45MPP
12 (7) P→R 36CP
1 (8) (P→(Q→R))→(P→R) 26CP
(9)(P→Q)→((P→(Q→R))→(P→R)) 18CP
(ⅲ)├ P→(Q→P&Q)
1 (1)P A
2(2)Q A
12(3) P&Q 12&I
1 (4) Q→P&Q 23CP
(5)P→(Q→P&Q) 14CP
(ⅳ)├ P&Q→P
1(1)P&Q A
1(2)P 1&E
(3)P&Q→P 12RAA
(ⅴ)├ P→P∨Q
1(1) P A
1(2) P∨Q 1∨I
(3)P→P∨Q 12CP
(ⅵ)├(P→R)→((Q→R)→(P∨Q→R))
1 (1) P→R A
2 (2) Q→R A
3 (3) P∨Q A
4 (4) P A
1 4 (5) R 14MPP
6(7) Q A
2 6(8) R 27MPP
123 (9) R 34578∨E
12 (ア) P∨Q→R 39CP
1 (イ) (Q→R)→(P∨Q→R) 2アCP
(ウ)(P→R)→((Q→R)→(P∨Q→R)) 1イCP
(ⅶ)├(P→ Q)→((P→~Q)→~P)
1 (1) P→ Q A
2 (2) P→~Q A
3(3) P A
1 3(4) Q 13MPP
23(5) ~Q 23MPP
123(6) Q&~Q 45&I
12 (7) ~P 36RAA
1 (8) (P→~Q)→~P 27CP
(9)(P→ Q)→((P→~Q)→~P) 18CP
(ⅷ)├ ~~P→P
1(1)~~P A
1(2) P 1DN
(3)~~P→P 12CP
従って、
(01)(02)により、
(03)
(ⅰ)├ P→(Q→P)
(ⅱ)├(P→Q)→((P→(Q→R))→(P→R))
(ⅲ)├ P→(Q→P&Q)
(ⅵ)├ P&Q→P
(ⅴ)├ P→P∨Q
(ⅵ)├(P→R)→((Q→R)→(P∨Q→R))
(ⅶ)├(P→Q)→((P→~Q)→~P)
(ⅷ)├ ~~P→P
は全て、「CPを適用することによって導かれる」所の「定理(Theorems)」である。
従って、
(03)により、
(04)
PをAに置き換へ、
QをBに置き換へ、
RをCに置き換へ、
&を∧に置き換へ、
~を¬に置き換へた、
(ⅰ)├ A→(B→A)
(ⅱ)├(A→B)→((A→(B→C))→(A→C))
(ⅲ)├ A→(B→A∧B)
(ⅵ)├ A∧B→A
(ⅴ)├ A→A∨B
(ⅵ)├(A→C)→((B→C)→(A∨B→C))
(ⅶ)├(A→B)→((A→¬B)→¬A)
(ⅷ)├ ¬¬A→A
は、すべて、「定理(Theorems)」である。
cf.
「論理学の記号」は、「数学の記号」とは異なり、統一されてゐない。
然るに、
(05)
公理
(1) A→(B→A)
(2)(A→B)→((A→(B→C))→(A→C))
(3) A→(B→A∧B)
(4) A∧B→A
(5) A→A∨B
(6)(A→C)→((B→C)→(A∨B→C))
(7)(A→B)→((A→¬B)→¬A)
(08) ¬¬A→A
(吉永良正、ゲーデル・不完全定理、1992年、204頁)
― 中略、―
図1-6 推論を行うための論理法則(ヒルベルト=アッカーマンの公理系による)
(吉永良正、ゲーデル・不完全定理、1992年、204頁)
然るに、
(06)
自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系Lは、証明の構文規則に関する次のような「10個の基本的規則(10 Primitive rules)」だけを持つ。
仮定の規則(A)
肯定肯定式(MPP)
否定否定式(MTT)
二重否定(DN)
条件的証明(CP)
&-導入(&I)
&-除去(&E)
∨-導入(∨I)
∨-除去(∨E)
背理法(RAA)
(ウィキペディア改)
従って、
(01)~(06)により、
(07)
「ジョン・レモンが開発した体系L」には、「公理(axioms)」が無くて、その代はりに、「10個の基本的規則(10 Primitive rules)」が有るため、
(1) A→(B→A)
(2)(A→B)→((A→(B→C))→(A→C))
(3) A→(B→A∧B)
(4) A∧B→A
(5) A→A∨B
(6)(A→C)→((B→C)→(A∨B→C))
(7)(A→B)→((A→¬B)→¬A)
(08) ¬¬A→A
といふ「ヒルベルト=アッカーマンの公理(axioms)」は、「ジョン・レモンが開発した体系L」に於ける「定理(theorems)」である。
然るに、
(08)
axiomの意味 - 小学館 プログレッシブ英和中辞典
1自明の理
2(確立している)原理,原則,格言,金言;《論理学・数学》公理,公準
従って、
(08)により、
(09)
「公理(axioms)」には、「自明の理(おのづから明らかな、ことわり)」といふ「意味」が有る。
然るに、
(10)
例へば、
(2)(A→B)→((A→(B→C))→(A→C))≡
(〃)(AならばBである)ならば((Aならば(BならばCである))ならば(AならばCである))。
といふ「言ひ方」は、「自明の理(おのづから明らかな、ことわり)」であるとは、言へないはずである。
然るに、
(11)
その一方で、「ジョン・レモンが開発した体系L」の「10個の基本的規則」は、概ね、
(2)(AならばBである)ならば((Aであるならば(BであるならばCである))ならば(AならばCである))。
よりは「分りやすく」、それ故、「自然な演繹(Natural deduction)」といふ「名前」で、呼ばれてゐる。
然るに、
(12)
いま、「├ A→A」(A→Aは証明可能)」を公理から導いてみましょう(図1-7)
通常の解釈では「A→A」は、要するに「AならばA」のことにほかならないので、「自明の理」のように思われます。
しかし、ここで採用した公理に「A→A」は入っていないので、形式的には証明の可能性は保証されてはいず、ご覧のようにかなり複雑な手順を踏んで証明しなければなりません。
(吉永良正、ゲーデル・不完全定理、1992年、205頁改)
然るに、
(01)(06)により、
(13)
もう一度、確認すると、
38 ├ P→P
1(1)P A(仮定の規則)
(2)P→P 11CP(条件的規則)
従って、
(13)により、
(14)
1(1)A A(仮定の規則)
(2)A→A 11CP(条件的証明)
従って、
(06)(14)により、
(15)
「ジョン・レモンが開発した体系L」であれば、
「A→A(AならばAである。)」は、「10個の基本的規則(10 Primitive rules)」の内の「2つ」によって、「証明される」。
最新の画像[もっと見る]
- (219)「雜説・韓愈」の述語論理(Ⅱ):「返り点」に注意。 6年前
- (148)足りないのは「和文力」。 6年前
- (145)「雑説、韓愈」に於ける「連言の否定」(Ⅴ) 6年前
- (142)「雑説、韓愈」に於ける「連言の否定」(Ⅱ)。 6年前
- (141)「雑説、韓愈」と「連言の否定」。 6年前
- (139)『括弧』と『返り点』。 6年前
- (137)「君子不以其所以養人者害人」等の「不」について。 6年前
- (135)「以十五城(副詞句)」の位置について。 6年前
- (130)「白話文(北京語)」の、有り得ない「返り点」について。 6年前
- (130)「白話文(北京語)」の、有り得ない「返り点」について。 6年前
※コメント投稿者のブログIDはブログ作成者のみに通知されます