No Cover Image

Book chapter 1219 views 180 downloads

Proof theory and Martin-Löf Type Theory

Anton Setzer Orcid Logo

One Hundred Years of Intuitionism (1907–2007), Pages: 257 - 279

Swansea University Author: Anton Setzer Orcid Logo

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...

Full description

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