Jean-Louis Krivine
PPS, Université Paris-Diderot
https://www.irif.fr/~krivine/
Date(s) : 26/03/2015 iCal
11 h 00 min - 12 h 30 min
L’opérateur de bar recursion, introduit dans les années 60 par C. Spector pour “prouver” la consistance de l’Analyse, a été recyclé à partir de 1998, par Berardi, Bezem, Coquand, Berger, Oliva, Kohlenbach, … pour obtenir des programmes à l’aide de l’axiome du choix dépendant (DC).
Une autre méthode pour ce faire est, en réalisabilité classique, d’utiliser une instruction “quote”. La question se posait, du rapport entre ces deux méthodes. En fait, on verra que l’opérateur de “bar recursion” ne fonctionne que dans les modèles de sémantique dénotationnelle, où “quote” n’a aucun sens. On verra aussi que, dans ces modèles, cet opérateur fournit des programmes pour l’axiome du bon ordre sur R, et pour toutes les formules “vraies” d’Analyse.
http://www.pps.univ-paris-diderot.fr/~krivine/
Catégories