Book chapter 1172 views 159 downloads
Proof theory and Martin-Löf Type Theory
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 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
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 |