No Cover Image

Book chapter 1232 views 190 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
first_indexed 2013-07-23T11:46:34Z
last_indexed 2018-02-09T04:26:57Z
id cronfa12
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2015-05-17T17:33:21.9529114</datestamp><bib-version>v2</bib-version><id>12</id><entry>2011-10-01</entry><title>Proof theory and Martin-L&#xF6;f Type Theory</title><swanseaauthors><author><sid>5f7695285397f46d121207120247c2ae</sid><ORCID>0000-0001-5322-6060</ORCID><firstname>Anton</firstname><surname>Setzer</surname><name>Anton Setzer</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2011-10-01</date><deptcode>MACS</deptcode><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.</abstract><type>Book chapter</type><journal>One Hundred Years of Intuitionism (1907&#x2013;2007)</journal><volume></volume><journalNumber></journalNumber><paginationStart>257</paginationStart><paginationEnd>279</paginationEnd><publisher>Birkh&#xE4;user</publisher><placeOfPublication/><issnPrint/><issnElectronic/><keywords/><publishedDay>9</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2008</publishedYear><publishedDate>2008-11-09</publishedDate><doi>10.1007/978-3-7643-8653-5_16</doi><url>http://www.springerlink.com/content/lw112klq80w11636/</url><notes>In One hundred years of intuitionism (1907 -- 2007) (ed. Atten, M. v.; Boldini, P.; Bourdeau, M.; Heinzmann, G.)</notes><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2015-05-17T17:33:21.9529114</lastEdited><Created>2011-10-01T00:00:00.0000000</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>1</order></author></authors><documents><document><filename>0009213-18052015010232.pdf</filename><originalFilename>setzerProofTheoryAndMartinLoefTypeTheory.pdf</originalFilename><uploaded>2015-05-17T17:33:12.8730000</uploaded><type>Output</type><contentLength>264302</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2015-05-17T17:33:12.0000000</embargoDate><documentNotes/><copyrightCorrect>false</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling 2015-05-17T17:33:21.9529114 v2 12 2011-10-01 Proof theory and Martin-Löf Type Theory 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2011-10-01 MACS 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. Book chapter One Hundred Years of Intuitionism (1907–2007) 257 279 Birkhäuser 9 11 2008 2008-11-09 10.1007/978-3-7643-8653-5_16 http://www.springerlink.com/content/lw112klq80w11636/ In One hundred years of intuitionism (1907 -- 2007) (ed. Atten, M. v.; Boldini, P.; Bourdeau, M.; Heinzmann, G.) COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2015-05-17T17:33:21.9529114 2011-10-01T00:00:00.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Anton Setzer 0000-0001-5322-6060 1 0009213-18052015010232.pdf setzerProofTheoryAndMartinLoefTypeTheory.pdf 2015-05-17T17:33:12.8730000 Output 264302 application/pdf Accepted Manuscript true 2015-05-17T17:33:12.0000000 false
title Proof theory and Martin-Löf Type Theory
spellingShingle Proof theory and Martin-Löf Type Theory
Anton Setzer
title_short Proof theory and Martin-Löf Type Theory
title_full Proof theory and Martin-Löf Type Theory
title_fullStr Proof theory and Martin-Löf Type Theory
title_full_unstemmed Proof theory and Martin-Löf Type Theory
title_sort Proof theory and Martin-Löf Type Theory
author_id_str_mv 5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 5f7695285397f46d121207120247c2ae_***_Anton Setzer
author Anton Setzer
author2 Anton Setzer
format Book chapter
container_title One Hundred Years of Intuitionism (1907–2007)
container_start_page 257
publishDate 2008
institution Swansea University
doi_str_mv 10.1007/978-3-7643-8653-5_16
publisher Birkhäuser
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://www.springerlink.com/content/lw112klq80w11636/
document_store_str 1
active_str 0
description 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.
published_date 2008-11-09T06:02:06Z
_version_ 1821384194450784256
score 11.047501

Similar Items