La réalisabilité classique permet d'interpréter des théories mathématiques classiques, comme la théorie des ensembles ZF, dans divers modèles de calcul (lambda-calcul avec continuations, domaines…) axiomatisés au moyen d'algèbres de réalisabilité. Elle produit ainsi des modèles de ces théories, de même qu'une technique bien connue, le forcing de Cohen, dont elle est en fait une généralisation.

Jusqu'ici, la réalisabilité classique a seulement été étudiée à partir d'un modèle de départ “raisonnable”, supposé au moins valider AC, voire même défini comme l'univers constructible. Dans cet exposé, on étudiera un analogue des “conditions d'antichaîne” du forcing nous permettant d'exporter certaines propriétés du modèle de départ au modèle de réalisabilité; et on l'appliquera pour obtenir des programmes réalisant Non DC (resp. Non CH) à partir de modèles de ZF bien choisis validant Non DC (resp. Non CH).

— DC: axiome du choix dépendant CH: hypothèse du continu