The logic of first order intuitionistic type theory with weak sigma- elimination
Journal of Symbolic Logic 56 (2):467-483 (1991)
| 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 | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,705 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesBranislav R. Boričić (1986). A Cut-Free Gentzen-Type System for the Logic of the Weak Law of Excluded Middle. Studia Logica 45 (1):39 - 53.
Daniel Dzierzgowski (1995). Models of Intuitionistic TT and N. Journal of Symbolic Logic 60 (2):640-653.
Jonathan P. Seldin (2000). On the Role of Implication in Formal Logic. Journal of Symbolic Logic 65 (3):1076-1114.
G. Mints (1999). Cut-Elimination for Simple Type Theory with an Axiom of Choice. Journal of Symbolic Logic 64 (2):479-485.
Itay Ben-Yaacov & Frank O. Wagner (2004). On Almost Orthogonality in Simple Theories. Journal of Symbolic Logic 69 (2):398 - 408.
Mitsuhiro Okada (1987). A Weak Intuitionistic Propositional Logic with Purely Constructive Implication. Studia Logica 46 (4):371 - 382.
W. W. Tait (2003). The Completeness of Heyting First-Order Logic. Journal of Symbolic Logic 68 (3):751-763.
D. C. McCarty (1996). Undecidability and Intuitionistic Incompleteness. Journal of Philosophical Logic 25 (5):559 - 565.
M. D. G. Swaen (1992). A Characterization of ML in Many-Sorted Arithmetic with Conditional Application. Journal of Symbolic Logic 57 (3):924 - 953.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads3 ( #202,056 of 549,196 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
