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

DOI10.1007/BF00262943zbMATH Open0692.03034MaRDI QIDQ583201FDOQ583201

Authors: Bart Jacobs 

Publication date: 1989

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

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

zbMATH Keywords

inconsistencyconstructive higher order systemsMartin-Löf's constructive type theory

Mathematics Subject Classification ID

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

Cited In (8)

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

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)