- New
-
Topics
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- Journals
- Submit material
- More
The Friedman‐Translation for Martin‐Löf's Type Theory
Mathematical Logic Quarterly 41 (3):314-326 (1995)
Abstract
In this note we show that Friedman's syntactic translation for intuitionistic logical systems can be carried over to Martin-Löf's type theory, inlcuding universes provided some restrictions are made. Using this translation we show that the theory is closed under a higher type version of Markov's ruleOther Versions
No versions found
My notes
Similar books and articles
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.
An Intuitionistic Version of Cantor's Theorem.Dario Maguolo & Silvio Valentini - 1996 - Mathematical Logic Quarterly 42 (1):446-448.
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 Justification of Identity Elimination in Martin-Löf’s Type Theory.Ansten Klev - 2019 - Topoi 38 (3):577-590.
Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
Decidability in Intuitionistic Type Theory is Functionally Decidable.Silvio Valentini - 1996 - Mathematical Logic Quarterly 42 (1):300-304.
The independence of peano's fourth axiom from Martin-löf's type theory without universes.Jan M. Smith - 1988 - Journal of Symbolic Logic 53 (3):840-845.
A Construction of Type: Type in Martin-Lof's Partial Type Theory with One Universe.Erik Palmgren - 1991 - Journal of Symbolic Logic 56 (3):1012-1015.
EM + Ext− + ACint is equivalent to ACext.Jesper Carlström - 2004 - Mathematical Logic Quarterly 50 (3):236-240.
Programming in Martin-Löf's Type Theory. An Introduction.Kent Petersson & Jan M. Smith - 1992 - Journal of Symbolic Logic 57 (1):272-274.
Analytics
Added to PP
2013-12-01
Downloads
42 (#558,368)
6 months
1 (#1,572,794)
2013-12-01
Downloads
42 (#558,368)
6 months
1 (#1,572,794)
Historical graph of downloads
Citations of this work
Minimal models of Heyting arithmetic.Ieke Moerdijk & Erik Palmgren - 1997 - Journal of Symbolic Logic 62 (4):1448-1460.
References found in this work
Constructivism in Mathematics: An Introduction.A. S. Troelstra & Dirk Van Dalen - 1988 - Amsterdam: North Holland. Edited by D. van Dalen.
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-99fc7d78b-gv576 uwo