The independence of peano's fourth axiom from Martin-löf's type theory without universes

Journal of Symbolic Logic 53 (3):840-845 (1988)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.2307/2274575

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Categorical and algebraic aspects of Martin-löf type theory.Adam Obtułowicz - 1989 - Studia Logica 48 (3):299 - 317.
The inconsistency of higher order extensions of Martin-löf's type theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
A correspondence between Martin-löf type theory, the ramified theory of types and pure type systems.Fairouz Kamareddine & Twan Laan - 2001 - Journal of Logic, Language and Information 10 (3):375-402.
A construction of non-well-founded sets within Martin-löf's type theory.Ingrid Lindström - 1989 - Journal of Symbolic Logic 54 (1):57-64.
Homotopy theoretic models of identity types.Steve Awodey & Michael A. Warren - unknown
A construction of type: Type in Martin-löf's partial type theory with one universe.Erik Palmgren - 1991 - Journal of Symbolic Logic 56 (3):1012-1015.
Twenty-five years of constructive type theory: proceedings of a congress held in Venice, October 1995.Giovanni Sambin & Jan M. Smith (eds.) - 1998 - New York: Oxford University Press.
An interpretation of Martin-löf's type theory in a type-free theory of propositions.Jan Smith - 1984 - Journal of Symbolic Logic 49 (3):730-753.

Analytics

Added to PP
2009-01-28

Downloads
49 (#317,389)

6 months
2 (#1,232,442)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

EM + Ext_ + AC~i~n~t is equivalent to AC~e~x~t.Jesper Carlström - 2004 - Mathematical Logic Quarterly 50 (3):236.
EM + Ext− + ACint is equivalent to ACext.Jesper Carlström - 2004 - Mathematical Logic Quarterly 50 (3):236-240.
Classical predicative logic-enriched type theories.Robin Adams & Zhaohui Luo - 2010 - Annals of Pure and Applied Logic 161 (11):1315-1345.

Add more citations

References found in this work

Grundzüge der theoretischen Logik.D. Hilbert & W. Ackermann - 1928 - Annalen der Philosophie Und Philosophischen Kritik 7:157-157.

Add more references