The Friedman-Translation for Martin-Löf's Type Theory

Erik Palmgren, Mathematical Logic Quarterly 41(1995), 314 - 326.

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, including universes provided some restrictions are made. Using this translation we show that the theory is closed under a higher type version of Markov's rule.

Back to the list of publications.

Erik Palmgren, March 9, 1999.