Hereditarily Finite Sets in Constructive Type Theory

DOI10.1007/978-3-319-43144-4_23zbMath1478.03073OpenAlexW2490033929MaRDI QIDQ2829273

Gert Smolka, Kathrin Stark

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_23

Mathematics Subject Classification ID

Axiomatics of classical set theory and its fragments (03E30) Nonclassical and second-order set theories (03E70) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (4)

Trakhtenbrot’s Theorem in Coq ⋮ Categoricity results for second-order ZF in dependent type theory ⋮ Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version ⋮ Unnamed Item

Uses Software

• Coq
• Hereditarily Finite Sets
• Finite Automata HF

Cites Work

• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Finitary set theory
• A foundation of finite mathematics
• Induction and foundation in the theory of hereditarily finite sets
• Die Widerspruchsfreiheit der allgemeinen Mengenlehre
• A Formalisation of Finite Automata Using Hereditarily Finite Sets
• Finite sets and Gödel's incompleteness theorems

This page was built for publication: Hereditarily Finite Sets in Constructive Type Theory