Apparaît dans la collection : 2014 - T2 - Semantics of proofs and certified mathematics

Classical realizability appeared as a method to extend the proof-program correspondence to the whole of ZF set theory, even with DC (dependent choice). As a by-product, it gives completely new models of ZF + DC, that we shall consider in these talks. The method of forcing is indeed a (very) particular case, that we shall avoid, of course. The principal tools are :i) A conservative extension of ZF, called ZF_epsilon, with a new strong membership relation, which does not satisfy extensionality. ii) The structure of realizability algebra, which is a three-sorted extension of the well known combinatory algebra of Curry. The ordered sets of conditions, used in forcing, are degenerate cases of realizability algebras. he usual models of lambda-calculus (stable spaces, hypercoherence spaces, . . . ) are examples of realizability algebras. The models of ZF obtained in this way are much more difficult to study than the ordinary forcing models: they are not extensions of the ground model, ordinals and even integers are not preserved and neither is the axiom of choice. I shall explain what we already know about their structure. We shall look at some examples, which give some new relative consistency results, with DC and R not well ordered. Up to now, there are few such new results, even though the method is much more general than forcing. The reason is, of course, that we do not yet understand sufficiently well the structure of these models.