直覺主義邏輯

直覺主義邏輯或構造性邏輯是最初由阿蘭德·海廷開發的為魯伊茲·布勞威爾的數學直覺主義計畫提供形式基礎的符號邏輯。這個系統保持跨越生成導出命題的變換的證實性而不是真理性。從實用的觀點，也有使用直覺邏輯的強烈動機，因為它有存在性質，這使它還適合其他形式的數學構造主義。
1）語法
直覺邏輯的公式的語法類似於命題邏輯或一階邏輯。但是直覺邏輯的連結詞不像經典邏輯那樣是可互定義的，因此它們的選擇是重要的。在直覺命題邏輯中通常使用 →, ∧, ∨, ⊥ 作為基本連結詞，把 ¬ 作為 ¬A = (A → ⊥)的簡寫處理。在直覺一階邏輯中量詞 ∃, ∀ 都是需要的。
不同在於很多經典邏輯的重言式在直覺邏輯中不再是可證明的。例子不只包括排中律 P ∨ ¬P，還有皮爾士定律((P → Q) → P) → P，甚至還有雙重否定除去。在經典邏輯中，P → ¬¬P 和 ¬¬P → P 二者都是定理。在直覺邏輯中，只有前者是定理: 雙重否定可以介入但不能除去。
對很多經典有效重言式不是直覺邏輯的定理的觀察導致了弱化經典邏輯的證明論的想法。
2）語義
建立在模態邏輯的語義的工作之上，索爾·阿倫·克里普克為直覺邏輯建立了另一套語義，叫做克里普克語義或關係語義