「排中律」への「代入例」と「直観主義論理は不思議である。」

（01）
１　（１）　～（～Ｐ∨Ｐ）　　Ａ
　２（２）　　　～Ｐ　　　　　Ａ
　２（３）　　　～Ｐ∨Ｐ　　　２∨Ｉ
１２（４）　～（～Ｐ∨Ｐ）＆
　　　　　　　（～Ｐ∨Ｐ）　　１３＆Ｉ
１　（５）　　～～Ｐ　　　　　２４ＲＡＡ
１　（６）　　　　Ｐ　　　　　５ＤＮ
１　（７）　　　～Ｐ∨Ｐ　　　６∨Ｉ
１　（８）　～（～Ｐ∨Ｐ）＆
　　　　　　　（～Ｐ∨Ｐ）　　１７＆Ｉ
　　（９）～～（～Ｐ∨Ｐ）　　１８ＲＡＡ
　　（ア）　　　～Ｐ∨Ｐ　　　９ＤＮ
従って、
（01）により、
（02）
① ～Ｐ∨Ｐ＝Ｐでないか、Ｐである（排中律）
は、「恒真式（トートロジー）」である。
従って、
（02）により、
（03）
① Ｐ＝∃ｘ（Ｆｘ＆～Ｇｘ）
であるとして、
② ～∃ｘ（Ｆｘ＆～Ｇｘ）∨∃ｘ（Ｆｘ＆～Ｇｘ）
といふ「論理式（排中律）」は、「恒真式（トートロジー）」である。
然るに、
（04）
（ⅰ）
１　　　（１）　～∃ｘ（Ｆｘ＆～Ｇｘ）∨∃ｘ（Ｆｘ＆～Ｇｘ）　Ａ
　２　　（２）　～∃ｘ（Ｆｘ＆～Ｇｘ）　　　　　　　　　　　　Ａ
　２　　（３）　∀ｘ～（Ｆｘ＆～Ｇｘ）　　　　　　　　　　　　２量化子の関係
　２　　（４）　　　～（Ｆａ＆～Ｇａ）　　　　　　　　　　　　３ＵＥ
　２　　（５）　　　　～Ｆａ∨　Ｇａ　　　　　　　　　　　　　４ド・モルガンの法則
　２　　（６）　　　　　Ｆａ→　Ｇａ　　　　　　　　　　　　　５含意の定義
　２　　（７）　　∀ｘ（Ｆｘ→　Ｇｘ）　　　　　　　　　　　　６ＵＩ
　２　　（８）～～∀ｘ（Ｆｘ→　Ｇｘ）　　　　　　　　　　　　７∨Ｉ
　２　　（９）～～∀ｘ（Ｆｘ→　Ｇｘ）∨∃ｘ（Ｆｘ＆～Ｇｘ）　７∨Ｉ
　２　　（ア）　～∀ｘ（Ｆｘ→　Ｇｘ）→∃ｘ（Ｆｘ＆～Ｇｘ）　８含意の定義
　　イ　（イ）　　　　　　　　　　　　　∃ｘ（Ｆｘ＆～Ｇｘ）　Ａ
　　イ　（ウ）～～∀ｘ（Ｆｘ→　Ｇｘ）∨∃ｘ（Ｆｘ＆～Ｇｘ）　イ∨Ｉ
　　イ　（エ）　～∀ｘ（Ｆｘ→　Ｇｘ）→∃ｘ（Ｆｘ＆～Ｇｘ）　ウ含意の定義
１　　　（オ）　～∀ｘ（Ｆｘ→　Ｇｘ）→∃ｘ（Ｆｘ＆～Ｇｘ）　１２アイエ∨Ｅ
　　　オ（カ）　　　　　　　　　　　　～∃ｘ（Ｆｘ＆～Ｇｘ）　Ａ
１　　オ（キ）～～∀ｘ（Ｆｘ→　Ｇｘ）　　　　　　　　　　　　オカＭＴＴ
１　　オ（ク）　　∀ｘ（Ｆｘ→　Ｇｘ）　　　　　　　　　　　　キＤＮ
１　　　（ケ）　～∃ｘ（Ｆｘ＆～Ｇｘ）→∀ｘ（Ｆｘ→　Ｇｘ）　オクＣＰ
（ⅱ）
１　　　（１）　～∃ｘ（Ｆｘ＆～Ｇｘ）→∀ｘ（Ｆｘ→　Ｇｘ）　Ａ
　２　　（２）　　　　　　　　　　　　　∃ｘ（Ｆｘ＆～Ｇｘ）　Ａ
　　３　（３）　　　　　　　　　　　　　　　　Ｆａ＆～Ｇａ　　Ａ
　　　４（４）　　　　　　　　　　　　　∀ｘ（Ｆｘ→　Ｇｘ）　Ａ
　　　４（５）　　　　　　　　　　　　　　　　Ｆａ→　Ｇａ　　４ＵＥ
　　３　（６）　　　　　　　　　　　　　　　　　　　～Ｇａ　　３＆Ｅ
　　３４（７）　　　　　　　　　　　　　　　～Ｆａ　　　　　　５６ＭＴＴ
　　３　（８）　　　　　　　　　　　　　　　　Ｆａ　　　　　　３＆Ｅ
　　３４（９）　　　　　　　　　　　　　　　～Ｆａ＆Ｆａ　　　７８＆Ｉ
　　３　（ア）　　　　　　　　　　　　～∀ｘ（Ｆｘ→　Ｇｘ）　４９ＲＡＡ
　２　　（イ）　　　　　　　　　　　　～∀ｘ（Ｆｘ→　Ｇｘ）　２３アＥＥ
１２　　（ウ）～～∃ｘ（Ｆｘ＆～Ｇｘ）　　　　　　　　　　　　１イＭＴＴ
１２　　（エ）　　∃ｘ（Ｆｘ＆～Ｇｘ）　　　　　　　　　　　　ウＤＮ
１　　　（オ）　　∃ｘ（Ｆｘ＆～Ｇｘ）→∃ｘ（Ｆｘ＆～Ｇｘ）　２エＣＰ
１　　　（カ）　～∃ｘ（Ｆｘ＆～Ｇｘ）∨∃ｘ（Ｆｘ＆～Ｇｘ）　オ含意の定義
従って、
（04）により、
（05）
① ～∃ｘ（Ｆｘ＆～Ｇｘ）∨∃ｘ（Ｆｘ＆～Ｇｘ）
② ～∃ｘ（Ｆｘ＆～Ｇｘ）→∀ｘ（Ｆｘ→　Ｇｘ）
に於いて、
①＝② である。
然るに、
（06）
（ⅲ）
１　　（１）　∀ｘ（Ｆｘ→　Ｇｘ）　　Ａ
　２　（２）　∃ｘ（Ｆｘ＆～Ｇｘ）　　Ａ
１　　（３）　　　　Ｆａ→　Ｇａ　　　１ＵＥ
　　４（４）　　　　Ｆａ＆～Ｇａ　　　Ａ
　　４（５）　　　　Ｆａ　　　　　　　４＆Ｅ
　　４（６）　　　　　　　～Ｇａ　　　４＆Ｅ
１　４（７）　　　　　　　　Ｇａ　　　３５ＭＰＰ
１　４（８）　　　　～Ｇａ＆Ｇａ　　　６７＆Ｉ
　　４（９）　　～（Ｆａ→　Ｇａ）　　１８ＲＡＡ
１　　（ア）　　　　Ｆａ→　Ｇａ　　　１ＵＥ
１　４（イ）　　～（Ｆａ→　Ｇａ）＆
　　　　　　　　　（Ｆａ→　Ｇａ）　　９ア＆Ｉ
　　４（ウ）～∀ｘ（Ｆｘ→　Ｇｘ）　　１イＲＡＡ
　２　（エ）～∀ｘ（Ｆｘ→　Ｇｘ）　　２４ウＥＥ
１２　（オ）　∀ｘ（Ｆｘ→　Ｇｘ）＆
　　　　　　～∀ｘ（Ｆｘ→　Ｇｘ）　　１エ＆Ｉ
１　　（カ）～∃ｘ（Ｆｘ＆～Ｇｘ）　　２オＲＡＡ
（ⅳ）
１　　　（１）～∃ｘ（Ｆｘ＆～Ｇｘ）　　Ａ
　２　　（２）　　　　Ｆａ＆～Ｇａ　　　Ａ
　２　　（３）　∃ｘ（Ｆｘ＆～Ｇｘ）　　２ＥＩ
１２　　（４）～∃ｘ（Ｆｘ＆～Ｇｘ）＆
　　　　　　　　∃ｘ（Ｆｘ＆～Ｇｘ）　　１３＆Ｉ
１　　　（５）　　～（Ｆａ＆～Ｇａ）　　２４ＲＡＡ
　　６　（６）　　　　Ｆａ　　　　　　　Ａ
　　　７（７）　　　　　　　～Ｇａ　　　Ａ
　　６７（８）　　　　Ｆａ＆～Ｇａ　　　６７＆
１　６７（９）　　～（Ｆａ＆～Ｇａ）＆
　　　　　　　　　　（Ｆａ＆～Ｇａ）　　５８＆Ｉ
１　６　（ア）　　　　　　～～Ｇａ　　　７９ＲＡＡ
１　６　（イ）　　　　　　　　Ｇａ　　　アＤＮ
１　　　（ウ）　　　　Ｆａ→　Ｇａ　　　６イＣＰ
１　　　（エ）　∀ｘ（Ｆｘ→　Ｇｘ）　　ウＵＩ
従って、
（06）により、
（07）
③ 　∀ｘ（Ｆｘ→　Ｇｘ）
④ ～∃ｘ（Ｆｘ＆～Ｇｘ）
に於いて、
③＝④ である。
従って、
（05）（06）（07）により、
（08）
① ～∃ｘ（Ｆｘ＆～Ｇｘ）∨∃ｘ（Ｆｘ＆～Ｇｘ）
② ～∃ｘ（Ｆｘ＆～Ｇｘ）→∀ｘ（Ｆｘ→　Ｇｘ）
③ 　∀ｘ（Ｆｘ→　Ｇｘ）
④ ～∃ｘ（Ｆｘ＆～Ｇｘ）
に於いて、
①＝② であって、尚且つ、
③＝④ である。
従って、
（03）（08）により、
（09）
① ～∃ｘ（Ｆｘ＆～Ｇｘ）∨　∃ｘ（Ｆｘ＆～Ｇｘ）
② ～∃ｘ（Ｆｘ＆～Ｇｘ）→　∀ｘ（Ｆｘ→　Ｇｘ）
③ 　∀ｘ（Ｆｘ→　Ｇｘ）→～∃ｘ（Ｆｘ＆～Ｇｘ）
に於いて、
① は、「排中律（トートロジー）」であって、
② も、「排中律（トートロジー）」であって、
③ も、「排中律（トートロジー）」であって、
①＝②＝③ である。
然るに、
（10）
いまひとつの、特に言っておいてよいほどに一般的な語法は、「Ｆをもつ幾らかのものはＧをもたない」あるいは「ＦをもつがＧをもたないものが存在する」（「幾らかのフランス人は寛大でない」、「寛大でないフランス人が存在する」）である。これは明らかに、「ｘがＦをもちそしてｘがＧをもたないようなｘが存在する」、すなわち、
　（27）∃ｘ（Ｆｘ＆～Ｇｘ）
となる（論理学初歩、E.J.レモン、竹尾 治一郎・浅野 楢英 訳、1973年、１２３頁）。
従って、
（03）（09）（10）により、
（11）
①（寛大でないフランス人は存在しないか）、または（寛大でないフランス人は存在する）。
②（寛大でないフランス人が存在しない）ならば（すべてのフランス人は寛大である）。
③（すべてのフランス人が寛大である）ならば（寛大でないフランス人は存在しない）。
に於いて、
① は、「排中律（トートロジー）」であって、
② は、「排中律（トートロジー）」であって、
③ は、「排中律（トートロジー）」であって、尚且つ、
①＝②＝③ である。
然るに、
（12）
排中律 ～Ｐ∨Ｐ の拒絶は古典論理に親しい者には奇妙に思われるが、直観主義論理で命題論理式を証明するには、全ての可能な命題論理式に対して真または偽の証明が要求され、これは様々な理由によって不可能である（ウィキペディア）。
従って、
（11）（12）により、
（13）
「古典論理」とは異なり、「直観主義論理」にの場合は、例へば、
③（すべてのフランス人が寛大である）ならば（寛大でないフランス人は存在しない）。
といふ「排中律」を、「恒真式（トートロジー）」である。とは、認めない（？）。
といふ、ことになる。
令和０３年０５月１３日、毛利太。