The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
From MaRDI portal
Publication:3809795
DOI10.2307/2274575zbMath0661.03045OpenAlexW2017438886WikidataQ114589028 ScholiaQ114589028MaRDI QIDQ3809795
Publication date: 1988
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2274575
First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35)
Related Items
Introducing data types in intuitionistic type theory, Constructing a small category of setoids, Classical predicative logic-enriched type theories, Coalgebras in functional programming and type theory, Remarks on Martin-Löf's partial type theory, Setoids and universes, A pluralist approach to the formalisation of mathematics, Domain theoretic models of polymorphism, A general formulation of simultaneous inductive-recursive definitions in type theory
Cites Work
