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

DOI10.1002/malq.19950410304zbMath0827.03035OpenAlexW2051002678MaRDI QIDQ4844507

Erik Palmgren

Publication date: 13 December 1995

Published in: Mathematical Logic Quarterly (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/malq.19950410304

zbMATH Keywords

proof theoryMartin-Löf's type theoryintuitionismMarkov's ruleFriedman-translation

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40) Relative consistency and interpretations (03F25)

Cites Work

• Unnamed Item
• Unnamed Item