Navigation – Plan du site

AccueilNuméros165Proof Theory of Martin-Löf Type T...

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

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 06 février 2025. URL : http://journals.openedition.org/msh/2959 ; DOI : https://doi.org/10.4000/msh.2959

Haut de page

Droits 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
Search OpenEdition Search

You will be redirected to OpenEdition Search