The inconsistency of higher order extensions of Martin-Löf's type theory

DOI10.1007/BF00262943MaRDI QIDQ583201zbMATH OpenFDO

Authors Bart Jacobs

Publication date 1989

Published in Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF00262943

zbMATH Keywords

constructive higher order systemsinconsistencyMartin-Löf's constructive type theory

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• scientific article; zbMATH DE number 1746890
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• A construction of type: type in Martin-Löf's partial type theory with one universe
• scientific article; zbMATH DE number 733401
• scientific article; zbMATH DE number 3853066

Cited in

(8)

• Proceeding in Abstraction. From Concepts to Types and the Recent Perspective on Information
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
• scientific article; zbMATH DE number 733401 (Why is no real title available?)
• scientific article; zbMATH DE number 1746890 (Why is no real title available?)
• Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
• scientific article; zbMATH DE number 1420853 (Why is no real title available?)
• ERRATA: "The paper: MARTIN-LOF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK"

This page was built for publication: The inconsistency of higher order extensions of Martin-Löf's type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q583201)