Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories

Ciarán Dunne, Joe Wells

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Downloads (Pure)


A generalized set theory (GST) is like a standard set theory but also can have non-set structured objects that can contain other structured objects including sets.  This paper presents Isabelle/HOL support for GSTs, which are treated as type classes that combine features that specify kinds of mathematical objects, e.g., sets, ordinal numbers, functions, etc.  GSTs can have an exception feature that eases representing partial functions and undefinedness.  When assembling a GST, extra axioms are generated following a user-modifiable policy to fill specification gaps.  Specialized type-like predicates called soft types are used extensively.  Although a GST can be used without a model, for confidence in its consistency we build a model for each GST from components that specify each feature's contribution to each tier of a von-Neumann-style cumulative hierarchy defined via ordinal recursion, and we then connect the model to a separate type which the GST occupies.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication15th International Conference, CICM 2022; Tbilisi, Georgia, September 19–23, 2022; Proceedings
EditorsKevin Buzzard, Temur Kutsia
ISBN (Electronic)978-3-031-16681-5
ISBN (Print)978-3-031-16680-8
Publication statusPublished - 17 Sept 2022
Event15th Conference on Intelligent Computer Mathematics - Tbilisi, Georgia
Duration: 19 Sept 202223 Sept 2022

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conference15th Conference on Intelligent Computer Mathematics
Abbreviated titleCICM 2022
Internet address


  • Higher-order logic
  • Isabelle
  • Set theory
  • Soft types

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories'. Together they form a unique fingerprint.

Cite this