直觉主义逻辑 -- 来自

命题演算和一阶逻辑的证明理论通常被称为经典逻辑。

直觉主义命题逻辑可以被描述为经典命题演算，其中公理模式

(1)

被替换为

(2)

类似地，直觉主义谓词逻辑是直觉主义命题逻辑与经典一阶谓词演算的结合。

直觉主义逻辑是经典逻辑的一部分，也就是说，所有在直觉主义逻辑中可证明的公式在经典逻辑中也是可证明的。然而，即使是经典逻辑的一些基本定理在直觉主义逻辑中也不成立。当然，排中律

(3)

在直觉主义命题逻辑中不成立。

以下是一些在直觉主义命题逻辑中不可证明的命题公式的例子

(4)

(5)

以下是一些在直觉主义谓词逻辑中不可证明的一阶公式的例子

(6)

(7)

命题联结词的真值表定义了经典命题演算在两个元素域上的解释：真和假。这种解释是经典命题演算的模型，也就是说，重言式且仅有重言式是形式定理。相比之下，直觉主义命题演算没有有限模型，但它有可数模型。

反证法在直觉主义逻辑中是不允许的。所有直觉主义证明都是构造性的，这由以下性质证明是合理的。直觉主义命题逻辑具有析取性质：如果在直觉主义命题演算中是可证明的，那么或在直觉主义命题演算中是可证明的。直觉主义谓词逻辑具有存在性性质：如果是一个不含自由变量的公式，并且它在直觉主义谓词逻辑中是可证明的，那么存在一个不含自由变量的项使得在直觉主义谓词逻辑中是可证明的。