Realizability and Generalized Forcing in Set Theory

Jean-Louis Krivine

The well known Curry-Howard correspondence between proofs and programs was originally discovered for a very restricted logic : the system of simple types, which uses the intuitionistic propositional calculus, with the only connective →. It was extended to second order intuitionistic logic, in 1970, by J.-Y. Girard, under the name of system F. The relation with programming languages was made by J. Reynolds.

In 1990, this correspondence was extended to classical logic, following Felleisen and Griffin who found that the law of Peirce corresponds to control instructions in functional programming languages. Since then, several type systems have been given, which extend the Curry-Howard correspondence to second order classical logic. It was left the problem of extending this correspondence to the whole of classical Zermelo-Frænkel set theory, and this is the subject of the present talk.

In order to do this, we inductively build realizability models, like in the well known construction of forcing. We show that each axiom of ZF (except the axiom of choice) is then realized ; we obtain in this way a type system in which set-theoretic proofs are formalizable and give rise to programs, which are terms of the λ-calculus extended with control instructions. In this system, the normalization property is “ essentially true ” in the sense that we get correct computations on data types. Of course, not every typable term is normalizable since, for example, the fixed point operator Y has the type of the foundation axiom.

This construction is indeed a generalization of forcing, the realizability models being the analog of Boolean valued models in usual forcing. Since we work in classical logic, it is now easy to turn them into ordinary models of ZF. Models obtained in this way are rather fascinating objects, which differ deeply from forcing models and pose several interesting problems. First of all, they always have non standard integers (except in a “ degenerate case ”, which is usual forcing), and therefore, they are not end extensions of the original model of ZFC. Although I did not yet prove this, it is very likely that they never satisfy the axiom of choice.

J.-L. Krivine. Typed lambda-calculus in classical Zermelo-Frænkel set theory. To appear in Archiv for Math. Logic.

Preprint at www.logique.jussieu.fr/www.krivine.

Address: UFR de Mathématiques, Université Paris VII, 2 Pl. Jussieu, 75251 Paris Cedex 05, France

E-mail: krivine@logique.jussieu.fr