---
tag: Q11N8X99FK
kind: concept
name: Intuitionistic logic
msc: [03B20, 03F55]
sources:
  - url: https://en.wikipedia.org/wiki/Intuitionistic_logic
same_as:
  wikidata: Q176786
  wikipedia: Intuitionistic logic
---

## Summary

Intuitionistic logic is the logic of constructive reasoning, in which a statement counts as true only when it has a proof.
It is classical logic without the [[law of excluded middle|0RYYK8PG4S]] $\varphi \lor \neg\varphi$ and without double negation elimination $\neg\neg\varphi \to \varphi$.
Its semantics include [[Heyting algebras|NG943XNQWH]], [[Kripke models|NGHWZ9Y7ZV]] and the [[Brouwer–Heyting–Kolmogorov interpretation|7B53ZGXXEQ]].
Through the [[Curry–Howard correspondence|A77FER1Q5H]], its proofs correspond to typed programs.

## Explanations

### L1 human

In intuitionistic logic, to prove "$A$ or $B$" you must prove $A$ or prove $B$, and to prove "there exists $x$" you must exhibit one.
So "$A$ or not $A$" is not a law, because you may have a proof of neither.
For example, a classical proof that some pair of irrational numbers $a, b$ has $a^b$ rational, without telling which pair, is not an intuitionistic proof.
Everything provable intuitionistically is provable classically, but not conversely.