直観主義命題論理で成り立たない論理式とその証明1 | 宇宙とブラックホールのQ&A (ameblo.jp)
直観主義命題論理で成り立たない論理式とその証明2 | 宇宙とブラックホールのQ&A (ameblo.jp)
---------------------------------------------
３．直観主義命題論理IPLとその周辺の話題
いくつかの有用な定理を証明抜きで載せます。
3-1
直観主義命題論理 IPLで成り立たない論理式を一通り見てきました。
式によって異なるモデルを使っているのを見て、不思議に思われた人もいるかもしれません。
古典命題論理CPLのBA1のように（BA2ほかのブール代数も全部同じですが）、そこでは IPLで証明できる式はすべて成り立ち、証明できない式はすべて成り立たないHAモデルを使えば良いのではないかと。
残念ながら、そういう便利で簡単なHAモデルは存在しないのです。
定理： IPLと双方向の対応関係にある有限HAモデルは存在しない。
（元は形式的な表現なのですが、私なりに文章で表現しているのであしからず。）
3-2
CPLでは、4つの基本命題関数 →，∧，∨，￢ のうち、→，∧，∨ の3者は他の基本関数により定義することができました。
（ただし、必要に応じて推論規則を変更する。また、￢を定義するためには代わりに零項命題関数 偽⊥を導入する必要がある。）
それでは、IPLではどうなのでしょうか？
定理： IPLにおいては、→，∧，∨，￢ のいずれの基本命題関数も他の3つの基本関数から定義することはできない。
証明：HA3モデルで証明する。HA3モデルで次の式を他の基本関数の組合せで表すことはできない。
(1) (1/2→1/4) ＝ 1/2’．
(2) (1/2∧1/2’) ＝ 3/4．
(3) (1/2∨1/2’) ＝ 1/4．
(4) ￢1 ＝ 0．
HA3
・1
│
・3/4
／ ＼
・1/2 ・1/2’
＼ ／
・1/4
│
・0
3-3
CPLの論理式と IPLの論理式の関係については、次の定理が成り立ちます。
定理：論理式 A∈WFF について、
A ∈ CPL ⇐⇒ ￢￢A ∈ IPL．
￢A ∈ CPL ⇐⇒ ￢A ∈ IPL．
（⇐⇒は、左辺と右辺が論理的同値であることを意味する）
最初の式の例として、排中律 ￢￢.A∨￢A ∈ IPL．
第2の式の例として、矛盾律 ￢.A∧￢A ∈ IPL．
（この記事の最後に、パースの法則、二重否定除去、排中律、Clebiusの法則それぞれの二重否定について IPLでの証明を載せます。）
なお、述語論理でも同様の対応関係が成り立ちますが、対応する直観主義述語論理の式は否定がたくさん入ってずっと複雑になります。
3-4
これまで、CPL、IPL、それに最小命題論理MPLの3者だけを扱ってきました。
この3者とさらに偽も含めたすべての論理式全体WFFの関係を再掲します。
MPL ⊂ IPL ⊂ CPL ⊂ WFF
≠ ≠ ≠
定理：CPLとWFFの間には、論理は存在しない。
ここで論理と呼んでいるのは、論理式の集合の閉じた集合あるいは閉包のことです。
「閉じた」あるいは「閉包」というのは、その集合の式から代入と推論規則で導かれる式はすべてその集合に含まれる、という意味です。
それでは、IPLとCPLの間ではどうでしょうか？
これに関しては次の強力な定理が成り立ちます。
定義： IPL ⊂ L ⊂ CPL をみたす論理Lを中間論理(intermediate logic)という。
≠ ≠
定理：連続体濃度の中間論理が存在する。
有限の公理をもつ論理は可算無限濃度なので、有限的に公理化できない中間論理が存在する。
なお、MPLと IPLの間については、私は情報を持ち合わせていません。
3-5
最後に、パースの法則、二重否定除去、排中律、Clebiusの法則（ IPLで証明できない方）それぞれの二重否定を IPLで証明します。
ただし、○を付けたものは最小論理MPLでは証明できないことを、Mを付けたものはMPLの範囲で証明できることを意味します。 (右増) を使うか使わないかの違いです。
・パースの法則の二重否定○
(左増)A ⇒ A
(右→)A→B.→A，A ⇒ A
(左￢)A ⇒ A→B.→A:→A
(左換)￢:.A→B.→A:→A，A ⇒
(右増)A，￢:.A→B.→A:→A ⇒
(右→)A，￢:.A→B.→A:→A ⇒ B
(左→)￢:.A→B.→A:→A ⇒ A→B A ⇒ A
(左換)￢:.A→B.→A:→A，A→B.→A ⇒ A
(右→)A→B.→A，￢:.A→B.→A:→A ⇒ A
(左￢)￢:.A→B.→A:→A ⇒ A→B.→A:→A
(左減)￢:.A→B.→A:→A，￢:.A→B.→A:→A ⇒
(右￢)￢:.A→B.→A:→A ⇒
⇒ ￢￢:.A→B.→A:→A ／／
・二重否定除去の二重否定○
(左増)A ⇒ A
(右→)￢￢A，A ⇒ A
(左￢)A ⇒ ￢￢A→A
(左換)￢.￢￢A→A，A ⇒
(右￢)A，￢.￢￢A→A ⇒
(左￢)￢.￢￢A→A ⇒ ￢A
(右増)￢￢A，￢.￢￢A→A ⇒
(右→)￢￢A，￢.￢￢A→A ⇒ A
(左￢)￢.￢￢A→A ⇒ ￢￢A→A
(左減)￢.￢￢A→A，￢.￢￢A→A ⇒
(右￢)￢.￢￢A→A ⇒
⇒ ￢￢.￢￢A→A ／／
・排中律の二重否定M
(右∨1)A ⇒ A
(左￢)A ⇒ A∨￢A，
(左換)￢.A∨￢A，A ⇒
(右￢)A，￢.A∨￢A ⇒
(右∨2)￢.A∨￢A ⇒ ￢A
(左￢)￢.A∨￢A ⇒ A∨￢A
(左減)￢.A∨￢A，￢.A∨￢A ⇒
(右￢)￢.A∨￢A ⇒
⇒ ￢￢.A∨￢A ／／
・Clebiusの法則( IPLで証明できない方)の二重否定M
(左増)A ⇒ A
(右→)￢A→A，A ⇒ A
(左￢)A ⇒ ￢A→A.→A
(左換)￢.￢A→A.→A，A ⇒
(右￢)A，￢.￢A→A.→A ⇒
(左→)￢.￢A→A.→A ⇒ ￢A A ⇒ A
(左換)￢.￢A→A.→A，￢A→A ⇒ A
(右→)￢A→A，￢.￢A→A.→A ⇒ A
(左￢)￢.￢A→A.→A ⇒ ￢A→A.→A
(左減)￢.￢A→A.→A，￢.￢A→A.→A ⇒
(右￢)￢.￢A→A.→A ⇒
⇒ ￢￢.￢A→A.→A ／／
証明のテクニックとしては、最後の方で必ず (左減) を使うのがポイントです。
二重否定の付いていない元の式をCPLで証明するのより行数が増えるのは、致し方ありませんね。
★ 毎日雨が降って洗濯のタイミングが見つかりません。部屋干しを考えなくては。
★★ 今日のロジバン 各種薬
lo crofanta 「ロﾟ ㇱロファンタ」
鎮痛剤 （（例）アスピリン、イブプロフェンなど）
lo vaxlu'a xukmi 「ロﾟ ヴァㇰㇷルﾟハ ㇰフㇰミ」
風邪薬
lo canti xukmi 「ロﾟ シャンティ ㇰフㇰミ」
胃腸薬
crofanta ： 鎮痛剤 だ<- cro+fanta, cro<- cortu
cortu ： 痛みを感じる，x1(者)は x2(箇所)に；x2が痛い。-cor-, -cro-
fanta ： 発生を防ぐ/抑える，x1は x2(事)の
vaxlu'a ： (肺より上の)呼吸器系の<- vax+lu’a, vax<- vasxu, lu’a<- pluta
vasxu ： 吸う/吐く，x1は x2(気体)を。-vax-, -va’u-
pluta ： 経路/道筋だ，x1は x2(終点)･x3(起点)･x4(途中の点の集合)。-lut-, -lu’a-
xukmi ： 化学薬品/化学物質だ，x1は x2(成分)・x3(純度)の。-xum-, -xu’i-
canti ： 消化器官/胃腸だ，x1は x2(本体)の
各種の薬を表す表現です。
薬は普通は xukmi ですが、以前の例文で velmikce 「治療手段」で薬を表すものもありました。
出典は、
ロジバン語会話集 - ウィキトラベル (wikitravel.org) 買い物の項