Introduction

Basic Idea#

Invented in 1945 by Kleene, and attempt to make explicit the algorithmic content of constructive proofs. 

From proofs of existential statements \(\exists y R(\vec{x},y)\), one would like to read off a so-called Skolem function \(f\): a function \(f\) such that \(R(\vec{x},f(\vec{x}))\) holds for all \(\vec{x}\). With the assumption of (a mild form of the) axiom of choice, such an \(f\) always exists whenever \(\exists y R(\vec{x},y)\) holds, but in general \(f\) will not be computable:

Why? Suppose that \(P\) is an undecidable property of natural numbers, and \(\exists y(y=0 \wedge P(x))\vee (y=1 \wedge \neg P(x))\), there cannot exist an algorithmic Skolem function \(f:\mathbb{N}\to\{0,1\}\) with \(\forall x (f(x)=0\wedge P(x))\vee(f(x)=1\wedge \neg P(x))\) since otherwise \(f\) would give rise to a ecision procedure for the predicate \(P\).

And we don't even need the parameters \(\vec{x}\). From provability of \(\exists xA(x)\) it doesn't necessarily follow that there is a constant \(c\) for which \(A(c)\) is provable. For example let \(P\) be a decidable predicate of natural numbers such that \(\forall x\neg P(x)\) holds but is not provable, then \(\exists x(\neg P(x) \to \forall y \neg P(y))\) is provable, but for no natural number \(n\) one can prove \(\neg P(n)\to \forall y\neg P(y)\) as it is logically equivalent to the unprovable statement \(\forall y \neg P(y)\).

This is to say that classical proofs of \(\exists x A(x)\) do not always give rise to witnesses, namely objects \(c\) for which \(A(c)\) is provable. Constructive logic restricts the rules and axioms of logic in such a way that

• Whenever \(\exists xA(x)\) is provable then \(A(t)\) is provable for some term \(t\).
• If \(A\vee B\) is provable then \(A\) is provable or \(B\) is provable or both.

Which form part of an informal semantics of constructive logic which has come to be widely known under the name of Brouwer-Heyting-Kolmogorov interpretation:

1. a witness of \(A\wedge B\) is a pair \(\langle p, q\rangle\) such that \(p\) is a witness of \(A\) and \(q\) is a witness of \(B\).
2. a witness of \(A\to B\) is a function \(p\) mapping any witness \(q\) of \(A\) to a witness \(p(q)\) of \(B\).
3. a witness of \(A\vee B\) is a pair \(\langle i,p\rangle\) such that either \(i=0\) and \(p\) is a witness of \(A\) or \(i=1\) and \(p\) is a witness of \(B\).
4. a witness of \(\forall x A(x)\) is a function \(p\) mapping any object \(c\) to a witness \(p(c)\) of \(A(c)\).
5. a witness of \(\exists xA(x)\) is a pair \(\langle c,p\rangle\) such that \(p\) is a witness of \(A(c)\).
6. there is no witness for \(\bot\).

For basic assertions \(A\) it is intentionally left unspecified what are their witnesses. Being a witness of a proposition is a basic notion that cannot be further analyzedbut this also applies to the notion of “truth of a proposition” as employed in the usual informal explanation of classical logic a la Tarski. The meaning explanation a la Tarski is usually called truth value semantics, and the meaning explanation a la Brouwer-Heyting-Kolmogorov may be called a proof semantics as it specifies for every proposition \(A\) what is a proof - or a witness - of \(A\).

The basic idea of realizability is to provide mathematically precise instantiations of the BHK interpretations where the informal notion of witness is replaced by a particular mathematical structure \(\mathcal{A}\) which can be understood as a universal untyped model of computation. Having fixed such an \(\mathcal{A}\) propositions are interpreted as subsetes of \(\mathcal{A}\), namely, a proposition \(A\) is identified with the set of its witnesses in \(\mathcal{A}\).

Overview#

