Isabelle/GST

A generalized set theory (GST) is like a standard set theory but also has non-set structured objects that can contain other structured objects including arbitrary sets. For a discussion of the preceding work, please see:

• Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories. Dunne, Wells, 2022.
• Generating Custom Set Theories with Non-Set Structured Objects. Dunne, Wells, Kamareddine, 2021.

This development adds Isabelle/HOL support for GSTs:

• Features that specify kinds of mathematical objects, defined as classes with some extra structure.
• Combining features to create GSTs, also as classes.
• Model components that specify schematics for building models of GSTs,
• Integration with Lifting and Transfer for connecting a model of a GST in a type dᵢ to another type dⱼ.

Installation Instructions

Prerequisites

1. Isabelle 2021-1:

Our development is built in Isabelle/HOL, using the 2021-1 version of Isabelle. Installation instructions and documentation can be found on the Isabelle webpage.

Make sure that the Isabelle binary is in your $PATH environment variable.

2. A clone of ZFC_in_HOL:

We use Paulson's ZFC_in_HOL, which is an entry in Isabelle's Archive of Formal Proofs (AFP), to bootstrap our development. Download the entry and unpack the contents into an appropriate directory DIR. Then make ZFC_in_HOL available to Isabelle:

• For UNIX based systems:

isabelle components -u DIR/ZFC_in_HOL

• For Windows 10 using Cygwin, if DIR is on drive DRIVE:

isabelle components -u /cygdrive/DRIVE/DIR/ZFC_in_HOL

Installing and building Isabelle/HOL/GST

1. Clone this repository:

git clone [email protected]:ultra-group/isabelle-gst.git

or alternatively using HTTPS:

git clone https://github.com/ultra-group/isabelle-gst.git

2. If you don't want to have to check ZFC_in_HOL, then navigate to isabelle-gst and build heap images:

cd isabelle-gst; make build-heap

3. Open a file in Isabelle/jEdit, using ZFC_in_HOL as a base logic. For example:

isabelle jedit -l ZFC_in_HOL src/GST_Features.thy

Alternatively, open Isabelle/jEdit and manually change the logic:

Plugins > Plugin Options > Isabelle > General > Logic > ZFC_in_HOL

After changing logic, restart Isabelle/jEdit and open a file.

Building HTML for browsing

To build the HTML for output in html/, run:

make build-html

Entry Points

File	Description
GST_Logic.thy	Definition of the definite description with a default operator
Soft_Types.thy	Definition of Soft Types, inspired by Kappelmann/Krauss/Chen
Tools/*.ML	Isabelle/ML code for building GSTs
GST_Features.thy	Definintion of GZF, Ordinal, OPair, Relation, Function, Exception features
GZF/*.thy	Development of GZF feature
Ordinal/*.thy	Development of Ordinal feature
OPair/*.thy	Development of OPair feature
Function/*.thy	Development of Function feature
Exception/*.thy	Development of Exception feature
Relations/*.thy	Development of Binary Relation feature
ModelKit/*.thy	Model building kit
ModelKit/Tools/*.ML	Isabelle/ML code for building models of GSTs
Founder/ZFC_in_HOL_Bootstrap.thy	Instantiating V as a GST
Founder/Test.thy	Building ZF⁺ in d₀ by building a model in V

Usage

Features & GSTs

1. To define a GST feature, first define a class of the form:

class Foo = D₁ + ... + Dₙ +
  fixes 
    Foo_default :: 'a and 
    ...
  assumes 
    ...

a. To perform reasoning from the axioms of a feature, open the context of the feature's class by:

context Foo begin
...
end

2. Declare a feature as an ML value, specifying terms for logo and cargo types:

ML ‹val Foo = Feature
  { cla = @{class Foo}, deps = [GZF], 
    logo = @{trm ...}, cargo = @{trm ...},
    default_param = @{trm Foo_default} }›

3. Define a list of feature configurations:

ML ‹val GST_spec = 
  [ {feat = Foo, default_val = @{term ...}, blacklist = [...]},
    {feat = Bar, default_val = @{term ...}, blacklist = [...]},
    {feat = Baz, default_val = @{term ...}, blacklist = [...]} ]›

4. Create a class for a GST called by:

local_setup ‹snd o mk_gst "<NAME>" GST_spec›