The strength of some Martin-Löf type theories
type: Item
instance of: scholarly article
title: The strength of some Martin-Löf type theories
zbMATH Open document ID: 0819.03047
DOI: 10.1007/BF01278464
author: Edward R. Griffor
author: Michael Rathjen
published in: Archive for Mathematical Logic
publication date: 1995-08-27T00:00:00Z
review text: The main result of this paper shows that the classical second-order arithmetic of \(\Delta^ 1_ 2- \text{CA}+ \text{BI}\) (bar induction) is reducible to \(\text{ML}_ 1 \text{W}\), Martin-Löf's type theory with one universe and the type of well-founded trees. The method used is, in the authors' parlance, a ``soft'' proof theory, like the interpretation of one theory into another, and no (hard) ordinal analysis is employed. The paper has the character of a survey, and many constructive theories are discussed, compared, and interpreted, on the way to achieving the above result. They include KP (Kripke-Platek set theory), CZF (constructive ZF of Aczel), \(\text{T}_ 0\) (of Feferman), and IARI (intuitionistic second order arithmetic). KP, CZF, \(\text{ML}_ 1 \text{V}\) (here, V is Aczel's set of iterative sets) and ten or so other theories are shown to be mutually interpretable. A second group contains \(\text{T}_ 0\), \(\Delta^ 1_ 2- \text{CA}+ \text{BI}\), KPi (i for inaccessible ordinal) and \(\text{ML}_{1 \text{W}} \text{V}\) (the subscript W indicates W-formation for small types). In the `Conclusions', the authors announce that they will consider intuitionistic transfinite types in the future.
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 722179
zbMATH Keywords: constructive systems
zbMATH Keywords: Kripke-Platek set theory
zbMATH Keywords: constructive ZF
zbMATH Keywords: intuitionistic second order arithmetic
zbMATH Keywords: classical second-order arithmetic
zbMATH Keywords: Martin-Löf's type theory
MaRDI profile type: Publication
cites work: Q3937387
cites work: Q3310616
cites work: Q3762311
cites work: Q4075450
cites work: Recursive models for constructive set theories
cites work: Q3679172
cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
cites work: Q4128540
cites work: Q3882452
cites work: Zur Beweistheorie Der Kripke-Platek-Mengenlehre Über Den Natürlichen Zahlen
cites work: A well-ordering proof for Feferman's theoryT 0
cites work: Q3041187
cites work: Q3688389
cites work: Constructive set theory
cites work: Q3999860
cites work: Type-theoretic interpretation of iterated, strictly positive inductive definitions
cites work: Proof-theoretic analysis of KPM
cites work: Q4715478
cites work: Constructivism in mathematics. An introduction. Volume II
description: scientific article; zbMATH DE number 722179