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

TL;DR

This paper introduces Isabelle/HOL support for generalized set theories (GSTs), enabling formal reasoning about complex structured objects with flexible features and consistency assurance through hierarchical models.

Contribution

It presents a novel integration of GSTs into Isabelle/HOL, including support for non-set objects, exception features, soft types, and model construction for consistency verification.

Findings

GSTs can include non-set objects and structured data.

Models for GSTs are constructed from hierarchical components.

Support for partial functions and undefinedness in formal proofs.

Abstract

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.