19/03/22 11:11:55.25 WSdp8+VY.net
>>687
つづく
古典論理との関係
古典論理の体系は次のどれかを公理に追加することによって得られる：
・排中律
・二重否定除去
・パースの法則
別の関係性としてはゲーデル＝ゲンツェン変換によるものがある。これは古典一階述語論理が直観主義一階述語論理に埋め込めることを示す。すなわち一階述語論理式が古典論理で証明可能であることと、それをゲーデル・ゲンツェン変換したものが直観主義論理で証明可能であることとが同値となる。
またグリベンコの定理によれば、命題論理式が古典論理で証明可能であることと、それを二重否定したものが直観主義論理で証明可能であることとは同値である。したがって直観主義論理は古典論理を構成的意味論の観点から拡大したものと見做すことができる。
意味論
ハイティング代数意味論
他の論理との関係
直観主義論理は双対性によって矛盾許容論理の一種であり、ブラジリアン論理、反直観主義論理、双対直観主義論理などと呼ばれる論理と対応している。[3]
直観主義論理から爆発原理を取り除いたものは最小論理として知られる。
多値論理との関係
クルト・ゲーデルは1932年に直観主義論理が多値論理ではないことを証明した。（#ハイティング代数意味論は直観主義論理の"無限多値論理"としての解釈の一種と見られる。）
様相論理との関係
直観主義命題論理の論理式は次のように様相命題論理S4の論理式に翻訳できる：
ラムダ計算
カリー＝ハワード対応はIPCと直和と直積を持つ単純型付きラムダ計算との間に拡張できる。[5]
(引用終わり)
以上