「ルカジェヴィッツの３つの公理」と「E.J.レモンの１０個の規則」。

（01）
ジョン・レモンが開発した自然演繹の体系は、証明の構文規則に関する次のような「１０個の基本的規則（10 Primitive rules）」だけを持つ。
１.仮定の規則（Ａ）
２.肯定肯定式（ＭＰＰ）
３.否定否定式（ＭＴＴ）
４.二重否定律（ＤＮ）
５.条件的証明（ＣＰ）
６.＆-導入　 （＆Ｉ）
７.＆-除去   （＆Ｅ）
８.∨-導入   （∨Ｉ）
９.∨-除去   （∨Ｅ）
10.背理法    （ＲＡＡ）
（E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳、1973年、５０・５１頁を参照）
然るに、
（02）
最後に注意してよいことは、ＭＴＴは原始的規則と解す必要はなく、他の規則から導出される規則としてえられるということである。つまり、
５５　Ｐ→Ｑ，～Ｑ├ ～Ｐ
　１　　（１）　Ｐ→Ｑ　Ａ
　　２　（２）　　～Ｑ　Ａ
　　　３（３）　Ｐ　　　Ａ
　１　３（４）　　　Ｑ　１３ＭＰＰ
　１２３（５）～Ｑ＆Ｑ　２４＆Ｉ
　１２　（６）～Ｐ　　　３５ＲＡＡ
（E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳、1973年、７８頁）
然るに、
（03）
　１　　（１）　Ｐ→Ｑ　Ａ
　　２　（２）　Ｐ　　　Ａ
　　　３（３）　　～Ｑ　Ａ
　１　３（４）～Ｐ　　　１３ＭＴＴ
　１２３（５）Ｐ＆～Ｐ　２３＆Ｉ
　１２　（６）　～～Ｑ　３５ＲＡＡ
　１２　（７）　　　Ｑ　６ＤＮ
従って、
（02）（03）により、
（04）
「ＭＴＴは原始的規則と解す必要はなく、他の規則（ＭＰＰ）から導出される規則としてえられる」といふのであれば、
「ＭＰＰも原始的規則と解す必要はなく、他の規則（ＭＴＴ）から導出される規則としてえられる」といふことになる。
加へて、
（05）
練習問題
EXERCCISES
１　１０個の原始的規則のみを用ひて、次の連式を証明せよ。
１　Using only 10 Primitive rules, prove the following sequents;
（E.J.レモン、論理学初歩、竹尾治一郎・浅野楢英 訳、1973年、７９頁）
従って、
（01）～（05）により、
（06）
「ジョン・レモンが開発した体系 L は、証明の構文規則に関する次のような　９つの基本的規則だけを持つ（ウィキペディア）。」といふのは、意図的なマチガイであって、
「ジョン・レモンが開発した体系 L は、証明の構文規則に関する次のような１０個の基本的規則だけを持つ。」とするのが、正しい。
然るに、
（07）
［公理］
　ルカジェヴィッツによる公理
（１）　Ｐ→（Ｑ→Ｐ）
（２）［Ｐ→（Ｑ→Ｒ）］→［（Ｐ→Ｑ）→（Ｐ→Ｒ）］
（３）（～Ｐ→～Ｑ）→（Ｑ→Ｐ）　
これはフレーゲが提出した６つの公理を簡単にしたものである。
（沢田允、現代論理学入門、1962年、１７３頁）
然るに、
（08）
（ⅰ）
１　　　　　（１）　　Ｐ　　　　　Ａ
１　　　　　（２）　～Ｑ∨　Ｐ　　１∨Ｉ
　３　　　　（３）　　Ｑ＆～Ｐ　　Ａ
　　４　　　（４）　～Ｑ　　　　　Ａ
　３　　　　（５）　　Ｑ　　　　　３＆Ｅ
　３４　　　（６）　～Ｑ＆Ｑ　　　４５＆Ｉ
　　４　　　（７）～（Ｑ＆～Ｐ）　３６ＲＡＡ
　　　８　　（８）　　　　　Ｐ　　Ａ
　３　　　　（９）　　　　～Ｐ　　３＆Ｅ
　３　８　　（ア）　　Ｐ＆～Ｐ　　８９＆Ｉ
　　　８　　（イ）～（Ｑ＆～Ｐ）　３アＲＡＡ
１　　　　　（ウ）～（Ｑ＆～Ｐ）　２４７８イ∨Ｅ
　　　　エ　（エ）　　Ｑ　　　　　Ａ
　　　　　オ（オ）　　　　～Ｐ　　Ａ
　　　　エオ（カ）　　Ｑ＆～Ｐ　　エオ＆Ｉ
１　　　エオ（キ）～（Ｑ＆～Ｐ）
　　　　　　　　　　（Ｑ＆～Ｐ）　ウカ＆Ｉ
１　　　エ　（ク）　　　～～Ｐ　　オキＲＡＡ
１　　　エ　（ケ）　　　　　Ｐ　　クＤＮ
１　　　　　（コ）　　　Ｑ→Ｐ　　エケＣＰ
　　　　　　（サ）Ｐ→（Ｑ→Ｐ）　１コＣＰ
（ⅱ）
１　　（１）　Ｐ→（Ｑ→Ｒ）　　　　　　　　　　　　　　　　Ａ
　２　（２）　Ｐ　　　　　　　　　　　　　　　　　　　　　　Ａ
　　３（３）　Ｐ→　Ｑ　　　　　　　　　　　　　　　　　　　Ａ
１２　（４）　　　　Ｑ→Ｒ　　　　　　　　　　　　　　　　　１２ＭＰＰ
　２３（５）　　　　Ｑ　　　　　　　　　　　　　　　　　　　２３ＭＰＰ
１２３（６）　　　　　　Ｒ　　　　　　　　　　　　　　　　　４５ＭＰＰ
１　３（７）　　　　　　　　　　　　Ｐ→Ｒ　　　　　　　　　２６ＣＰ
１　　（８）　　　　　　　　　　　（Ｐ→Ｑ）→（Ｐ→Ｒ）　　３７ＣＰ
　　　（９）［Ｐ→（Ｑ→Ｒ）］→［（Ｐ→Ｑ）→（Ｐ→Ｒ）］　１８ＣＰ
（ⅲ）
１　（１）　～Ｐ→～Ｑ　　　　　　　　Ａ
　２（２）　　　　　　　　　Ｑ　　　　Ａ
　２（３）　　　　　　　～～Ｑ　　　　２ＤＮ
１２（４）　　　　　　　～～Ｐ　　　　１３ＭＴＴ
１２（５）　　　　　　　　　Ｐ　　　　４ＤＮ
１　（６）　　　　　　　　　Ｑ→Ｐ　　２５ＣＰ
　　（７）（～Ｐ→～Ｑ）→（Ｑ→Ｐ）　１６ＣＰ
従って、
（01）（06）（07）（08）により、
（09）
フレーゲが提出した６つの公理を簡単にしたものである所の、
（１）　Ｐ→（Ｑ→Ｐ）
（２）［Ｐ→（Ｑ→Ｒ）］→［（Ｐ→Ｑ）→（Ｐ→Ｒ）］
（３）（～Ｐ→～Ｑ）→（Ｑ→Ｐ）
といふ「ルカジェヴィッツによる３つの公理」は、「E.J.レモンの１０個の規則」によって、「証明」出来る。
然るに、
（10）
（ⅰ）
１　　　　　（１）　　Ｐ　　　　　Ａ
１　　　　　（２）　～Ｑ∨　Ｐ　　１∨Ｉ
　３　　　　（３）　　Ｑ＆～Ｐ　　Ａ
　　４　　　（４）　～Ｑ　　　　　Ａ
　３　　　　（５）　　Ｑ　　　　　３＆Ｅ
　３４　　　（６）　～Ｑ＆Ｑ　　　４５＆Ｉ
　　４　　　（７）～（Ｑ＆～Ｐ）　３６ＲＡＡ
　　　８　　（８）　　　　　Ｐ　　Ａ
　３　　　　（９）　　　　～Ｐ　　３＆Ｉ
　３　８　　（ア）　　Ｐ＆～Ｐ　　８９＆Ｉ
　　　８　　（イ）～（Ｑ＆～Ｐ）　３アＲＡＡ
１　　　　　（ウ）～（Ｑ＆～Ｐ）　２４７８イ∨Ｅ
　　　　エ　（エ）　　Ｑ　　　　　Ａ
　　　　　オ（オ）　　　　～Ｐ　　Ａ
　　　　エオ（カ）　　Ｑ＆～Ｐ　　エオ＆Ｉ
１　　　エオ（キ）～（Ｑ＆～Ｐ）
　　　　　　　　　　（Ｑ＆～Ｐ）　ウカ＆Ｉ
１　　　エ　（ク）　　　～～Ｐ　　オキＲＡＡ
１　　　エ　（ケ）　　　　　Ｐ　　クＤＮ
１　　　　　（コ）　　　Ｑ→Ｐ　　エケＣＰ
　　　　　　（サ）Ｐ→（Ｑ→Ｐ）　１コＣＰ
に於いて、
Ｑ＝～Ｑ
といふ「代入（Substitution）」を行ふと、
１　　　　　（１）　　　Ｐ　　　　　Ａ
１　　　　　（２）　～～Ｑ∨　Ｐ　　１∨Ｉ
　３　　　　（３）　　～Ｑ＆～Ｐ　　Ａ
　　４　　　（４）　～～Ｑ　　　　　Ａ
　３　　　　（５）　　～Ｑ　　　　　３＆Ｅ
　３４　　　（６）　～～Ｑ＆～Ｑ　　４５＆Ｉ
　　４　　　（７）～（～Ｑ＆～Ｐ）　３６ＲＡＡ
　　　８　　（８）　　　　　　Ｐ　　Ａ
　３　　　　（９）　　　　　～Ｐ　　３＆Ｉ
　３　８　　（ア）　　　Ｐ＆～Ｐ　　８９＆Ｉ
　　　８　　（イ）～（～Ｑ＆～Ｐ）　３アＲＡＡ
１　　　　　（ウ）～（～Ｑ＆～Ｐ）　２４７８イ∨Ｅ
　　　　エ　（エ）　　～Ｑ　　　　　Ａ
　　　　　オ（オ）　　　　　～Ｐ　　Ａ
　　　　エオ（カ）　　～Ｑ＆～Ｐ　　エオ＆Ｉ
１　　　エオ（キ）～（～Ｑ＆～Ｐ）
　　　　　　　　　　（～Ｑ＆～Ｐ）　ウカ＆Ｉ
１　　　エ　（ク）　　　　～～Ｐ　　オキＲＡＡ
１　　　エ　（ケ）　　　　　　Ｐ　　クＤＮ
１　　　　　（コ）　　　～Ｑ→Ｐ　　エケＣＰ
　　　　　　（サ）Ｐ→（～Ｑ→Ｐ）　１コＣＰ
然るに、
（11）
１ 代入の規則
　一つの恒真式のなかの命題変項を他の命題変項、または論理式でおきかえることによって得られた式は同じく恒真式である。
（沢田允、現代論理学入門、1962年、１７３頁）
従って、
（09）（10）（11）により、
（12）
（１）Ｐ→（　Ｑ→Ｐ）≡Ｐであるならば（Ｑであるならば、Ｐである）。
（４）Ｐ→（～Ｑ→Ｐ）≡Ｐであるならば（Ｑでないならば、Ｐである）。
に於いて、
（１）は、「ルカジェヴィッツの公理」であって、
（４）は、「ルカジェヴィッツの公理」から導かれた、「恒真式（トートロジー）」である。
然るに、
（13）
（１）Ｐであるならば（Ｑであるならば、Ｐである）。
（４）Ｐであるならば（Ｑでないならば、Ｐである）。
といふことは、
（１）Ｐであるならば（Ｑであろうと、Ｑでなかろうと、いづれにせよ、Ｐである）。
といふことである。
然るに、
（14）
（１）Ｐであるならば（Ｑであろうと、Ｑでなかろうと、いづれにせよ、Ｐである）。
といふことは、「明らかに、正しい」。
従って、
（13）（14）により、
（15）
（１）Ｐであるならば（Ｑであるならば、Ｐである）。
といふ「言ひ方」に、「不自然さ」を感じるのであれば、
（１）Ｐであるならば（Ｑであろうと、Ｑでなかろうと、いづれにせよ、Ｐである）。
といふ風に、「読み変へ」ても、かまはない。
然るに、
（16）
１（１）Ｐ　　　Ａ
　（２）Ｐ→Ｐ　１１ＣＰ
従って、
（01）（16）により、
（17）
Ｐ→Ｐ≡Ｐであるならば、Ｐである。
といふ「同一律（Principle of identity）」は、「E.J.レモンの１０個の規則」によって、「証明」出来る。
然るに、
（18）
［公理］
　ルカジェヴィッツによる公理
（１）　Ｐ→（Ｑ→Ｐ）
（２）［Ｐ→（Ｑ→Ｒ）］→［（Ｐ→Ｑ）→（Ｐ→Ｒ）］
（３）（～Ｐ→～Ｑ）→（Ｑ→Ｐ）　
［規則］
１ 代入の規則
　一つの恒真式のなかの命題変項を他の命題変項、または論理式でおきかえることによって得られた式は同じく恒真式である。
２ 推論の規則
　論理式「Ｐ」と「Ｐ→Ｑ」が共に真ならば、論理式「Ｑ」も真である。
　―中略、―
いま、右の公理（ルカジェヴィッツ）と規則とから、新しいトートロジー
　Ｐ→Ｐ
を導き出してみよう。この場合、この命題は公理と規則から導き出された定理であることが証明されたことになる。このようにして公理から導き出される式を定理とよぶ。
　―中略、―
このためにはまずルカジェヴィッツの公理２から出発して、
（２）［Ｐ→（Ｑ→Ｒ）］→［（Ｐ→Ｑ）→（Ｐ→Ｒ）］
　　　　　　のＲにＰを代入して、
（３）［Ｐ→（Ｑ→Ｐ）］→［（Ｐ→Ｑ）→（Ｐ→Ｐ）］
を得る。この（３）と、公理（１）である、
（１）　Ｐ→（Ｑ→Ｐ）
２ 推論の規則　をあてはめれば、
　　　　　　　　　　　（４）（Ｐ→Ｑ）→（Ｐ→Ｐ）
となる。　　　　　この（４）の　　Ｑに、
１ 代入の規則　により、　　　　 （Ｑ→Ｐ）を代入すると、
　　　　　　　　　　（５）［Ｐ→（Ｑ→Ｐ）］→（Ｐ→Ｐ）
となる。　　　　この（５）と、
　　　　　　　　　　（１）　Ｐ→（Ｑ→Ｐ）に対して、
２ 推論の規則　をあてはめれば、
　　　　　　　　　　　　　　　　　　　　　（６）Ｐ→Ｐ
が導出できる（沢田允、現代論理学入門、1962年、１７３～１７５頁改）。
従って、
（18）により、
（19）
「ルカジェヴィッツによる３つの公理と、代入規則と、推論の規則」により、
「Ｐ→Ｐ≡Ｐであるならば、Ｐである。」といふ「同一律」が、「導出」出来る。
従って、
（17）（18）（19）により、
（20）
例へば、
「Ｐ→Ｐ≡Ｐであるならば、Ｐである。」といふ「同一律」は、
「E.J.レモンの１０個の規則」を用ひても、
「ルカジェヴィッツによる３つの公理と、代入規則と、推論の規則」を用ひても、「証明」出来るものの、「その証明の仕方」は、「全く違ってゐる」。
然るに、
（21）
ゲンツェンのシークエント計算は、もっともっと私たちの直観から遠いものとなっています（簡単には説明できないので、ここではお見せしません）。
（小島寛之、論理と証明に強くなる、2017年、１３６頁）
（22）
この３つの演算システムは、演算能力は同一なのですが、見た目が違うし、それぞれに固有の特徴があります。
（小島寛之、論理と証明に強くなる、2017年、１３６頁）
従って、
（20）（21）（22）により、
（23）
「シークエント計算」に於いて、
「Ｐ→Ｐ≡Ｐであるならば、Ｐである。」といふ「同一律」が、「公理」ではないならば、
「シークエント計算」に於ける、
「Ｐ→Ｐ≡Ｐであるならば、Ｐである。」といふ「同一律」の「証明」は、
「ルカジェヴィッツによる３つの公理と、代入規則と、推論の規則」による「証明」よりも、「もっともっと私たちの直観から遠いもの」である。
といふことに、なりそうである。
令和０２年０１月２２日、毛利太。