Book chapter 1637 views 337 downloads
Proof theory and Martin-Löf Type Theory
Anton Setzer 
One Hundred Years of Intuitionism (1907–2007), Pages: 257 - 279
Swansea University Author:
Anton Setzer
-
PDF | Accepted Manuscript
Download (292.28KB)
DOI (Published version): 10.1007/978-3-7643-8653-5_16
Abstract
In this article an overview over the work of the author on developing proof theoretic strong extensions of Martin-Loef Type Theory including precise proof theoretic bounds is given. It presents the first publication of the proof theoretically strongest known extensions of Martin-Loef Type Theory, na...
| Published in: | One Hundred Years of Intuitionism (1907–2007) |
|---|---|
| Published: |
Birkhäuser
2008
|
| Online Access: |
http://www.springerlink.com/content/lw112klq80w11636/ |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa12 |
| Abstract: |
In this article an overview over the work of the author on developing proof theoretic strong extensions of Martin-Loef Type Theory including precise proof theoretic bounds is given. It presents the first publication of the proof theoretically strongest known extensions of Martin-Loef Type Theory, namely the hyper-Mahlo Universe, the hyper-alpha-Mahlo universe, the autononomous Mahlo universe and the Pi_3-reflecting universe. This is part of a proof theoretic program in developing proof theoretic as strong as possible constructive theories in order to obtain a constructive underpinning of strong classical theories with a full proof theoretic analysis. |
|---|---|
| Item Description: |
In One hundred years of intuitionism (1907 -- 2007) (ed. Atten, M. v.; Boldini, P.; Bourdeau, M.; Heinzmann, G.) |
| College: |
Faculty of Science and Engineering |
| Start Page: |
257 |
| End Page: |
279 |