直観主義論理（ちょっかんしゅぎろんり、英: intuitionistic logic）または直観論理（ちょっかんろんり）、あるいは構成的論理（こうせいてきろんり、英: constructive logic）とは、ある種の論理体系であり、伝統的な真理値の概念が構成的証明の概念に置き換わっている点で古典論理とは異なる。例えば古典論理では、全ての論理式に真か偽の真理値 ( { ⊤ , ⊥ } {\displaystyle \{\top ,\bot \}} ) が割り当てられる。このときその真理値に対する直接的なエビデンスを持つか否かは問題にしない。これはどのような曖昧な命題においても「真か偽かが決定可能である」ということを意味する。対照的に、直観主義論理では確定的に論理式に真理値を割り当てるのではなく、それが真であるとは「直接的なエビデンス」つまり「証明」があることと見做す。

証明論的な視点から見ると、直観主義論理は古典論理の制限であって排中律や二重否定除去が公理として許容されないものである。排中律や二重否定除去はいくつかの論理式に対しては個別に証明できることがあるけれども、古典論理のように普遍的に成立することはない。

直観主義論理の色々な意味論が研究されている。ひとつの意味論は古典的なブール代数値意味論を写しとったものでブール代数の代わりにハイティング代数を用いる。別の意味論ではクリプキ・モデルを用いる。

直観主義論理は実際的な有用性を持つ。何故ならばこの制限によって存在具体性を持つ証明が作られるからであり、これは直観主義論理が数学的構成主義のある形態として適当なものとする。非正式には、ある対象が存在することの構成的証明があれば、その構成的証明はそのような対象の例を生成するアルゴリズムとして使える、ということを意味する。

形式化された直観主義論理はアレン・ハイティングによってヤン・ブラウワーの直観主義プログラムの形式的な基礎として発展せられたものである。
構文論と証明体系Rieger?Nishimura束のハッセ図。これのノードは変数をひとつだけ持つ命題論理式の直観主義的な同値性による同値類で、その順序は直観主義的な含意から誘導されるものである。

直観主義論理の論理式の構文は古典命題論理や古典述語論理と類似である。しかしながら、直観主義的な論理結合子は、古典論理におけるように、他の論理結合子を用いて定義することはできない。（そのため { → , ⊥ } {\displaystyle \{\to ,\bot \}} , { ∧ , ¬ } {\displaystyle \{\wedge ,\neg \}} , { ∨ , ¬ } {\displaystyle \{\vee ,\neg \}} などの論理結合子だけを用いて定式化することはできない。）直観主義命題論理では習慣的に → , ∧ , ∨ , ⊥ {\displaystyle \to ,\wedge ,\vee ,\bot } を基本的な結合子として採用する。ここで ¬ A {\displaystyle \neg A} は A → ⊥ {\displaystyle A\to \bot } の省略形として扱う。直観主義述語論理ではこれに量化記号 ∃ , ∀ {\displaystyle \exists ,\forall } を加える。

多くの古典論理の恒真式は直観主義的には証明できない。排中律 p ∨ ¬ p {\displaystyle p\vee \neg p} だけでなくパースの法則 ( ( p → q ) → p ) → p {\displaystyle ((p\to q)\to p)\to p} や二重否定除去 ¬ ¬ p → p {\displaystyle \neg \neg p\to p} などがその例である。古典論理において二重否定導入 p → ¬ ¬ p {\displaystyle p\to \neg \neg p} と二重否定除去 はともに定理である。直観主義論理においては前者のみが定理である。すなわち二重否定を導入することはできるが、除去することはできない。ただし三重否定除去 ¬ ¬ ¬ p → ¬ p {\displaystyle \neg \neg \neg p\to \neg p} は定理である。排中律 p ∨ ¬ p {\displaystyle p\vee \neg p} の拒絶は古典論理に親しい者には奇妙に思われるが、直観主義論理で命題論理式を証明するには、全ての可能な命題論理式に対して真または偽の証明が要求され、これは様々な理由によって不可能である。

多くの古典論理で妥当な恒真式は直観主義論理では定理でないが、全ての直観主義論理で妥当な定理は古典論理に於いても妥当であるから、直観主義論理は古典論理を弱めたものであるという見方ができる。ただし直観主義論理は古典論理にはない良い性質を多く持っている。
シークエント計算詳細は「シークエント計算」を参照

