Constructivism, Realizability, Computability



The idea of realizability is a way of making the Brouwer-Heyting-Kolmogorov interpretation of constructivism and intuitionistic mathematics precise. It is related to the propositions as types paradigm. For instance, constructively a proof of an existential quantification xXϕ(x)\underset{x\in X}{\exists} \phi(x) consists of constructing a specific xXx \in X and a proof of ϕ(x)\phi(x), which “realizes” the truth of the statement, whence the name (see e.g. Streicher 07, section 1, Vermeeren 09, section 1 for introductions to the rough idea, or Bauer 05, page 12 and def. 4.7 for an actual definition).


type I computabilitytype II computability
typical domainnatural numbers \mathbb{N}Baire space of infinite sequences 𝔹= \mathbb{B} = \mathbb{N}^{\mathbb{N}}
computable functionspartial recursive functioncomputable function (analysis)
type of computable mathematicsrecursive mathematicscomputable analysis, Type Two Theory of Effectivity
type of realizabilitynumber realizabilityfunction realizability
partial combinatory algebraKleene's first partial combinatory algebraKleene's second partial combinatory algebra


Realizability originates with the interpretation of intuitionistic number theory, later developed as Heyting arithmetic, in

A historical survey of realizability (including categorical realizability) is in

A quick survey is in

being a summary of

A modern textbook account is

Lecture notes include


based on

See also