Categoricity results for second-order ZF in dependent type theory

DOI10.1007/978-3-319-66107-0_20zbMath1468.03012MaRDI QIDQ1687749

Gert Smolka, Dominik Kirst

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_20

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

03E70: Nonclassical and second-order set theories

03C62: Models of arithmetic and set theory

03C35: Categoricity and completeness of theories

68V20: Formalization of mathematics in connection with theorem provers

03B38: Type theory

Related Items

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

Uses Software

• Coq

Cites Work

• Set theory. An introduction to independence proofs
• Set theory for verification. I: From foundations to functions
• Die Widerspruchsfreiheit der allgemeinen Mengenlehre
• Sur le théorème de Zorn
• Hereditarily Finite Sets in Constructive Type Theory
• Transfinite Constructions in Classical Type Theory
• A Declarative Language for the Coq Proof Assistant
• 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
• Two notes on the foundations of set-theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item