「ルカジェヴィッツの公理」と「自然演繹の規則」。

（01）
１ 原始的規則あるい導出された規則を、既に証明されたどのような連式あるいは定理とでも、ともに用いて、次の連式を証明せよ。
１ Using primitive or derived rules, together with any sequents or theorems already proved, prove the followint sequent.
１ 兎に角、次の連式を証明せよ。
（１）├ Ｐ→（Ｑ→Ｐ）：ルカジェヴィッツの公理１
（証明ａ）
　　（１）　　　Ｐ∨～Ｐ　　ＴＩ（排中律）
２　（２）　　　Ｐ　　　　　Ａ
２　（３）　　　～Ｑ∨Ｐ　　２∨Ｉ
２　（４）　　　　Ｑ→Ｐ　　３含意の定義
　　（５）　Ｐ→（Ｑ→Ｐ）　２４ＣＰ
　６（６）　　　　　～Ｐ　　Ａ
　６（７）～Ｐ∨（Ｑ→Ｐ）　６∨Ｉ
　６（８）　Ｐ→（Ｑ→Ｐ）　７含意の定義
　　（９）　Ｐ→（Ｑ→Ｐ）　１２５７８∨Ｅ
　　（〃）Ｐならば（ＱならばＰである）。
（証明ｂ）
１　　　（１）　～（Ｐ∨～Ｐ）　　Ａ
　２　　（２）　　　Ｐ　　　　　　Ａ
　２　　（３）　　　Ｐ∨～Ｐ　　　２∨Ｉ
１２　　（４）　～（Ｐ∨～Ｐ）＆
　　　　　　　　　（Ｐ∨～Ｐ）　　１３＆Ｉ
１　　　（５）　　～Ｐ　　　　　　２４ＲＡＡ
１　　　（６）　　　Ｐ∨～Ｐ　　　５∨Ｉ
１　　　（７）　～（Ｐ∨～Ｐ）＆
　　　　　　　　　（Ｐ∨～Ｐ）　　１６＆Ｉ
１　　　（８）～～（Ｐ∨～Ｐ）　　１７ＲＡＡ
　　　　（９）　　　Ｐ∨～Ｐ　　　８ＤＮ
　　ア　（ア）　　　Ｐ　　　　　　Ａ
　　ア　（イ）　　　～Ｑ∨Ｐ　　　ア∨Ｉ
　　ア　（ウ）　　　　Ｑ→Ｐ　　　イ含意の定義
　　　　（エ）　Ｐ→（Ｑ→Ｐ）　　アウＣＰ
　　　オ（オ）　　　　　～Ｐ　　　Ａ
　　　オ（カ）～Ｐ∨（Ｑ→Ｐ）　　オ∨Ｉ
　　　オ（キ）　Ｐ→（Ｑ→Ｐ）　　カ含意の定義
　　　　（ク）　Ｐ→（Ｑ→Ｐ）　　９アエオキ∨Ｅ
　　　　（〃）Ｐならば（ＱならばＰである）。
従って、
（01）により、
（02）
（証明ａ）は、　「９行」からなり、「排中律（Ｐ∨～Ｐ）」　　　　　から始まってゐて、
（証明ｂ）は、「１７行」からなり、「排中律（Ｐ∨～Ｐ）」の「証明」から始まってゐる。
従って、
（02）により、
（03）
あるいは、
　Ｐ∨～Ｐ
などいつでも使える出発点（公理）として準備したほうがいいのではないか、と思うでしょう。しかし、そんな必要はないのです。なぜなら、「排中律」は自然演繹で演繹できてしまうのです（小島寛之、証明と論理に強くなる、2017年、１４１頁改）。
といふ、ことになる。
然るに、
（04）
（証明ｃ）
１（１）　　　　　Ｐ　　Ａ
１（２）　　～Ｑ∨Ｐ　　１∨Ｉ
１（３）　　　Ｑ→Ｐ　　２含意の定義
　（４）Ｐ→（Ｑ→Ｐ）　１３ＣＰ
　（〃）Ｐならば（ＱならばＰである）。
（証明ｄ）
１　　　　　（１）　　　　　Ｐ　　　Ａ
１　　　　　（２）　～Ｑ∨　Ｐ　　　１∨Ｉ
　３　　　　（３）　　Ｑ＆～Ｐ　　　Ａ
　　４　　　（４）　～Ｑ　　　　　　Ａ
　３　　　　（５）　　Ｑ　　　　　　３＆Ｅ
　３４　　　（６）　～Ｑ＆　Ｑ　　　４５＆Ｉ
　　４　　　（７）～（Ｑ＆～Ｐ）　　３６ＲＡＡ
　　　８　　（８）　　　　　Ｐ　　　Ａ
　３　　　　（９）　　　　～Ｐ　　　３＆Ｅ
　３　８　　（ア）　　Ｐ＆～Ｐ　　　８９＆Ｉ
　　　８　　（イ）～（Ｑ＆～Ｐ）　　３アＲＡＡ
１　　　　　（ウ）～（Ｑ＆～Ｐ）　　２４７８イ∨Ｅ
　　　　エ　（エ）　　Ｑ　　　　　　Ａ
　　　　　オ（オ）　　　　～Ｐ　　　Ａ
　　　　エオ（カ）　　Ｑ＆～Ｐ　　　エオ＆Ｉ
１　　　エオ（キ）～（Ｑ＆～Ｐ）＆
　　　　　　　　　　（Ｑ＆～Ｐ）　　ウカ＆Ｉ
１　　　エ　（ク）　　　～～Ｐ　　　オキＲＡＡ
１　　　エ　（ケ）　　　　　Ｐ　　　クＤＮ
１　　　　　（コ）　　　Ｑ→Ｐ　　　エケＣＰ
　　　　　　（サ）Ｐ→（Ｑ→Ｐ）　　１コＣＰ
　　　　　　（〃）Ｐならば（ＱならばＰである）。
従って、
（04）により、
（05）
（証明ｃ）は、　「４行」からなり、「含意の定義」を用ひてゐて、
（証明ｄ）は、「２１行」からなり、「含意の定義」の「証明」を、「証明の過程」で、行ってゐる。
然るに、
（06）
① 仮定（Ａ）
② 前件肯定（ＭＰＰ）
③ 後件否定（ＭＴＴ）
④ 二重否定（ＤＮ）
⑤ 条件法的証明（ＣＰ）
⑥ 連言導入（＆Ｉ）
⑦ 連言除去（＆Ｅ）
⑧ 選言導入（∨Ｉ）
⑨ 選言除去（∨Ｅ）
⑩ 背理法（ＲＡＡ）
を、「原始的規則（10 primitive rules）」といふ。
従って、
（06）により、
（07）
「原始的規則（10 primitive rules）」の中に、
⑪ 含意の定義
は、入ってゐない。
従って、
（04）～（07）により、
（08）
１ 原始的規則あるい導出された規則を、既に証明されたどのような連式あるいは定理とでも、ともに用いて、次の連式を証明せよ。
１ Using primitive or derived rules, together with any sequents or theorems already proved, prove the followint sequent.
１ 兎に角、次の連式を証明せよ。
（ⅰ）├ Ｐ→（Ｑ→Ｐ）：ルカジェヴィッツの公理１
ではなく、
２ 次の連式を、原始的規則のみによって証明せよ
２ Prove the following sequent by primitive rules alone:
（ⅰ）├ Ｐ→（Ｑ→Ｐ）：ルカジェヴィッツの公理１
であるならば、
（証明ｃ）
１（１）　　　　　Ｐ　　Ａ
１（２）　　～Ｑ∨Ｐ　　１∨Ｉ
１（３）　　　Ｑ→Ｐ　　２含意の定義
　（４）Ｐ→（Ｑ→Ｐ）　１３ＣＰ
　（〃）Ｐならば（ＱならばＰである）。
ではなく、
（証明ｄ）
１　　　　　（１）　　　　　Ｐ　　　Ａ
１　　　　　（２）　～Ｑ∨　Ｐ　　　１∨Ｉ
　３　　　　（３）　　Ｑ＆～Ｐ　　　Ａ
　　４　　　（４）　～Ｑ　　　　　　Ａ
　３　　　　（５）　　Ｑ　　　　　　３＆Ｅ
　３４　　　（６）　～Ｑ＆　Ｑ　　　４５＆Ｉ
　　４　　　（７）～（Ｑ＆～Ｐ）　　３６ＲＡＡ
　　　８　　（８）　　　　　Ｐ　　　Ａ
　３　　　　（９）　　　　～Ｐ　　　３＆Ｅ
　３　８　　（ア）　　Ｐ＆～Ｐ　　　８９＆Ｉ
　　　８　　（イ）～（Ｑ＆～Ｐ）　　３アＲＡＡ
１　　　　　（ウ）～（Ｑ＆～Ｐ）　　２４７８イ∨Ｅ
　　　　エ　（エ）　　Ｑ　　　　　　Ａ
　　　　　オ（オ）　　　　～Ｐ　　　Ａ
　　　　エオ（カ）　　Ｑ＆～Ｐ　　　エオ＆Ｉ
１　　　エオ（キ）～（Ｑ＆～Ｐ）＆
　　　　　　　　　　（Ｑ＆～Ｐ）　　ウカ＆Ｉ
１　　　エ　（ク）　　　～～Ｐ　　　オキＲＡＡ
１　　　エ　（ケ）　　　　　Ｐ　　　クＤＮ
１　　　　　（コ）　　　Ｑ→Ｐ　　　エケＣＰ
　　　　　　（サ）Ｐ→（Ｑ→Ｐ）　　１コＣＰ
　　　　　　（〃）Ｐならば（ＱならばＰである）。
だけが、「正解」である。
然るに、
（09）
　ルカジェヴィッツによる公理
（１）　Ｐ→（Ｑ→Ｐ）
（２）［Ｐ→（Ｑ→Ｒ）］→［（Ｐ→Ｑ）→（Ｐ→Ｒ）］
（３）（～Ｐ→～Ｑ）→（Ｑ→Ｐ）　
これはフレーゲが提出した６つの公理を簡単にしたものである。
（沢田允、現代論理学入門、1962年、１７３頁）
従って、
（01）～（09）により、
（10）
　ルカジェヴィッツによる公理
（１）　Ｐ→（Ｑ→Ｐ）
（２）［Ｐ→（Ｑ→Ｒ）］→［（Ｐ→Ｑ）→（Ｐ→Ｒ）］
（３）（～Ｐ→～Ｑ）→（Ｑ→Ｐ）　
といふ「３つの公理（Axioms）」の中の、
（１）　Ｐ→（Ｑ→Ｐ）
については、
① 仮定（Ａ）
② 前件肯定（ＭＰＰ）
③ 後件否定（ＭＴＴ）
④ 二重否定（ＤＮ）
⑤ 条件法的証明（ＣＰ）
⑥ 連言導入（＆Ｉ）
⑦ 連言除去（＆Ｅ）
⑧ 選言導入（∨Ｉ）
⑨ 選言除去（∨Ｅ）
⑩ 背理法（ＲＡＡ）
といふ、「自然演繹の規則」を用ひて、「証明済み」である。
然るに、
（11）
（ⅱ）├［Ｐ→（Ｑ→Ｒ）］→［（Ｐ→Ｑ）→（Ｐ→Ｒ）］
１　　（１）　Ｐ→（Ｑ→Ｒ）　　　　　　　　　　　　　　　　Ａ
　２　（２）  Ｐ→　Ｑ　　　　　　　　　　　　　　　　　　　Ａ
　　３（３）　Ｐ　　　　　　　　　　　　　　　　　　　　　　Ａ
１　３（４）　　　　Ｑ→Ｒ　　　　　　　　　　　　　　　　　１３ＭＰＰ
１２３（５）　　　　Ｑ　　　　　　　　　　　　　　　　　　　２３ＭＰＰ
１２３（６）　　　　　　Ｒ　　　　　　　　　　　　　　　　　４５ＭＰＰ
１２　（７）　　　　　　　　　　　　　　　　　　Ｐ→Ｒ　　　３６ＭＰＰ
１　　（８）　　　　　　　　　　　（Ｐ→Ｑ）→（Ｐ→Ｒ）　　２７ＣＰ
      （９）［Ｐ→（Ｑ→Ｒ）］→［（Ｐ→Ｑ）→（Ｐ→Ｒ）］　１８ＣＰ
