Formalizing parts of hereditarily finite set theory in Isabelle proof system

Formalization of Fragments of the Theory of Hereditarily Finite Sets

Logic in Computer Science

Summary

Hereditarily finite sets involve collections that are finite and have finite members all the way down. The paper explores how to write down the rules of these finite sets carefully using a formal logic system, then programs this in Isabelle/HOL, a tool that checks logical proofs. It breaks down the theory into smaller parts connected to different sets of rules or axioms, paying special attention to defining what 'finite' means in multiple equivalent ways. This work also shows how some rules cannot be derived from others by building example models that prove independence. This helps ensure the logical system is well understood and rigorously checked.

What this means in practice

  • For formal methods engineers: Develop verified software that manipulates finite set data structures by using rigorously formalized axioms in Isabelle/HOL.
  • For programming language designers: Use formal definitions of finiteness and regularity to design type systems or reasoning tools that handle finite data collections precisely.

A theory result. No direct application yet.

Authors

Zuzana Haniková, Štěpán Holub

Abstract

The axiomatization of the theory of hereditarily finite sets in first-order classical logic is systematically explored and formalized in Isabelle/HOL. The formalization uses a hierarchy of locales, each corresponding to a fragment of the theory given by a particular collection of axioms. An inductive definition of first-order definable predicates is introduced and used to formalize axiom schemata. Special attention is paid to several equivalent axioms of finiteness, as well as to several equivalent ways of expressing regularity. The work also formalizes several facts about the independence of an axiom from a system of axioms by defining appropriate models.
View PDFOpen arXiv