Navigation – Plan du site

Proof Theory of Martin-Löf Type Theory. An overview

La théorie de la preuve de la théorie des types de Marin-Löf
Anton Setzer

Résumés

We give an overview over the historic development of proof theory and the main techniques used in ordinal theoretic proof theory. We argue, that in a revised Hilbert’s program, ordinal theoretic proof theory has to be supplemented by a second step, namely the development of strong equiconsistent constructive theories. Then we show, how, as part of such a programe, the proof theoretic analysis of Martin-Löf type theory with W-type and one microscopic universe containing only two finite sets is carried out. Then we look at the analysis Martin-Löf type theory with W-type and a universe closed under the W-type, and consider the extension of type theory by one Mahlo universe and its proof-theoretic analysis. Finally, we repeat the concept of inductive-recursive definitions, which extends the notion of inductive definitions substantially. We introduce a closed formalization, which can be used in generic programming, and explain, what is known about its strength.

La théorie de la preuve de la théorie des types de Marin-Löf

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.

Haut de page

Pour 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 19 novembre 2017. URL : http://msh.revues.org/2959

Haut de page

Droits d’auteur

© École des hautes études en sciences sociales

Haut de page