直覺主義邏輯

1）語法

直覺邏輯的公式的語法類似於命題邏輯或一階邏輯。但是直覺邏輯的連結詞不像經典邏輯那樣是可互定義的，因此它們的選擇是重要的。在直覺命題邏輯中通常使用 →, ∧, ∨, ⊥ 作為基本連結詞，把 ¬ 作為 ¬A = (A → ⊥)的簡寫處理。在直覺一階邏輯中量詞 ∃, ∀ 都是需要的。

不同在於很多經典邏輯的重言式在直覺邏輯中不再是可證明的。例子不只包括排中律P ∨ ¬P，還有皮爾士定律((P →Q) →P) →P，甚至還有雙重否定除去。在經典邏輯中，P → ¬¬P 和 ¬¬P →P 二者都是定理。在直覺邏輯中，只有前者是定理: 雙重否定可以介入但不能除去。

對很多經典有效重言式不是直覺邏輯的定理的觀察導致了弱化經典邏輯的證明論的想法。

2）語義

建立在模態邏輯的語義的工作之上，索爾·阿倫·克里普克為直覺邏輯建立了另一套語義，叫做 克里普克語義或 關係語義