basic constructions:
strong axioms
further
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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 $\underset{x\in X}{\exists} \phi(x)$ consists of constructing a specific $x \in X$ and a proof of $\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 computability | type II computability | |
---|---|---|
typical domain | natural numbers $\mathbb{N}$ | Baire space of infinite sequences $\mathbb{B} = \mathbb{N}^{\mathbb{N}}$ |
computable functions | partial recursive function | computable function (analysis) |
type of computable mathematics | recursive mathematics | computable analysis, Type Two Theory of Effectivity |
type of realizability | number realizability | function realizability |
partial combinatory algebra | Kleene's first partial combinatory algebra | Kleene'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
Symposium (A. S. Toelstra and D. van Dalen, eds.), North-Holland Publishing Company, 1982, pp. 165–216
A modern textbook account is
Lecture notes include
and
based on
Andrej Bauer, The Realizability Approach to
Computable Analysis and Topology_, PhD thesis CMU (2000) (pdf)
Peter Lietz, From Constructive Mathematics to Computable Analysis via the Realizability Interpretation (pdf.gz)
See also
Steven Awodey, Andrej Bauer, Sheaf toposes for realizability (pdf)
Wouter Pieter Stekelenburg, Realizability Categories, PhD thesis, Utrecht 2013 (arXiv:1301.2134)
Martin Hyland, Variations on realizability: realizing the propositional axiom of choice, Mathematical Structures in Computer Science, Volume 12, Issue 3, June 2002, pp. 295 - 317 (doi:10.1017/S0960129502003651, pdf)
Last revised on December 10, 2020 at 10:41:05. See the history of this page for a list of all contributions to it.