「パースの法則」と「演繹定理」。

―「昨日（令和０３年０４月０９日）の記事」を補足します。―
（01）
命題計算では、パースの法則は （（Ｐ→Ｑ）→Ｐ）→Ｐ のことを言う。この意味するところを書き出すと、命題Ｐについて、命題Ｑが存在して、「ＰならばＱ」からＰが真であることが従うときには、Ｐは真でなければならないとなる。とりわけ、Ｑとして偽を選んだ場合には、Ｐから偽が従うときは常にＰが真であるならば、Ｐは真であるとなる。
パースの法則は直観論理や中間命題論理では成立せず、演繹定理だけからでは導くことができない（ウィキペディア）。
然るに、
（02）
１　　　（１）　　（Ｐ→Ｑ）→Ｐ　　　Ａ
　２　　（２）　　～Ｐ∨Ｑ　　　　　　Ａ
　２　　（３）　　　Ｐ→Ｑ　　　　　　２含意の定義
１２　　（４）　　　　　　　　Ｐ　　　１３ＭＰＰ
１　　　（５）　（～Ｐ∨Ｑ）→Ｐ　　　２４ＣＰ（演繹定理）
１　　　（６）～（～Ｐ∨Ｑ）∨Ｐ　　　２含意の定義
　　７　（７）～（～Ｐ∨Ｑ）　　　　　Ａ
　　７　（８）　　Ｐ＆～Ｑ　　　　　　７ド・モルガンの法則
　　７　（９）　　Ｐ　　　　　　　　　８＆Ｅ
　　　ア（ア）　　　　　　　　Ｐ　　　Ａ
１　　　（イ）　　Ｐ　　　　　　　　　６７９アア∨Ｅ
　　　　（ウ）（（Ｐ→Ｑ）→Ｐ）→Ｐ　１イＣＰ（演繹定理）
従って、
（02）により、
（03）
Γ├（（Ｐ→Ｑ）→Ｐ）→Ｐ
といふ「連式（Sequent）」に於ける、
Γ は、空 である。
然るに、
（04）
演繹定理（Deduction theorem）は次のように表現される。
　Γ，Ａ├ Ｂ
ならば、
　Γ├ Ａ→Ｂ
であるが、
　Γ が空のときは当然、
　　├ Ａ→Ｂ
である。
（長尾真・淵一博、論理と意味、1983年、３９・４０頁改）
然るに、
従って、
（02）（03）（04）により、
（05）
「証明（02）」は、紛れもなく、
（Γ，Ａ├ Ｂ）⇔（Γ├ Ａ→Ｂ）
である所の、「演繹定理」による「証明」である。
然るに、
（06）
「証明（02）」の際に、
「定理（含意の定義・ド・モルガンの法則）」を用ひない場合は、
「やむを得ず、その分、長くなる」のであって、「次の証明」がそれである。
１　　　　　　　　　　　　　（１）　　　　（Ｐ→Ｑ）→　Ｐ　　　Ａ
　２　　　　　　　　　　　　（２）　　　　～Ｐ∨Ｑ　　　　　　　Ａ
　　３　　　　　　　　　　　（３）　　　　Ｐ＆～Ｑ　　　　　　　Ａ
　　　４　　　　　　　　　　（４）　　　　～Ｐ　　　　　　　　　Ａ
　　３　　　　　　　　　　　（５）　　　　Ｐ　　　　　　　　　　３＆Ｅ
　　３４　　　　　　　　　　（６）　　　　Ｐ＆～Ｐ　　　　　　　４５＆Ｉ
　　　４　　　　　　　　　　（７）　　～（Ｐ＆～Ｑ）　　　　　　３６ＲＡＡ
　　　　８　　　　　　　　　（８）　　　　　　　Ｑ　　　　　　　Ａ
　　３　　　　　　　　　　　（９）　　　　　　～Ｑ　　　　　　　３＆Ｅ
　　３　８　　　　　　　　　（ア）　　　　Ｑ＆～Ｑ　　　　　　　８９＆Ｉ
　　　　８　　　　　　　　　（イ）　　～（Ｐ＆～Ｑ）　　　　　　３アＲＡＡ
　２　　　　　　　　　　　　（ウ）　　～（Ｐ＆～Ｑ）　　　　　　２４７８イ∨Ｅ
　　　　　エ　　　　　　　　（エ）　　　　Ｐ　　　　　　　　　　Ａ
　　　　　　オ　　　　　　　（オ）　　　　　　～Ｑ　　　　　　　Ａ
　　　　　エオ　　　　　　　（カ）　　　　Ｐ＆～Ｑ　　　　　　　エオ＆Ｉ
　２　　　エオ　　　　　　　（キ）　　～（Ｐ＆～Ｑ）＆
　　　　　　　　　　　　　　　　　　　　（Ｐ＆～Ｑ）　　　　　　ウカ＆Ｉ
　２　　　エ　　　　　　　　（ク）　　　　　～～Ｑ　　　　　　　オキＲＡＡ
　２　　　エ　　　　　　　　（ケ）　　　　　　　Ｑ　　　　　　　クＤＮ
　２　　　　　　　　　　　　（コ）　　　　　Ｐ→Ｑ　　　　　　　エケＣＰ（演繹定理）
１２　　　　　　　　　　　　（サ）　　　　　　　　　　　Ｐ　　　１コＭＰＰ
１　　　　　　　　　　　　　（シ）　　　（～Ｐ∨Ｑ）→　Ｐ　　　２サＣＰ（演繹定理）
　　　　　　　ス　　　　　　（ス）　　　（～Ｐ∨Ｑ）＆～Ｐ　　　Ａ
　　　　　　　ス　　　　　　（セ）　　　（～Ｐ∨Ｑ）　　　　　　ス＆Ｅ
１　　　　　　ス　　　　　　（ソ）　　　　　　　　　　　Ｐ　　　シセＭＰＰ
　　　　　　　ス　　　　　　（タ）　　　　　　　　　　～Ｐ　　　ス＆Ｅ
１　　　　　　ス　　　　　　（チ）　　　　　　　　Ｐ＆～Ｐ　　　ソタ＆Ｉ
１　　　　　　　　　　　　　（ツ）　～｛（～Ｐ∨Ｑ）＆～Ｐ｝　　スチＲＡＡ
　　　　　　　　テ　　　　　（テ）～｛～（～Ｐ∨Ｑ）∨　Ｐ｝　　Ａ
　　　　　　　　　ト　　　　（ト）　　～（～Ｐ∨Ｑ）　　　　　　Ａ
　　　　　　　　　ト　　　　（ナ）　　～（～Ｐ∨Ｑ）∨　Ｐ　　　ト∨Ｉ
　　　　　　　　テト　　　　（ニ）～｛～（～Ｐ∨Ｑ）∨　Ｐ｝＆
　　　　　　　　　　　　　　　　　　｛～（～Ｐ∨Ｑ）∨　Ｐ｝　　テナ＆Ｉ
　　　　　　　　テ　　　　　（ヌ）　～～（～Ｐ∨Ｑ）　　　　　　トニＲＡＡ
　　　　　　　　テ　　　　　（ネ）　　　（～Ｐ∨Ｑ）　　　　　　ヌＤＮ
　　　　　　　　　　ノ　　　（ノ）　　　　　　　　　　　Ｐ　　　Ａ
　　　　　　　　　　ノ　　　（ハ）　　～（～Ｐ∨Ｑ）∨　Ｐ　　　ノ∨Ｉ
　　　　　　　　テ　ノ　　　（ヒ）～｛～（～Ｐ∨Ｑ）∨　Ｐ｝＆
　　　　　　　　　　　　　　　　　　｛～（～Ｐ∨Ｑ）∨　Ｐ｝　　テハ＆Ｉ
　　　　　　　　テ　　　　　（フ）　　　　　　　　　　～Ｐ　　　ノヒＲＡＡ
　　　　　　　　テ　　　　　（ヘ）　　　（～Ｐ∨Ｑ）＆～Ｐ　　　ネフ＆Ｉ
１　　　　　　　テ　　　　　（ホ）　～｛（～Ｐ∨Ｑ）＆～Ｐ｝＆
　　　　　　　　　　　　　　　　　　　｛（～Ｐ∨Ｑ）＆～Ｐ｝　　ツヘ＆Ｉ
１　　　　　　　　　　　　　（マ）～～｛～（～Ｐ∨Ｑ）∨Ｐ｝　　テホＲＡＡ
１　　　　　　　　　　　　　（ミ）　　　～（～Ｐ∨Ｑ）∨Ｐ　　　マＤＮ
　　　　　　　　　　　ム　　（ム）　　　～（～Ｐ∨Ｑ）　　　　　Ａ
　　　　　　　　　　　　メ　（メ）　　　　　～Ｐ　　　　　　　　Ａ
　　　　　　　　　　　　メ　（モ）　　　　　～Ｐ∨Ｑ　　　　　　メ∨Ｉ
　　　　　　　　　　　ムメ　（ヤ）　　　～（～Ｐ∨Ｑ）＆
　　　　　　　　　　　　　　　　　　　　　（～Ｐ∨Ｑ）　　　　　ムモ＆Ｉ
　　　　　　　　　　　ム　　（ユ）　　　　～～Ｐ　　　　　　　　メヤＲＡＡ
　　　　　　　　　　　ム　　（ヨ）　　　　　　Ｐ　　　　　　　　ユＤＮ
　　　　　　　　　　　　　ラ（ラ）　　　　　　　　　　　Ｐ　　　Ａ
１　　　　　　　　　　　　　（リ）　　　　　　Ｐ　　　　　　　　ミムヨララ∨Ｅ
　　　　　　　　　　　　　　（ル）　（（Ｐ→Ｑ）→Ｐ）→Ｐ　　　１リＣＰ（演繹定理）
従って、
（02）（06）により、
（07）
（（Ｐ→Ｑ）→Ｐ）→Ｐ である所の、「パースの法則」は、
「E.J.レモンの、自然演繹の規則」である所の、「原子規則（10 primitive rules）」である所の、
「Ａ、ＭＰＰ、ＤＮ、ＣＰ、＆Ｉ、＆Ｅ、∨Ｉ、∨Ｅ、ＲＡＡ」によって、「証明」出来る。
然るに、
（08）
命題計算の規則は、本質的にゲンツェン（G.Gentzen）に由来するものである。
（E.J.レモン 著、論理学初歩、竹尾治一郎・浅野 楢英 訳、1973年、序ⅲ）
従って、
（07）（08）により、
（09）
（（Ｐ→Ｑ）→Ｐ）→Ｐ である所の、「パースの法則」は、
「E.J.レモンの、自然演繹の規則（ゲンツェンの自然演繹に由来する）」によって、「証明」出来る。
従って、
（01）（09）により、
（10）
（（Ｐ→Ｑ）→Ｐ）→Ｐ である所の、「パースの法則」は、「演繹定理」だけでは導くことができない（ウィキペディア）。」
とは言ふものの、「パースの法則」は、「ゲンツェンの自然演繹」だけで、導くことができる。
然るに、
（11）
１（１）　　　　　Ｐ　　Ａ
１（２）　　～Ｑ∨Ｐ　　１∨Ｉ
１（３）　　　Ｑ→Ｐ　　２含意の定義
　（４）Ｐ→（Ｑ→Ｐ）　１３ＣＰ（演繹定理）
従って、
（07）（11）により、
（12）
　Ｐ→（Ｑ→Ｐ） である所の、「ルカジェヴィッツの公理（Ⅰ）」も、
「E.J.レモンの、自然演繹の規則（ゲンツェンの自然演繹に由来する）」によって、「証明」出来る。
従って、
（02）（09）（11）（12）により、
（13）
①（（Ｐ→Ｑ）→Ｐ）→Ｐ
②  Ｐ→（Ｑ→Ｐ）
である所の、
①「パースの法則」と、
②「ルカジェヴィッツの公理（Ⅰ）」等は、 （ⅰ）
１　　　（１）　　（Ｐ→Ｑ）→Ｐ　　　Ａ
　２　　（２）　　～Ｐ∨Ｑ　　　　　　Ａ
　２　　（３）　　　Ｐ→Ｑ　　　　　　２含意の定義
１２　　（４）　　　　　　　　Ｐ　　　１３ＭＰＰ
１　　　（５）　（～Ｐ∨Ｑ）→Ｐ　　　２４ＣＰ（演繹定理）
１　　　（６）～（～Ｐ∨Ｑ）∨Ｐ　　　２含意の定義
　　７　（７）～（～Ｐ∨Ｑ）　　　　　Ａ
　　７　（８）　　Ｐ＆～Ｑ　　　　　　７ド・モルガンの法則
　　７　（９）　　Ｐ　　　　　　　　　８＆Ｅ
　　　ア（ア）　　　　　　　　Ｐ　　　Ａ
１　　　（イ）　　Ｐ　　　　　　　　　６７９アア∨Ｅ
　　　　（ウ）（（Ｐ→Ｑ）→Ｐ）→Ｐ　１イＣＰ（演繹定理）
（ⅱ）
　　　１（１）　　　　　Ｐ　　Ａ
　　　１（２）　　～Ｑ∨Ｐ　　１∨Ｉ
　　　１（３）　　　Ｑ→Ｐ　　２含意の定義
　　　　（４）Ｐ→（Ｑ→Ｐ）　１３ＣＰ（演繹定理）
といふ「自然演繹」で「導出可能（derivable）」な、「普通の、恒真式（トートロジー）」である。
令和０３年０４月０９日、毛利太。