The logic of first order intuitionistic type theory with weak sigma- elimination

Journal of Symbolic Logic 56 (2):467-483 (1991)
  Copy   BIBTEX

Abstract

Via the formulas-as-types embedding certain extensions of Heyting Arithmetic can be represented in intuitionistic type theories. In this paper we discuss the embedding of ω-sorted Heyting Arithmetic HA ω into a type theory WL, that can be described as Troelstra's system ML 1 0 with so-called weak Σ-elimination rules. By syntactical means it is proved that a formula is derivable in HA ω if and only if its corresponding type in WL is inhabited. Analogous results are proved for Diller's so-called restricted system and for a type theory based on predicate logic instead of arithmetic

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,221

External links

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

Through your library

Similar books and articles

Undecidability and intuitionistic incompleteness.D. C. McCarty - 1996 - Journal of Philosophical Logic 25 (5):559 - 565.
The completeness of Heyting first-order logic.W. W. Tait - 2003 - Journal of Symbolic Logic 68 (3):751-763.
On Almost Orthogonality in Simple Theories.Itay Ben-Yaacov & Frank O. Wagner - 2004 - Journal of Symbolic Logic 69 (2):398 - 408.
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
On the role of implication in formal logic.Jonathan P. Seldin - 2000 - Journal of Symbolic Logic 65 (3):1076-1114.
Models of intuitionistic TT and N.Daniel Dzierzgowski - 1995 - Journal of Symbolic Logic 60 (2):640-653.

Analytics

Added to PP
2009-01-28

Downloads
39 (#354,874)

6 months
1 (#1,028,709)

Historical graph of downloads
How can I increase my downloads?