PaperlayerView exact revision on arXiv

Source-linked AI summary

Formalization of Fragments of the Theory of Hereditarily Finite Sets

Zuzana Haniková, Štěpán Holub

arXiv:2609.34877v1cs.LO

TL;DR

The paper addresses the lack of a comprehensive exposition of hereditarily finite set theory by formalizing its axiom-defined fragments in Isabelle/HOL. It develops a modular locale hierarchy and a semantic treatment of definable predicates, then formalizes equivalences between distinct axiomatizations and other fragment relationships.

  • Problem

    Hereditarily finite set theory lacks a comprehensive exposition, and its scattered fragment results make their relationships and the interplay of finiteness and regularity principles difficult to assess systematically.

    Source: §1 · p. 1

  • Method

    The paper formalizes axiom-defined fragments as Isabelle/HOL locales and inductively defines set-theoretically definable properties to handle axiom schemata.

    Source: §1 · p. 1

  • Results

    The formalization proves equivalence between two distinct axiomatizations of hereditarily finite sets and formalizes facts about fragment dependencies.

    Source: §1 · pp. 2–3

  • Takeaways & Limitations

    The verified presentation brings scattered results together and represents information about the relative strength of theory fragments.

    Source: §1 · p. 2

    Definitions such as the empty set’s intended meaning are clear, but its emptiness cannot be proved outside the locale providing the needed axioms.

    Source: §5 · p. 12

Abstract

from arXiv · show

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.

1 Introduction

The paper systematizes hereditarily finite set theory in Isabelle/HOL, addressing a scattered literature through a modular hierarchy of axiom-defined fragments. It formalizes equivalent finiteness and regularity principles, fragment dependencies, and independence results.

1 Introduction

  • The paper examines why regularity alone need not ensure well-founded membership without infinity, alongside interactions among replacement, separation, and induction.It also explores several ways to define finiteness in weaker axiomatic contexts.Source: §1 · p. 1
  • The theory’s interest also stems from its bi-interpretability with Peano arithmetic.The paper notes AST as an initial inspiration, but says that direction is not pursued.Source: §1 · pp. 1–2
  • The work unifies results previously scattered across sources and provides a verified account of the relative strength of theory fragments.The locale hierarchy spans more than 3000 lines of code, but the paper focuses on a convenient formalization approach and selected equivalences.Source: §1 · pp. 2–3
  • An inductive definition of set-theoretically definable properties addresses axiom schemata without formalizing formulas themselves.This semantic approach restricts predicates used in schemata to those definable in the membership-and-equality language.Source: §1 · p. 2
  • The formalization establishes equivalence between two distinct axiomatizations of hereditarily finite sets, including the set fragment of AST.The locale hierarchy represents fragments through combinations of axioms and schemata.Source: §1 · pp. 2–3
  • Positive formalized facts refine locale dependencies, while independence results use constructed models, including Rieger–Bernays permutation models.The approach demonstrates independence of regularity axioms from other axioms.Source: §1 · p. 3

2 Logic and set theory preliminaries

The preliminaries fix a one-sorted classical first-order language for set theory, with membership as its sole nonlogical symbol. They distinguish formulas and definable relations while introducing basic set-theoretic and finiteness notions.

2 Logic and set theory preliminaries

  • The theories use classical one-sorted first-order logic with equality and membership; other symbols are definable using membership and equality.The formalization uses ε for its abstract membership relation, while the presentation uses ∈.Source: §2 · pp. 3–4
  • Set-theoretic definability means that a relation in a structure is defined by a formula in the set language.This distinction matters in Isabelle/HOL because expressions definable there need not represent set formulas.Source: §2 · p. 3
  • ZF includes extensionality, empty set, union, powerset, replacement, infinity, and regularity; pairing and separation are derivable.ZFfin replaces infinity with ∈-induction and its negation, alongside extensionality, empty set, union, powerset, and replacement.Source: §2 · p. 4
  • The preliminaries define Dedekind finiteness by the absence of a bijection with a proper subset, and Tarski finiteness through maximal subsets of the powerset.They also define transitive sets, ordinals, and natural numbers.Source: §2 · p. 4

3 List of axioms used

This section lists the axioms and schemata formalized in the paper, using abbreviations as locale names. It includes set-formula schemata and multiple principles of finiteness, induction, and regularity.

3 List of axioms used

  • The axiom list uses abbreviated names for locales, and some familiar symbols become definable only in appropriate contexts.The listed principles include extensionality, empty set, and set successor.Source: §3 · p. 4
  • The formalized set-formula schemata include separation and replacement, each ranging over formulas in the set language.The list also includes induction, ∈-induction, and regularity schemata.Source: §3 · p. 5
  • The axioms include powerset, Tarski finiteness, and Dedekind finiteness.The section names these as distinct principles in the formalization.Source: §3 · p. 5
  • The list also includes transitive superset and a combined induction-and-regularity schema for set formulas.The latter is identified in connection with.Source: §3 · p. 6

4 Main formalized results

The formalization organizes hereditarily finite set theory into axiom-based locales and develops equivalences among finiteness and regularity principles in suitable contexts. It also formalizes independence results using permutation models.

