04/07/2002:
Jean-Louis Krivine (PPS)
L'axiome du choix dénombrable et l'instruction 'quote'.
Résumé
Il s'agit d'une interprétation de l'axiome du choix dénombrable
(et aussi de l'axiome du choix dépendant qui est logiquement un peu plus
fort) en logique classique du second ordre et dans ZF. Pour cela on ajoute
au lambda-calcul une instruction très similaire au 'quote' de LISP. Noter
qu'une telle instruction est incompatible avec la bêta-réduction, et doit
donc se manier avec précaution.
Preprint à http://www.pps.jussieu.fr/~krivine/articles/quote.pdf