Most theorems of interest are obtained in fact by application of CP. For example:
興味のある定理の大ていのものは、事実上ＣＰを適用することによって導かれる。たとえば、
３８ ├ Ｐ→Ｐ
１（１）Ｐ Ａ
（２）Ｐ→Ｐ １１ＣＰ
３９ ├ Ｐ→～～Ｐ
１（１）Ｐ Ａ
１（２）～～Ｐ １ＤＮ
（３）Ｐ→～～Ｐ １２ＣＰ
４０ ├ ～～Ｐ→Ｐ
１（１）～～Ｐ Ａ
１（２） Ｐ １ＤＮ
（３）～～Ｐ→Ｐ １２ＣＰ
４１ ├ Ｐ＆Ｑ→Ｐ
１（１）Ｐ＆Ｑ Ａ
１（２）Ｐ １＆Ｅ
（３）Ｐ＆Ｑ→Ｐ １２ＣＰ
（E.J.レモン著、竹尾治一郎・浅野楢英 訳、1973年、６４頁改）
然るに、
（02）
（ⅰ）├ Ｐ→（Ｑ→Ｐ）
１ （１） Ｐ Ａ
１ （２） ～Ｑ∨ Ｐ １∨Ｉ
３ （３） Ｑ＆～Ｐ Ａ
４ （４） ～Ｑ Ａ
３ （５） Ｑ ３＆Ｅ
３４ （６） ～Ｑ＆ Ｑ ４５＆Ｉ
４ （７）～（Ｑ＆～Ｐ） ３６ＲＡＡ
８ （８） Ｐ Ａ
３ （９） ～Ｐ ３＆Ｅ
３ ８ （ア） Ｐ＆～Ｐ ８９＆Ｉ
８ （イ）～（Ｑ＆～Ｐ） ３アＲＡＡ
１ （ウ）～（Ｑ＆～Ｐ） ２４７８イ∨Ｅ
エ （エ） Ｑ Ａ
オ（オ） ～Ｐ Ａ
エオ（カ） Ｑ＆～Ｐ エオ＆Ｉ
１ エオ（キ）～（Ｑ＆～Ｐ）＆
（Ｑ＆～Ｐ） ウカ＆Ｉ
１ エ （ク） ～～Ｐ オキＲＡＡ
１ エ （ケ） Ｐ クＤＮ
１ （コ） Ｑ→Ｐ エケＣＰ
（サ）Ｐ→（Ｑ→Ｐ） １コＣＰ
（ⅱ）├ （Ｐ→Ｑ）→（（Ｐ→（Ｑ→Ｒ））→（Ｐ→Ｒ））
１ （１） Ｐ→ Ｑ Ａ
２ （２） Ｐ→（Ｑ→Ｒ） Ａ
３（３） Ｐ Ａ
１ ３（４） Ｑ １３ＭＰＰ
２３（５） Ｑ→Ｒ ２３ＭＰＰ
１２３（６） Ｒ ４５ＭＰＰ
１２ （７） Ｐ→Ｒ ３６ＣＰ
１ （８） （Ｐ→（Ｑ→Ｒ））→（Ｐ→Ｒ） ２６ＣＰ
（９）（Ｐ→Ｑ）→（（Ｐ→（Ｑ→Ｒ））→（Ｐ→Ｒ）） １８ＣＰ
（ⅲ）├ Ｐ→（Ｑ→Ｐ＆Ｑ）
１ （１）Ｐ Ａ
２（２）Ｑ Ａ
１２（３） Ｐ＆Ｑ １２＆Ｉ
１ （４） Ｑ→Ｐ＆Ｑ ２３ＣＰ
（５）Ｐ→（Ｑ→Ｐ＆Ｑ） １４ＣＰ
（ⅳ）├ Ｐ＆Ｑ→Ｐ
１（１）Ｐ＆Ｑ Ａ
１（２）Ｐ １＆Ｅ
（３）Ｐ＆Ｑ→Ｐ １２ＲＡＡ
（ⅴ）├ Ｐ→Ｐ∨Ｑ
１（１） Ｐ Ａ
１（２） Ｐ∨Ｑ １∨Ｉ
（３）Ｐ→Ｐ∨Ｑ １２ＣＰ
（ⅵ）├（Ｐ→Ｒ）→（（Ｑ→Ｒ）→（Ｐ∨Ｑ→Ｒ））
１ （１） Ｐ→Ｒ Ａ
２ （２） Ｑ→Ｒ Ａ
３ （３） Ｐ∨Ｑ Ａ
４ （４） Ｐ Ａ
１ ４ （５） Ｒ １４ＭＰＰ
６（７） Ｑ Ａ
２ ６（８） Ｒ ２７ＭＰＰ
１２３ （９） Ｒ ３４５７８∨Ｅ
１２ （ア） Ｐ∨Ｑ→Ｒ ３９ＣＰ
１ （イ） （Ｑ→Ｒ）→（Ｐ∨Ｑ→Ｒ） ２アＣＰ
（ウ）（Ｐ→Ｒ）→（（Ｑ→Ｒ）→（Ｐ∨Ｑ→Ｒ）） １イＣＰ
（ⅶ）├（Ｐ→ Ｑ）→（（Ｐ→～Ｑ）→～Ｐ）
１ （１） Ｐ→ Ｑ Ａ
２ （２） Ｐ→～Ｑ Ａ
３（３） Ｐ Ａ
１ ３（４） Ｑ １３ＭＰＰ
２３（５） ～Ｑ ２３ＭＰＰ
１２３（６） Ｑ＆～Ｑ ４５＆Ｉ
１２ （７） ～Ｐ ３６ＲＡＡ
１ （８） （Ｐ→～Ｑ）→～Ｐ ２７ＣＰ
（９）（Ｐ→ Ｑ）→（（Ｐ→～Ｑ）→～Ｐ） １８ＣＰ
（ⅷ）├ ～～Ｐ→Ｐ
１（１）～～Ｐ Ａ
１（２） Ｐ １ＤＮ
（３）～～Ｐ→Ｐ １２ＣＰ
従って、
（01）（02）により、
（03）
（ⅰ）├ Ｐ→（Ｑ→Ｐ）
（ⅱ）├（Ｐ→Ｑ）→（（Ｐ→（Ｑ→Ｒ））→（Ｐ→Ｒ））
（ⅲ）├ Ｐ→（Ｑ→Ｐ＆Ｑ）
（ⅵ）├ Ｐ＆Ｑ→Ｐ
（ⅴ）├ Ｐ→Ｐ∨Ｑ
（ⅵ）├（Ｐ→Ｒ）→（（Ｑ→Ｒ）→（Ｐ∨Ｑ→Ｒ））
（ⅶ）├（Ｐ→Ｑ）→（（Ｐ→～Ｑ）→～Ｐ）
（ⅷ）├ ～～Ｐ→Ｐ
は全て、「ＣＰを適用することによって導かれる」所の「定理（Theorems）」である。
従って、
（03）により、
（04）
ＰをＡに置き換へ、
ＱをＢに置き換へ、
ＲをＣに置き換へ、
＆を∧に置き換へ、
～を￢に置き換へた、
（ⅰ）├ Ａ→（Ｂ→Ａ）
（ⅱ）├（Ａ→Ｂ）→（（Ａ→（Ｂ→Ｃ））→（Ａ→Ｃ））
（ⅲ）├ Ａ→（Ｂ→Ａ∧Ｂ）
（ⅵ）├ Ａ∧Ｂ→Ａ
（ⅴ）├ Ａ→Ａ∨Ｂ
（ⅵ）├（Ａ→Ｃ）→（（Ｂ→Ｃ）→（Ａ∨Ｂ→Ｃ））
（ⅶ）├（Ａ→Ｂ）→（（Ａ→￢Ｂ）→￢Ａ）
（ⅷ）├ ￢￢Ａ→Ａ
は、すべて、「定理（Theorems）」である。
ｃｆ.
「論理学の記号」は、「数学の記号」とは異なり、統一されてゐない。
然るに、
（05）
公理
（１） Ａ→（Ｂ→Ａ）
（２）（Ａ→Ｂ）→（（Ａ→（Ｂ→Ｃ））→（Ａ→Ｃ））
（３） Ａ→（Ｂ→Ａ∧Ｂ）
（４） Ａ∧Ｂ→Ａ
（５） Ａ→Ａ∨Ｂ
（６）（Ａ→Ｃ）→（（Ｂ→Ｃ）→（Ａ∨Ｂ→Ｃ））
（７）（Ａ→Ｂ）→（（Ａ→￢Ｂ）→￢Ａ）
（08） ￢￢Ａ→Ａ
（吉永良正、ゲーデル・不完全定理、1992年、２０４頁）
― 中略、―
図１－６ 推論を行うための論理法則（ヒルベルト=アッカーマンの公理系による）
（吉永良正、ゲーデル・不完全定理、1992年、２０４頁）
然るに、
（06）
自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系Ｌは、証明の構文規則に関する次のような「１０個の基本的規則（10 Primitive rules）」だけを持つ。
仮定の規則（Ａ）
肯定肯定式（ＭＰＰ）
否定否定式（ＭＴＴ）
二重否定（ＤＮ）
条件的証明（ＣＰ）
＆－導入（＆Ｉ）
＆－除去（＆Ｅ）
∨－導入（∨Ｉ）
∨－除去（∨Ｅ）
背理法（ＲＡＡ）
（ウィキペディア改）
従って、
（01）～（06）により、
（07）
「ジョン・レモンが開発した体系Ｌ」には、「公理（axioms）」が無くて、その代はりに、「１０個の基本的規則（10 Primitive rules）」が有るため、
（１） Ａ→（Ｂ→Ａ）
（２）（Ａ→Ｂ）→（（Ａ→（Ｂ→Ｃ））→（Ａ→Ｃ））
（３） Ａ→（Ｂ→Ａ∧Ｂ）
（４） Ａ∧Ｂ→Ａ
（５） Ａ→Ａ∨Ｂ
（６）（Ａ→Ｃ）→（（Ｂ→Ｃ）→（Ａ∨Ｂ→Ｃ））
（７）（Ａ→Ｂ）→（（Ａ→￢Ｂ）→￢Ａ）
（08） ￢￢Ａ→Ａ
といふ「ヒルベルト=アッカーマンの公理（axioms）」は、「ジョン・レモンが開発した体系Ｌ」に於ける「定理（theorems）」である。
然るに、
（08）
axiomの意味 - 小学館 プログレッシブ英和中辞典
1自明の理
2（確立している）原理，原則，格言，金言；《論理学・数学》公理，公準
従って、
（08）により、
（09）
「公理（axioms）」には、「自明の理（おのづから明らかな、ことわり）」といふ「意味」が有る。
然るに、
（10）
例へば、
（２）（Ａ→Ｂ）→（（Ａ→（Ｂ→Ｃ））→（Ａ→Ｃ））≡
（〃）（ＡならばＢである）ならば（（Ａならば（ＢならばＣである））ならば（ＡならばＣである））。
といふ「言ひ方」は、「自明の理（おのづから明らかな、ことわり）」であるとは、言へないはずである。
然るに、
（11）
その一方で、「ジョン・レモンが開発した体系Ｌ」の「１０個の基本的規則」は、概ね、
（２）（ＡならばＢである）ならば（（Ａであるならば（ＢであるならばＣである））ならば（ＡならばＣである））。
よりは「分りやすく」、それ故、「自然な演繹（Natural deduction）」といふ「名前」で、呼ばれてゐる。
然るに、
（12）
いま、「├ Ａ→Ａ」（Ａ→Ａは証明可能）」を公理から導いてみましょう（図１－７）
通常の解釈では「Ａ→Ａ」は、要するに「ＡならばＡ」のことにほかならないので、「自明の理」のように思われます。
しかし、ここで採用した公理に「Ａ→Ａ」は入っていないので、形式的には証明の可能性は保証されてはいず、
（吉永良正、ゲーデル・不完全定理、1992年、２０５頁改）
然るに、
（01）（06）により、
（13）
もう一度、確認すると、
３８ ├ Ｐ→Ｐ
１（１）Ｐ Ａ（仮定の規則）
（２）Ｐ→Ｐ １１ＣＰ（条件的規則）
従って、
（13）により、
（14）
１（１）Ａ Ａ（仮定の規則）
（２）Ａ→Ａ １１ＣＰ（条件的証明）
従って、
（06）（14）により、
（15）
「ジョン・レモンが開発した体系Ｌ」であれば、
「Ａ→Ａ（ＡならばＡである。）」は、「１０個の基本的規則（10 Primitive rules）」の内の「２つ」によって、「証明される」。
令和元年１１月０７日、毛利太。
0 件のコメント:
コメントを投稿