Proof Theory of Martin-Löf Type Theory. An overview
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 con...
Sparad:
| I publikationen: | URI:https://journals.openedition.org/msh, |
|---|---|
| Huvudupphovsman: | |
| Materialtyp: | Article ou chapitre numérique |
| Språk: | Anglais |
| Publicerad: |
Mathématiques et sciences humaines
2006
|
| Ämnen: | |
| Länkar: | Accès Université d'Orléans et IFPM Accès Université d'Orléans et IFPM |
| Sammanfattning: | 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. |
|---|