Hereditarily finite sets in constructive type theory
From MaRDI portal
Publication:2829273
DOI10.1007/978-3-319-43144-4_23zbMATH Open1478.03073OpenAlexW2490033929MaRDI QIDQ2829273FDOQ2829273
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
Nonclassical and second-order set theories (03E70) Formalization of mathematics in connection with theorem provers (68V20) Axiomatics of classical set theory and its fragments (03E30)
Cites Work
- A Formalisation of Finite Automata Using Hereditarily Finite Sets
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- Finite sets and Gödel's incompleteness theorems
- Die Widerspruchsfreiheit der allgemeinen Mengenlehre
- Finitary set theory
- Induction and foundation in the theory of hereditarily finite sets
- A foundation of finite mathematics
Cited In (11)
- Induction and foundation in the theory of hereditarily finite sets
- Title not available (Why is that?)
- Categoricity results for second-order ZF in dependent type theory
- Title not available (Why is that?)
- Heirs of box types in polynomially bounded structures
- Title not available (Why is that?)
- Title not available (Why is that?)
- Trakhtenbrot’s Theorem in Coq
- Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
- On Arithmetic Computations with Hereditarily Finite Sets, Functions and Types
- Hereditary undecidability of some theories of finite structures
Uses Software
Recommendations
This page was built for publication: Hereditarily finite sets in constructive type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829273)
