Fwd: [TYPES] Article on proof theory of type theory

----- Forwarded message from Anton Setzer <a.g.setzer-QvkbJbr/[email protected]> -----
    Date: Sun, 29 Feb 2004 17:10:10 +0000
    From: Anton Setzer <a.g.setzer-QvkbJbr/[email protected]>
Reply-To: Anton Setzer <a.g.setzer-QvkbJbr/[email protected]>
 Subject: [TYPES] Article on proof theory of type theory
      To: [email protected]

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Dear all,

I have written an overview article over type theory of Martin-L"of
type theory. It is intended for the reader who doesn't know
much about proof theory but has some knowledge about type theory.
I hope it is easy to read.

It is available via
http://www.cs.swan.ac.uk/~csetzer/articles/overviewProofTheoryTypeTheory2004.pdf
(Versions in .dvi, .ps, .bib format are as well available by
exchanging .pdf by these extensions)

Related articles are available from my homepage,
http://www.cs.swan.ac.uk/~csetzer


Anton Setzer


Abstract
~~~~~~~~

We give an overview over the historic development of proof theory and
the main techniques used in ordinal theoretic proof theory. We 
argue, that in a revised Hilbert's programme,
ordinal theoretic proof theory has to be supplemented
by a second step, namely the development of strong
equiconsistent constructive theories.  Then we show,
how, as part of such a programme, the proof theoretic 
analysis of Martin-L"of type theory with 
$\Wrm$-type and one microscopic universe containing
only two finite sets is carried out.
Then we look at the analysis
of Martin-L"of type theory
with $\Wrm$-type and a universe closed under the 
$\Wrm$-type, and consider the extension
of type theory by one Mahlo universe  and its proof-theoretic analysis. 
Finally we repeat the concept of 
inductive-recursive definitions, which extends the notion
of inductive definitions substantially. We introduce 
a closed formalisation, which can be 
used in generic programming, and explain, what is known about
its strength.

Keywords: Martin-L"of type theory, proof theory, Kripke-Platek set theory,
$\Wrm$-type, well-founded trees, Kleene's O, Mahlo universe, inductive-recursive
definitions, generic programming. 


-----------------------------------------------------------------------------
Anton Setzer                            Telephone:
Department of Computer Science          (national)        (01792) 513368 
University of Wales Swansea             (international) +44 1792  513368
Singleton Park                          Fax:
Swansea SA2 8PP                         (national)        (01792) 295708
UK                                      (international) +44 1792  295708
                                        
Visiting address:                       Email: [email protected]
Faraday Building,                       WWW:
Computer Science Dept.                 http://www.cs.swan.ac.uk/~csetzer/ 
2nd floor, room 211.                                                          
------------------------------------------------------------------------------
 
                    
  

----- End forwarded message -----