Categoricity results and large model constructions for second-order ZF in dependent type theory

DOI10.1007/s10817-018-9480-6zbMath1468.03013OpenAlexW2896864541MaRDI QIDQ2319994

Dominik Kirst, Gert Smolka

Publication date: 21 August 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-018-9480-6

zbMATH Keywords

categoricityCoqdependent type theorysecond-order set theorymodel constructionssets-as-trees interpretation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Nonclassical and second-order set theories (03E70) Models of arithmetic and set theory (03C62) Categoricity and completeness of theories (03C35) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)

Related Items

Unnamed Item, Categoricity results and large model constructions for second-order ZF in dependent type theory

Uses Software

• Coq
• Isabelle/ZF
• HoTT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Set theory. An introduction to independence proofs
• Set theory for verification. I: From foundations to functions
• Categoricity results for second-order ZF in dependent type theory
• Categoricity results and large model constructions for second-order ZF in dependent type theory
• Sur le théorème de Zorn
• Universe Polymorphism in Coq
• Transfinite Constructions in Classical Type Theory
• Models of Second-Order Zermelo Set Theory
• Second Order Logic or Set Theory?
• EVERY COUNTABLE MODEL OF SET THEORY EMBEDS INTO ITS OWN CONSTRUCTIBLE UNIVERSE
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Two notes on the foundations of set-theory
• Proof-irrelevance out of excluded-middle and choice in the calculus of constructions