Hereditarily finite sets in constructive type theory

DOI10.1007/978-3-319-43144-4_23MaRDI QIDQ2829273zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(17)

• Induction and foundation in the theory of hereditarily finite sets
• scientific article; zbMATH DE number 7566073 (Why is no real title available?)
• Categoricity results for second-order ZF in dependent type theory
• Finiteness and rational sequences, constructively
• scientific article; zbMATH DE number 2167511 (Why is no real title available?)
• A hierarchy of hereditarily finite sets
• Heirs of box types in polynomially bounded structures
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• scientific article; zbMATH DE number 58733 (Why is no real title available?)
• 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
• Finitary set theory
• Hereditary undecidability of some theories of finite structures

Describes a project that uses

Uses Software

• Finite Automata HF
• Hereditarily Finite Sets
• Coq

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)