No Cover Image

Book Chapter 352 views 35 downloads

Proof theory and Martin-Löf Type Theory / Anton Setzer

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

Swansea University Author: Setzer, Anton

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!
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:21Z</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><alternativeTitle></alternativeTitle><author>Anton Setzer</author><firstname>Anton</firstname><surname>Setzer</surname><active>true</active><ORCID>0000-0001-5322-6060</ORCID><ethesisStudent>false</ethesisStudent><sid>5f7695285397f46d121207120247c2ae</sid><email>61db1ab5eaeff34062db71cc1973df39</email><emailaddr>QBY4tVYqSovxQSx/NwDRpMjwe531u+mO/3IG3xe5jMg=</emailaddr><date>2011-10-01</date><deptcode>SCS</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>Chapter in book</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></placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint></issnPrint><issnElectronic></issnElectronic><keywords></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 of Science</college><department>Computer Science</department><CollegeCode>CSCI</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution/><researchGroup>Theoretical Computer Science</researchGroup><supervisor></supervisor><sponsorsfunders/><grantnumber/><degreelevel/><degreename></degreename><lastEdited>2015-05-17T17:33:21Z</lastEdited><Created>2011-10-01T00:00:00Z</Created><path><level id="1">College of Science</level><level id="2">Computer Science</level></path><authors><author><firstname>Anton</firstname><surname>Setzer</surname><orcid/><order>1</order></author></authors><documents><document><filename>0000012-17052015173312.pdf</filename><originalFilename>setzerProofTheoryAndMartinLoefTypeTheory.pdf</originalFilename><uploaded>2015-05-17T17:33:12Z</uploaded><type>Output</type><contentLength>264302</contentLength><contentType>application/pdf</contentType><version>AM</version><cronfaStatus>true</cronfaStatus><action>Published to Cronfa</action><actionDate>17/05/2015</actionDate><embargoDate>2015-05-17T17:33:12</embargoDate><documentNotes></documentNotes><copyrightCorrect>false</copyrightCorrect><language/></document></documents></rfc1807>
spelling 2015-05-17T17:33:21Z v2 12 2011-10-01 Proof theory and Martin-Löf Type Theory Anton Setzer Anton Setzer true 0000-0001-5322-6060 false 5f7695285397f46d121207120247c2ae 61db1ab5eaeff34062db71cc1973df39 QBY4tVYqSovxQSx/NwDRpMjwe531u+mO/3IG3xe5jMg= 2011-10-01 SCS 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. Chapter in book 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 of Science Computer Science CSCI SCS Theoretical Computer Science 2015-05-17T17:33:21Z 2011-10-01T00:00:00Z College of Science Computer Science Anton Setzer 1 0000012-17052015173312.pdf setzerProofTheoryAndMartinLoefTypeTheory.pdf 2015-05-17T17:33:12Z Output 264302 application/pdf AM true Published to Cronfa 17/05/2015 2015-05-17T17:33:12 false
title Proof theory and Martin-Löf Type Theory
spellingShingle Proof theory and Martin-Löf Type Theory
Setzer, Anton
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_***_Setzer, Anton
author Setzer, Anton
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 College of Science
hierarchytype
hierarchy_top_id collegeofscience
hierarchy_top_title College of Science
hierarchy_parent_id collegeofscience
hierarchy_parent_title College of Science
department_str Computer Science{{{_:::_}}}College of Science{{{_:::_}}}Computer Science
url http://www.springerlink.com/content/lw112klq80w11636/
document_store_str 1
active_str 1
researchgroup_str Theoretical Computer Science
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-09T03:52:32Z
_version_ 1645251764798095360
score 10.847605