4.1 Negating the axiom of infinity

  • In the context of extensionality, empty set, and set successor, set-formula induction proves several further axioms and each of the other finiteness principles.The formalization also shows induction entails union, powerset, replacement, pairing, separation, and that every set is Dedekind finite.Source: §4.1 · pp. 6–7
  • With extensionality, empty set, powerset, and replacement, negated infinity yields set-formula induction through cardinality and replacement.The proof constructs an inductive set from sets satisfying a formula, contradicting negated infinity; induction then yields union in the appropriate context.Source: §4.1 · p. 7
  • With extensionality, empty set, powerset, and replacement, the four principles—induction, negated infinity, Tarski finiteness, and Dedekind finiteness—are equivalent.For example, Dedekind finiteness yields negated infinity by contradiction using a bijection between the natural numbers and their successors.Source: §4.1 · pp. 7–8

4.2 Regularity and related principles

  • In a sufficiently strong fragment of ZFfin, epsilon induction, equivalently the regularity schema, is equivalent to regularity together with the transitive-superset axiom.The transitive-superset axiom also yields transitive closures with extensionality and separation; regularity plus that axiom yields the regularity schema.Source: §4.2 · pp. 9–10

4.3 Induction and regularity

  • The modified induction schema setindregsch yields both set-formula induction and epsilon induction with extensionality, empty set, and set successor.Conversely, it is provable from extensionality, set successor, set-formula induction, and epsilon induction; this supports equivalence of the canonical ZFfin and ASTset axiomatizations.Source: §4.3 · p. 10

4.4 Permutation models

  • The Rieger–Bernays permutation method redefines membership through a set-definable bijection, preserving extensionality, empty set, powerset, union, and replacement, but not necessarily regularity.The formalization applies the method to construct models for independence results.Source: §4.4 · p. 10
  • Swapping the empty set and its singleton preserves transitive-superset and set induction, yet makes the empty set a member of itself, showing regularity is independent of the listed axioms.The listed axioms are extensionality, empty set, powerset, union, replacement, transitive superset, and set induction.Source: §4.4 · p. 11
  • A permutation transposing n and {n+1} for nonzero natural numbers yields a model satisfying negated infinity and regularity but lacking transitive supersets and the regularity schema.Its membership relation has an infinite descending chain, while each set contains only a finite segment of that chain.Source: §4.4 · p. 11

5 Design principles of the formalization

The formalization models theory fragments as Isabelle/HOL locales over an arbitrary type, while inductively restricting predicates in axiom schemata to those definable by set-language formulas. It also develops tools for working with these predicates and explains the trade-off of defining set-theoretic symbols before their intended meanings are available.

5 Design principles of the formalization

  • Locales encode fragments through their axiom collections, with membership as the language’s only primitive relation on an arbitrary type.Locale dependencies are declared or established by interpretation or sublocale commands.Source: §5 · p. 12
  • The formalization defines symbols such as the empty set at the outset for convenience, although their intended meanings may require stronger locales to establish.The empty-set definition alone does not prove that nothing belongs to it outside the locale combining extensionality and the empty-set axiom; the empty-set axiom without extensionality also allows multiple empty sets.Source: §5 · pp. 12–13
  • SetFormulaPredicate inductively identifies predicates that correspond to first-order set formulas, excluding predicates outside the language’s definable class.Predicates act on assignments to countably many variables, allowing axiom schemata to range over formula-definable predicates.Source: §5 · p. 13
  • Named rewriting collections and rules automate proofs that predicates are set-formula definable, including predicates written with conjunction despite the inductive definition’s core logical rules.The logsimps and set_defs collections normalize logical and defined symbols before SFP_rules are applied.Source: §5 · p. 14
  • For any SetFormulaPredicate, its truth value depends on only finitely many assignment values, corresponding to the formula’s free variables.This property is proved by induction on the predicate’s structure and is captured by lemma bounded_free.Source: §5 · p. 14
  • The variable-renaming proof uses bounded_free to find a finite range of relevant variables, then transforms indices while preserving definability and predicate values.The formalization duplicates the value at the induction variable in a fresh slot before applying the setind locale axiom.Source: §5 · p. 15

6 Related work

The section places the formalization alongside Isabelle developments of set theory and first-order logic, distinguishing its locale-based semantic treatment from prior approaches. It also notes that direct comparison with those approaches is outside the paper’s scope.

6 Related work

  • Isabelle offers direct ZF formalization and ZF-in-HOL libraries, but the authors say it is unclear how those developments could serve their purposes.The HOL options include Obua’s library and Paulson’s AFP entry.Source: §6 · p. 16
  • Paulson’s HereditarilyFinite formalization defines membership on a type based on nat and verifies ZFfin axioms, whereas this work uses locales to capture axioms semantically.Paulson’s incompleteness development uses nominal types for first-order syntax, and its HF theory cannot be scaled down to subtheories.Source: §6 · p. 16
  • A direct comparison of this fully semantic approach with the cited approaches is explicitly beyond the paper’s scope.Source: §6 · p. 16

7 Concluding remark

The authors describe the formalization as open to additions, including extensions toward ZF and subsystems of Peano arithmetic. Their broader future intent is to extend it to classes and Vopěnka’s AST.

7 Concluding remark

  • Fragments without finiteness axioms can be extended with infinity to develop ZF.Source: §7 · p. 16
  • The principles used in the formalization can also be adapted to subsystems of Peano arithmetic.Source: §7 · p. 16
  • The authors’ broader intent is to extend the formalization to classes, with Vopěnka’s AST as an outlook.Source: §7 · p. 16
Loading 2609.34877v1…