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