ゲンツェンは彼の体系LK（古典論理のシークエント計算）の簡単な制限として直観主義論理の健全かつ完全な体系が得られることを見つけた。彼はこの体系をLJと呼んだ。LKにおいて任意個の論理式がシークエントの結論（右側）に来ることを許すが、LJにおいては高々ひとつの論理式だけを許す。この結果として例えば含意右の適用において直観主義的に許容できない推論が禁じられることから、直観主義論理の体系が得られるのである。（右辺が複数であることを許すと含意右を用いて α→α,⊥ から →α,¬α が得られ、排中律が導かれる。右辺を制限した結果として含意右が制限されて直観主義論理の体系が得られる。）

LKを制限して得られる直観主義論理の体系で結論が複数であることを許容するものもある。LJ'[1]はその例である。
ヒルベルト流の計算

直観主義論理は次のようにヒルベルト流の計算を用いても定義できる。これは古典命題論理の公理化（Propositional calculus#Alternative calculus）に類似である。

命題論理では、推論規則としてモーダスポネンス

MP: ϕ {\displaystyle \phi } および ϕ → ψ {\displaystyle \phi \to \psi } から ψ {\displaystyle \psi } を導く

を取り、公理図式として次のものを取る：

THEN-1: ϕ → ( χ → ϕ ) {\displaystyle \phi \to (\chi \to \phi )}

THEN-2: ( ϕ → ( χ → ψ ) ) → ( ( ϕ → χ ) → ( ϕ → ψ ) ) {\displaystyle (\phi \to (\chi \to \psi ))\to ((\phi \to \chi )\to (\phi \to \psi ))}

AND-1: ϕ ∧ χ → ϕ {\displaystyle \phi \land \chi \to \phi }

AND-2: ϕ ∧ χ → χ {\displaystyle \phi \land \chi \to \chi }

AND-3: ϕ → ( χ → ( ϕ ∧ χ ) ) {\displaystyle \phi \to (\chi \to (\phi \land \chi ))}

OR-1: ϕ → ϕ ∨ χ {\displaystyle \phi \to \phi \lor \chi }

OR-2: χ → ϕ ∨ χ {\displaystyle \chi \to \phi \lor \chi }

OR-3: ( ϕ → ψ ) → ( ( χ → ψ ) → ( ϕ ∨ χ → ψ ) ) {\displaystyle (\phi \to \psi )\to ((\chi \to \psi )\to (\phi \lor \chi \to \psi ))}

FALSE: ⊥ → ϕ {\displaystyle \bot \to \phi }

一階述語論理の体系を作るには次の推論規則を加える：

∀ {\displaystyle \forall } -GEN: ψ → ϕ {\displaystyle \psi \to \phi } から ψ → ( ∀ x   ϕ ) {\displaystyle \psi \to (\forall x\ \phi )} を導く；ただし固有変数条件「 x {\displaystyle x} は ψ {\displaystyle \psi } に自由に現れない」を満たす

∃ {\displaystyle \exists } -GEN: ϕ → ψ {\displaystyle \phi \to \psi } から ( ∃ x   ϕ ) → ψ {\displaystyle (\exists x\ \phi )\to \psi } を導く；ただし固有変数条件「 x {\displaystyle x} は ψ {\displaystyle \psi } に自由に現れない」を満たす

また次のものを公理図式に加える：

PRED-1: ( ∀ x   ϕ ( x ) ) → ϕ ( t ) {\displaystyle (\forall x\ \phi (x))\to \phi (t)} ただし項 t は ϕ {\displaystyle \phi } の中の x への代入について自由である (つまり t の中の変数記号は ϕ ( t ) {\displaystyle \phi (t)} の中で束縛されていない)

PRED-2: ϕ ( t ) → ( ∃ x   ϕ ( x ) ) {\displaystyle \phi (t)\to (\exists x\ \phi (x))} ただしPRED-1と同様の条件を満たす

オプションの結合子
否定

もし否定を表す結合子 ¬ {\displaystyle \lnot } を ϕ → ⊥ {\displaystyle \phi \to \bot } なる省略形の代わりに導入したいならば、次を公理に加えれば十分である：

NOT-1': ( ϕ → ⊥ ) → ¬ ϕ {\displaystyle (\phi \to \bot )\to \lnot \phi }

NOT-2': ¬ ϕ → ( ϕ → ⊥ ) {\displaystyle \lnot \phi \to (\phi \to \bot )}

否定を導入した代わりに偽を表す命題定数 ⊥ {\displaystyle \bot } を落としたいならば次のようにする。まず FALSE, NOT-1', NOT-2' を次の公理に置き換える：

NOT-1: ( ϕ → χ ) → ( ( ϕ → ¬ χ ) → ¬ ϕ ) {\displaystyle (\phi \to \chi )\to ((\phi \to \lnot \chi )\to \lnot \phi )}