直觉主义逻辑

直觉主义逻辑或构造性逻辑是最初由阿兰德·海廷开发的为鲁伊兹·布劳威尔的数学直觉主义计划提供形式基础的符号逻辑。这个系统保持跨越生成导出命题的变换的证实性而不是真理性。从实用的观点，也有使用直觉逻辑的强烈动机，因为它有存在性质，这使它还适合其他形式的数学构造主义。

语法

Rieger-Nishimura 格。它的节点是不别直觉逻辑等价之异的一元命题公式，按直觉逻辑蕴含排序。

直觉逻辑的公式的语法类似于命题逻辑或一阶逻辑。但是直觉逻辑的连结词不像经典逻辑那样是可互定义的，因此它们的选择是重要的。在直觉命题逻辑中通常使用 →, ∧, ∨, ⊥ 作为基本连结词，把 ¬ 作为 ¬A = (A → ⊥) 的简写处理。在直觉一阶逻辑中量词 ∃, ∀ 都是需要的。

不同在于很多经典逻辑的重言式在直觉逻辑中不再是可证明的。例子不只包括排中律 P ∨ ¬P，还有皮尔士定律 ((P → Q) → P) → P，甚至还有双重否定除去。在经典逻辑中，P → ¬¬P 和 ¬¬P → P 二者都是定理。在直觉逻辑中，只有前者是定理: 双重否定可以介入但不能除去。

对很多经典有效重言式不是直觉逻辑的定理的观察导致了弱化经典逻辑的证明论的想法。

根岑发现简单限制他的系统LK（他的经典逻辑的相继式演算）就导致了关于直觉逻辑的一个可靠和完备的系统。他称之为系统LJ。

推理规则是肯定前件，公理有:

THEN-1: φ → (χ → φ)

THEN-2: (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))

AND-1: φ ∧ χ → φ

AND-2: φ ∧ χ → χ

AND-3: φ → (χ → (φ ∧ χ))

OR-1: φ → φ ∨ χ

OR-2: χ → φ ∨ χ

OR-3: (φ → ψ) → ((χ → ψ) → (φ ∨ χ → ψ))

NOT-1: (φ → χ) → ((φ → ¬χ) → ¬ φ)

NOT-2: φ → (¬φ → χ)