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)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
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.
A Weak Intuitionistic Propositional Logic with Purely Constructive Implication.Mitsuhiro Okada - 1987 - Studia Logica 46 (4):371 - 382.
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.
A Characterization of ML in Many-Sorted Arithmetic with Conditional Application.M. D. G. Swaen - 1992 - Journal of Symbolic Logic 57 (3):924 - 953.
Added to index2009-01-28
Total downloads13 ( #355,371 of 2,172,599 )
Recent downloads (6 months)1 ( #325,337 of 2,172,599 )
How can I increase my downloads?