Categoricity results for second-order ZF in dependent type theory

DOI10.1007/978-3-319-66107-0_20zbMath1468.03012OpenAlexW2748981990MaRDI 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

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 (3)

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

This page was built for publication: Categoricity results for second-order ZF in dependent type theory