直覺主義邏輯 -- 來自

命題演算和一階邏輯的證明理論通常被稱為經典邏輯。

直覺主義命題邏輯可以被描述為經典命題演算，其中公理模式

(1)

被替換為

(2)

類似地，直覺主義謂詞邏輯是直覺主義命題邏輯與經典一階謂詞演算的結合。

直覺主義邏輯是經典邏輯的一部分，也就是說，所有在直覺主義邏輯中可證明的公式在經典邏輯中也是可證明的。然而，即使是經典邏輯的一些基本定理在直覺主義邏輯中也不成立。當然，排中律

(3)

在直覺主義命題邏輯中不成立。

以下是一些在直覺主義命題邏輯中不可證明的命題公式的例子

(4)

(5)

以下是一些在直覺主義謂詞邏輯中不可證明的一階公式的例子

(6)

(7)

命題聯結詞的真值表定義了經典命題演算在兩個元素域上的解釋：真和假。這種解釋是經典命題演算的模型，也就是說，重言式且僅有重言式是形式定理。相比之下，直覺主義命題演算沒有有限模型，但它有可數模型。

反證法在直覺主義邏輯中是不允許的。所有直覺主義證明都是構造性的，這由以下性質證明是合理的。直覺主義命題邏輯具有析取性質：如果在直覺主義命題演算中是可證明的，那麼或在直覺主義命題演算中是可證明的。直覺主義謂詞邏輯具有存在性性質：如果是一個不含自由變數的公式，並且它在直覺主義謂詞邏輯中是可證明的，那麼存在一個不含自由變數的項使得在直覺主義謂詞邏輯中是可證明的。