Generating Custom Set Theories with Non-Set Structured Objects

EasyChair Preprint 5663

Abstract

Set theory has long been viewed as a foundation of mathematics, is pervasive in mathematical culture, and is explicitly used by much written mathematics. Because arrangements of sets can represent a vast multitude of mathematical objects, in most set theories every object is a set. This causes confusion and adds difficulties to formalising mathematics in set theory. We wish to have set theory's features while also having many mathematical objects not be sets. A generalized set theory (GST) is a theory that has pure sets and may also have non-sets that can have internal structure and impure sets that mix sets and non-sets. This paper provides a GST-building framework. We show example GSTs that have sets and also (1) non-set ordered pairs, (2) non-set natural numbers, (3) a non-set exception object that can not be inside another object, and (4) modular combinations of these features. We show how to axiomatize GSTs and how to build models for GSTs in other GSTs.

Keyphrases: abstraction, foundations of mathematics, inductive datatypes, interactive theorem proving, set theory

@booklet{EasyChair:5663,
  author    = {Ciarán Dunne and Joe Wells and Fairouz Kamareddine},
  title     = {Generating Custom Set Theories with Non-Set Structured Objects},
  howpublished = {EasyChair Preprint 5663},
  year      = {EasyChair, 2021}}