直観主義論理
Smetanich論理は古典論理よりも弱く直観主義論理より強い論理の中で極大なものだからである。
別の関係性としてはゲーデル=ゲンツェン変換によるものがある。これは古典一階述語論理が直観主義一階述語論理に埋め込めることを示す。すなわち一階述語論理式が古典論理で証明可能であることと、それをゲーデル・ゲンツェン変換したものが直観主義論理で証明可能であることとが同値となる。またグリベンコの定理によれば、命題論理式が古典論理で証明可能であることと、それを二重否定したものが直観主義論理で証明可能であることとは同値である。したがって直観主義論理は古典論理を構成的意味論の観点から拡大したものと見做すことができる。
1932年にクルト・ゲーデルは古典論理と直観主義論理の間にあるゲーデル論理の体系を定義した。これは中間論理として知られる。
直観主義論理は次のようにヒルベルト流の計算を用いても定義できる。これは古典命題論理の公理化(Propositional calculus#Alternative calculus)に類似である。
命題論理では、推論規則としてモーダスポネンス
MP: φ {\displaystyle \phi } および φ → ψ {\displaystyle \phi \to \psi } から ψ {\displaystyle \psi } を導く
を取り、公理図式として次のものを取る:
THEN-1: φ → ( χ → φ ) {\displaystyle \phi \to (\chi \to \phi )}
THEN-2: ( φ → ( χ → ψ ) ) → ( ( φ → χ ) → ( φ → ψ ) ) {\displaystyle (\phi \to (\chi \to \psi ))\to ((\phi \to \chi )\to (\phi \to \psi ))}
AND-1: φ ∧ χ → φ {\displaystyle \phi \land \chi \to \phi }
AND-2: φ ∧ χ → χ {\displaystyle \phi \land \chi \to \chi }