Partial combinatory algebra (pca): Assume that \(\mathcal{A}\) is a non-empty set of “algorithms” together with a partial binary operation \(\cdot\) on \(\mathcal{A}\) where \(a\cdot b\) is thought of as the result of applying algorithm \(a\) to \(b\) (partial since the evaluation may fail to terminate; we do not distinguish between algorithms and data and accordingly everything is thrown into a single set \(\mathcal{A}\)). A conservative choice: take \(\mathbb{N}\) for \(\mathcal{A}\) and define \(n\cdot m\) as Kleene application \(\{n\}(m)\) where \(\{n\}\) denotes the \(n\)-th partial recursive function. We require that the structure \((\mathcal{A},\cdot)\) satisfies the following: for every polynomial \(t[x_1,\ldots,x_n,x]\) there is a polynomial \(\Lambda x.t[x_1,\ldots x_n,x]\) in the variables \(x_1,\ldots,x_n\) such that for all \(a_1,\ldots, a_n, a \in\mathcal{A}\) it holds that

\[(\Lambda x.t[a_1,\ldots,a_n,x])\cdot a = t[a_1,\ldots,a_n,a]\]

whenever \(t[a_1,\ldots,a_n,a]\downarrow\) (whenever \(t[a_1,\ldots,a_n,a]\) is defined). We do not require that definedness of \((\Lambda x.t[a_1,\ldots,a_n,x])\cdot a\) implies the definedness of \(t[a_1,\ldots,a_n,a]\). Such an untyped model of computation is usually called a pca.

Assemblies: given an untyped model \((\mathcal{A},\cdot)\) (a pca), one may build a category \(\textbf{Asm}(\mathcal{A})\) of so-called assemblies over \(\mathcal{A}\) which has got enough structure to interpret most of higher order intuitionistic logic. An assembly over \(\mathcal{A}\) is a pair \(X = (|X|,||\cdot||_X)\) where \(X\) is a set and \(||\cdot||_X:|X|\to\mathcal{P}(\mathcal{A})\) such that \(||x||_X \neq \emptyset\) for all \(x\in|X|\). The nonempty subset \(||x||_X\) is thought of as the set of realizers or codes for the element \(x\in |X|\). We also write \(a\Vdash_X x\) (\(a\) realizes \(x\)) for \(a\in ||x||_X\).

If \(X\) and \(Y\) are assemblies over \(\mathcal{A}\) then a morphism from \(X\) to \(Y\) in \(\textbf{Asm}(\mathcal{A})\) is a set-theoretic function \(f:|X|\to|Y|\) which is realized or tracked by an element \(e\in\mathcal{A}\) meaning that \(\forall x\in|X| \forall a\in||x||_X e\cdot a\downarrow \wedge e\cdot a \in ||f(x)||_Y\). We write \(e\Vdash f\) for “\(f\) is realized by \(e\)”. 

Intuitively the function \(f\) is realizable iff it can be implemented in terms of codes by an algorithm from \(\mathcal{A}\). The set of realizable maps from \(X\) to \(Y\) can itself be organized into an assembly \(Y^X\) with \(|Y^X| = \textbf{Asm}(\mathcal{A})(X,Y)\) and \(||f||_{Y^X} = \{e\in \mathcal{A}|e\Vdash f\}\).

Modest sets: There is a most useful full subcategory of \(\textbf{Asm}(\mathcal{A})\), the category \(\textbf{Mod}(\mathcal{A})\) whose objects are those assemblies \(X\) where \(x=x'\) whenver \(e\in ||x||_X\cap ||x'||_X\). The objects of \(\textbf{Mod}(\mathcal{A})\) are called modest sets over \(\mathcal{A}\). 

The intuition behind this notion is that elements of modest setse are determined uniquely by their realizers.

Results:

1. \(\textbf{Asm}(\mathcal{A})\) has enough structure for interpreting constructive logic and mathematics
2. \(\textbf{Mod}(\mathcal{A})\) is a well-behaved full subcategory of \(\textbf{Asm}(\mathcal{A})\) containing all data types needed for functional computation.