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

Journal of Symbolic Logic 56 (2):467-483 (1991)
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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2274694
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history
Request removal from index
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 28,191
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

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.

Monthly downloads

Added to index


Total downloads

13 ( #355,371 of 2,172,599 )

Recent downloads (6 months)

1 ( #325,337 of 2,172,599 )

How can I increase my downloads?

My notes
Sign in to use this feature

There  are no threads in this forum
Nothing in this forum yet.

Other forums