直観主義論理
AND-3: φ → ( χ → ( φ ∧ χ ) ) {\displaystyle \phi \to (\chi \to (\phi \land \chi ))}
OR-1: φ → φ ∨ χ {\displaystyle \phi \to \phi \lor \chi }
OR-2: χ → φ ∨ χ {\displaystyle \chi \to \phi \lor \chi }
OR-3: ( φ → ψ ) → ( ( χ → ψ ) → ( φ ∨ χ → ψ ) ) {\displaystyle (\phi \to \psi )\to ((\chi \to \psi )\to (\phi \lor \chi \to \psi ))}
FALSE: ⊥ → φ {\displaystyle \bot \to \phi }
一階述語論理の体系を作るには次の推論規則を加える:
∀ {\displaystyle \forall } -GEN: ψ → φ {\displaystyle \psi \to \phi } から ψ → ( ∀ x φ ) {\displaystyle \psi \to (\forall x\ \phi )} を導く;ただし固有変数条件「 x {\displaystyle x} は ψ {\displaystyle \psi } に自由に現れない」を満たす
証明論的な視点から見ると、直観主義論理は古典論理の制限であって排中律や二重否定除去が公理として許容されないものである。排中律や二重否定除去はいくつかの論理式に対しては個別に証明できることがあるけれども、古典論理のように普遍的に成立することはない。
直観主義論理の色々な意味論が研究されている。ひとつの意味論は古典的なブール代数値意味論を写しとったものでブール代数の代わりにハイティング代数を用いる。別の意味論ではクリプキ・モデルを用いる。
直観主義論理は実際的な有用性を持つ。何故ならばこの制限によって存在具体性を持つ証明が作られるからであり、これは直観主義論理が数学的構成主義のある形態として適当なものとする。非正式には、ある対象が存在することの構成的証明があれば、その構成的証明はそのような対象の例を生成するアルゴリズムとして使える、ということを意味する。
形式化された直観主義論理はアレン・ハイティングによってヤン・ブラウワーの直観主義プログラムの形式的な基礎として発展せられたものである。