Proof Theory of Martin-Löf Type Theory. An overview
Résumés
Nous donnons une vue d’ensemble du développement historique de la théorie de la preuve et des principales techniques utilisées dans la théorie ordinale de la preuve. Nous soutenons que, dans une forme révisée du programme d’Hilbert, la théorie ordinale de la preuve doit être complétée par une seconde étape, à savoir le développement de théories constructives fortes et équiconsistantes. Comme partie d’un tel programme, nous présentons ensuite l’analyse, en théorie de la preuve, de la théorie des types de Martin-Löf avec un univers microscopique ne contenant que deux types finis. Nous examinons ensuite l’analyse de la théorie des types de Martin-Löf avec type W et un univers clos pour ce type, puis nous étendons la théorie des types par un univers de Mahlo et considérons son analyse en théorie de la preuve. Enfin, nous présentons le concept de définition inductive-récursive, qui étend de façon substantielle la notion de définition inductive. Nous introduisons une formalisation close, qui peut être employée en programmation générique, et expliquons ce que nous savons de sa force ordinale.
Entrées d’index
Mots-clés :
arbres bien fondés, définition inductive-récursive, ordinaux de Kleene, programmation générique, théorie des ensembles, théorie des ensembles de Kripke Platek, théorie des types de Martin-Löf, univers de MahloKeywords:
generic programming, inductive-recursive definitions, Kleene's O, Kripke Platek set theory, Mahlo universe, Martin-Löf type theory, set theory, well-founded treesPour citer cet article
Référence électronique
Anton Setzer, « Proof Theory of Martin-Löf Type Theory. An overview », Mathématiques et sciences humaines [En ligne], 165 | Printemps 2004, mis en ligne le 22 février 2006, consulté le 06 février 2025. URL : http://journals.openedition.org/msh/2959 ; DOI : https://doi.org/10.4000/msh.2959
Haut de pageDroits d’auteur
Le texte et les autres éléments (illustrations, fichiers annexes importés), sont « Tous droits réservés », sauf mention contraire.
Haut de page