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

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.
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
PublisherSpringer
Chapter3
Pages38-55
ISBN (Electronic)978-3-031-16681-5
ISBN (Print)978-3-031-16680-8
DOIs
Publication statusPublished - 17 Sep 2022
Event15th Conference on Intelligent Computer Mathematics - Tbilisi, Georgia
Duration: 19 Sep 202223 Sep 2022
https://cicm-conference.org/2022/cicm.php

Publication series

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

Conference

Conference15th Conference on Intelligent Computer Mathematics
Abbreviated titleCICM 2022
Country/TerritoryGeorgia
CityTbilisi
Period19/09/2223/09/22
Internet address

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

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