Hereditarily finite sets in constructive type theory

DOI10.1007/978-3-319-43144-4_23zbMATH Open1478.03073OpenAlexW2490033929MaRDI QIDQ2829273FDOQ2829273

Authors: 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

Recommendations

• Induction and foundation in the theory of hereditarily finite sets
• On Arithmetic Computations with Hereditarily Finite Sets, Functions and Types
• A Unified Formal Description of Arithmetic and Set Theoretical Data Types
• Sets in Coq, Coq in Sets
• Finitary set theory

Mathematics Subject Classification ID

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

• 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
• Finiteness and rational sequences, constructively
• Title not available (Why is that?)
• A hierarchy of hereditarily finite sets
• Heirs of box types in polynomially bounded structures
• Title not available (Why is that?)
• Title not available (Why is that?)
• Enumeration of the adjunctive hierarchy of hereditarily finite sets
• Sets in Coq, Coq in Sets
• 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
• A formalisation of finite automata using hereditarily finite sets
• Hereditary undecidability of some theories of finite structures
• Finitary set theory

Uses Software

• Coq
• Hereditarily Finite Sets
• Finite Automata HF

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)