（ⅲ）├（～Ｐ→～Ｑ）→（Ｑ→Ｐ）　
１　　（１）　～Ｐ→～Ｑ　　　　　　　　Ａ
　２　（２）　　　　　Ｑ　　　　　　　　Ａ
　　３（３）　～Ｐ　　　　　　　　　　　Ａ
１　３（４）　　　　～Ｑ　　　　　　　　１３ＭＰＰ
１２３（５）　　Ｑ＆～Ｑ　　　　　　　　３４＆Ｉ
１２　（６）～～Ｐ　　　　　　　　　　　３５ＲＡＡ
１２　（７）　　Ｐ　　　　　　　　　　　６ＤＮ
１　　（８）　　　　　　　　　Ｑ→Ｐ　　２７ＣＰ
　　　（９）（～Ｐ→～Ｑ）→（Ｑ→Ｐ）　１８ＣＰ
従って、
（10）（11）により、
（12）
　ルカジェヴィッツによる公理
（１）　Ｐ→（Ｑ→Ｐ）
（２）［Ｐ→（Ｑ→Ｒ）］→［（Ｐ→Ｑ）→（Ｐ→Ｒ）］
（３）（～Ｐ→～Ｑ）→（Ｑ→Ｐ）　
といふ「３つの公理（Axioms）」は、３つとも、
① 仮定（Ａ）
② 前件肯定（ＭＰＰ）
③ 後件否定（ＭＴＴ）
④ 二重否定（ＤＮ）
⑤ 条件法的証明（ＣＰ）
⑥ 連言導入（＆Ｉ）
⑦ 連言除去（＆Ｅ）
⑧ 選言導入（∨Ｉ）
⑨ 選言除去（∨Ｅ）
⑩ 背理法（ＲＡＡ）
といふ、「自然演繹の規則」を用ひて、「証明」出来る。
然るに、
（13）
連式に対して１０個の原始的規則のみを用いて証明が見出されるならば、その連式を、簡単な言いかたをとって、導出可能（deriable）であるとよぶことにしよう。―中略、―
メタ定理１：すべての導出可能な連式は、トートロジーである。
（E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳、1973年、９７頁）
従って、
（12）（13）により、
（14）
　ルカジェヴィッツによる公理
（１）　Ｐ→（Ｑ→Ｐ）
（２）［Ｐ→（Ｑ→Ｒ）］→［（Ｐ→Ｑ）→（Ｐ→Ｒ）］
（３）（～Ｐ→～Ｑ）→（Ｑ→Ｐ）　
といふ「３つの公理（Axioms）」は、３つとも、「導出可能（deriable）」である。
令和０２年０２月０３日、毛利太。