×

Realizability. (English) Zbl 0911.03031

Buss, Samuel R. (ed.), Handbook of proof theory. Amsterdam: Elsevier. Stud. Logic Found. Math. 137, 407-473 (1998).
The essay under review presents a remarkably clear and updated survey of the (family of) methods that can be unified under the heading of ‘realizability interpretation’, and have nowadays become a powerful and flexible tool in the investigation of constructive theories.
To give an idea of its content, here is the list of the sections that constitute the skeleton of this work: 1. numerical realizability; 2. abstract realizability and function realizability; 3. modified realizability; 4. derivation of the Fan rule; 5. Lifschitz realizability; 6. extensional realizability; 7. realizability for intuitionistic second order arithmetic; 8. realizability for higher order logic and arithmetic; 9. a final chapter touching upon more specialized topics (among them, realizability for set theory, comparison with functional interpretation, formulas-as-types, applications to Computer Science).
As a reminder, realizability was originally invented by Kleene in 1945 as a technique for modeling the meaning of intuitionistic arithmetical statements, and it is inspired by (a non-standard reading of) the so-called Brouwer-Heyting-Kolmogorov interpretation. Roughly, it associates to each given statement \(A\) an object (the so-called realizer) encoding the constructive content of \(A\); typically, if \(A\) is existential, the realizer produces a witness for \(A\), while, if \(A\) is an implication \(B \rightarrow C\), it yields a method \(f\) which applies to any given proof \(p\) of \(B\), in order to produce a proof \(f(p)\) of \(C\). Hence realizability presupposes that the set of realizers is an applicative structure, since it must be possible to deal with operations, and application of an operation to a given argument; indeed, Kleene’s idea is just to interpret these notions into the applicative structure (actually a partial combinatory algebra) of indices of partial recursive functions, and hence to use numbers as realizers.
The present essay shows that the realizability techniques have been greatly generalized since 1945: it emerges that realizers have become more abstract mathematical objects, which live in per se interesting mathematical structures (e.g. the space of number-theoretic functions with continuous application, functionals of higher type, combinatory algebras, suitable sets in a topological space; see also the connections with categorical logic in section 8).
The typical results discussed in the paper are essentially proof-theoretic, e.g. consistency and inconsistency under addition of principles and rules (like extended Church thesis, suitable forms of choice, continuity, uniformity), partial conservation theorems. An elegant feature of the presentation of formal (numerical) realizability is that it is carried out in an ‘applicative’ conservative extension of Heyting Arithmetic with a partial application symbol as primitive (so terms are not always defined and the official logic of the system is the logic of partial terms). Section 4 offers a smooth derivation of the Fan Rule for \(\text{HA}^\omega\), which combines modified realizability with Howard majorizable functionals.
Of course, due the limited space, many proofs are only outlined; but full references are always supplied. In fact, the paper contains an extensive reference list of more than two hundred items, covering contributions from 1945 to 1996, and the text is interspersed with many technical and historical remarks, which render the paper a rich source for constructivism in the last fifty years.
In a nutshell, the paper is a welcome complement to the author’s “Realizability and functional interpretations” [in: A. S. Troelstra (ed.), Metamathematical investigation of intuitionistic arithmetic and analysis, Lect. Notes Math. 344, 175-187 (1973; Zbl 0275.02025)] and to her joint work with D. van Dalen [Constructivism in mathematics. An introduction. Vols. I, II (1988; Zbl 0653.03040 and Zbl 0661.03047)].
For the entire collection see [Zbl 0898.03001].

MSC:

03F50 Metamathematics of constructive systems
03F55 Intuitionistic mathematics
03F65 Other constructive mathematics
03F30 First-order arithmetic and fragments
03F35 Second- and higher-order arithmetic and fragments
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
PDFBibTeX XMLCite