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

Ciarán Dunne; Joe Wells

doi:10.1007/978-3-031-16681-5_3

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

Ciarán Dunne, Joe Wells

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

45 Downloads (Pure)

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 language	English
Title of host publication	Intelligent Computer Mathematics
Subtitle of host publication	15th International Conference, CICM 2022; Tbilisi, Georgia, September 19–23, 2022; Proceedings
Editors	Kevin Buzzard, Temur Kutsia
Publisher	Springer
Chapter	3
Pages	38-55
ISBN (Electronic)	978-3-031-16681-5
ISBN (Print)	978-3-031-16680-8
DOIs	https://doi.org/10.1007/978-3-031-16681-5_3
Publication status	Published - 17 Sept 2022
Event	15th Conference on Intelligent Computer Mathematics - Tbilisi, Georgia Duration: 19 Sept 2022 → 23 Sept 2022 https://cicm-conference.org/2022/cicm.php

Publication series

Name	Lecture Notes in Computer Science
Volume	13467
ISSN (Print)	0302-9743

Conference

Conference	15th Conference on Intelligent Computer Mathematics
Abbreviated title	CICM 2022
Country/Territory	Georgia
City	Tbilisi
Period	19/09/22 → 23/09/22
Internet address	https://cicm-conference.org/2022/cicm.php

Keywords

Higher-order logic
Isabelle
Set theory
Soft types

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-031-16681-5_3

Download pdf
This is a post-peer-review, pre-copyedit version of a paper published in Intelligent Computer Mathematics. CICM 2022. The final authenticated version is available online at: https://doi.org/10.1007/978-3-031-16681-5_3
Accepted author manuscript, 591 KB

Cite this

Dunne, C., & Wells, J. (2022). Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories. In K. Buzzard, & T. Kutsia (Eds.), Intelligent Computer Mathematics: 15th International Conference, CICM 2022; Tbilisi, Georgia, September 19–23, 2022; Proceedings (pp. 38-55). (Lecture Notes in Computer Science; Vol. 13467). Springer. https://doi.org/10.1007/978-3-031-16681-5_3

@inproceedings{1c10621572c64651bc913889f45eb426,

title = "Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories",

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.",

keywords = "Higher-order logic, Isabelle, Set theory, Soft types",

author = "Ciar{\'a}n Dunne and Joe Wells",

year = "2022",

month = sep,

day = "17",

doi = "10.1007/978-3-031-16681-5_3",

language = "English",

isbn = "978-3-031-16680-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "38--55",

editor = "Kevin Buzzard and Temur Kutsia",

booktitle = "Intelligent Computer Mathematics",

address = "United States",

note = "15th Conference on Intelligent Computer Mathematics, CICM 2022 ; Conference date: 19-09-2022 Through 23-09-2022",

url = "https://cicm-conference.org/2022/cicm.php",

}

Dunne, C & Wells, J 2022, Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories. in K Buzzard & T Kutsia (eds), Intelligent Computer Mathematics: 15th International Conference, CICM 2022; Tbilisi, Georgia, September 19–23, 2022; Proceedings. Lecture Notes in Computer Science, vol. 13467, Springer, pp. 38-55, 15th Conference on Intelligent Computer Mathematics, Tbilisi, Georgia, 19/09/22. https://doi.org/10.1007/978-3-031-16681-5_3

Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories. / Dunne, Ciarán; Wells, Joe.
Intelligent Computer Mathematics: 15th International Conference, CICM 2022; Tbilisi, Georgia, September 19–23, 2022; Proceedings. ed. / Kevin Buzzard; Temur Kutsia. Springer, 2022. p. 38-55 (Lecture Notes in Computer Science; Vol. 13467).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Dunne, Ciarán

AU - Wells, Joe

PY - 2022/9/17

Y1 - 2022/9/17

N2 - 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.

AB - 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.

KW - Higher-order logic

KW - Isabelle

KW - Set theory

KW - Soft types

UR - http://www.scopus.com/inward/record.url?scp=85138772915&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-16681-5_3

DO - 10.1007/978-3-031-16681-5_3

M3 - Conference contribution

SN - 978-3-031-16680-8

T3 - Lecture Notes in Computer Science

SP - 38

EP - 55

BT - Intelligent Computer Mathematics

A2 - Buzzard, Kevin

A2 - Kutsia, Temur

PB - Springer

T2 - 15th Conference on Intelligent Computer Mathematics

Y2 - 19 September 2022 through 23 September 2022

ER -

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

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this