---
tag: 4H35VQ16DC
kind: concept
name: Realizability
msc: ["03F50", "03F55", "03D80"]
uses: [CK8ZQRN183, KZSB5E471K, 7B53ZGXXEQ]
sources:
  - url: https://en.wikipedia.org/wiki/Realizability
same_as:
  wikidata: Q3454417
  wikipedia: Realizability
---

## Summary

Realizability is a way to read intuitionistic statements as statements about programs.
A realizer of a formula is a program, often the code of a [[computable function|KZSB5E471K]], that carries the computational content of a proof of it.
Kleene introduced number realizability for [[Heyting arithmetic|CK8ZQRN183]] in 1945, as a precise form of the [[Brouwer–Heyting–Kolmogorov interpretation|7B53ZGXXEQ]].
Realizability shows that intuitionistic proofs of existence yield algorithms, and it gives models in which classical principles fail.

## Explanations

### L1 human

In constructive mathematics, to prove "for every $n$ there is an $m$" one must in effect give a way to find $m$ from $n$.
Realizability makes "a way to find" precise: it is a program.
A program realizes a statement when it provides all the data the statement asks for.
For example, a program that sends $n$ to $2n$, together with a trivial check that $2n = n + n$, realizes "every number has a double".
Every theorem of Heyting arithmetic has a realizer, so its existence theorems come with algorithms.