Switch to: Citations

References in:

Quotient topologies in constructive set theory and type theory

Hajime Ishihara & Erik Palmgren

Annals of Pure and Applied Logic 141 (1):257-265 (2006)

Add references

You must login to add references.

The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.details One objective of this paper is the determination of the proof-theoretic strength of Martin-Löf's type theory with a universe and the type of well-founded trees. It is shown that this type system comprehends the consistency of a rather strong classical subsystem of second order arithmetic, namely the one with Δ 2 1 comprehension and bar induction. As Martin-Löf intended to formulate a system of constructive (intuitionistic) mathematics that has a sound philosophical basis, this yields a constructive consistency proof of a (...) Download Export citation Bookmark 48 citations
(1 other version)Constructive set theory.John Myhill - 1975 - Journal of Symbolic Logic 40 (3):347-382.details Download Export citation Bookmark 80 citations
The strength of Martin-Löf type theory with a superuniverse. Part I.Michael Rathjen - 2000 - Archive for Mathematical Logic 39 (1):1-39.details Universes of types were introduced into constructive type theory by Martin-Löf [12]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say $\mathcal{C}$ . The universe then “reflects” $\mathcal{C}$ .This is the first part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf. [16, 18, 19]).It is proved that Martin-Löf type theory (...) Download Export citation Bookmark 10 citations
Per Martin-Löf. Intuitionistic type theory. Studies in proof theory. Bibliopolis, Naples1984, ix + 91 pp. [REVIEW]W. A. Howard - 1986 - Journal of Symbolic Logic 51 (4):1075-1076.details Download Export citation Bookmark 96 citations
Inaccessible set axioms may have little consistency strength.L. Crosilla & M. Rathjen - 2002 - Annals of Pure and Applied Logic 115 (1-3):33-70.details The paper investigates inaccessible set axioms and their consistency strength in constructive set theory. In ZFC inaccessible sets are of the form Vκ where κ is a strongly inaccessible cardinal and Vκ denotes the κth level of the von Neumann hierarchy. Inaccessible sets figure prominently in category theory as Grothendieck universes and are related to universes in type theory. The objective of this paper is to show that the consistency strength of inaccessible set axioms heavily depend on the context in (...) Download Export citation Bookmark 8 citations
The Type Theoretic Interpretation of Constructive Set Theory.Peter Aczel, Angus Macintyre, Leszek Pacholski & Jeff Paris - 1984 - Journal of Symbolic Logic 49 (1):313-314.details Download Export citation Bookmark 78 citations
Regular universes and formal spaces.Erik Palmgren - 2006 - Annals of Pure and Applied Logic 137 (1-3):299-316.details We present an alternative solution to the problem of inductive generation of covers in formal topology by using a restricted form of type universes. These universes are at the same time constructive analogues of regular cardinals and sets of infinitary formulae. The technique of regular universes is also used to construct canonical positivity predicates for inductively generated covers. Download Export citation Bookmark 4 citations

1