PROOF THEORY OF MARTIN-LOF TYPE THEORY. AN OVERVIEW 168;….pdfVIP

Math. Sci. hum. / Mathematical Social Sciences (42e ann´ee, n◦ 165, 2004, p. 59–99) 1 ¨ PROOF THEORY OF MARTIN-LOF TYPE THEORY. AN OVERVIEW Anton SETZER 2 summary – 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 W-type and one microscopic universe containing only two finite sets in carried out. Then we look at the analysis Martin-L¨of theory with W-type and a universe closed under the W-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, W-type, Well- founded trees, Kleene’s O, Mahlo universe, Inductive-recursive definitions, Generic programming ´ ´ resume – La th´eorie de la preuve de la th´eorie des types de Martin-L¨o. Une vue d’ensemble Nous donnons une vue d’ensemble du d´eveloppement historique de la th´eorie de la preuve et des principales techniques utilis´ees dans la th´eorie ordinale de la preuve. Nous soutenons que, dans une forme