A Logical Framework for Set Theories

TL;DR

This paper introduces a unified logical framework for various axiomatic set theories, enabling formalization and validation of set terms across different levels of set-theoretic strength, bridging gaps with mathematical practice.

Contribution

It presents a novel, unified framework that supports formalization of multiple set theories with static validation of set terms, enhancing mathematical knowledge management.

Findings

Supports formalization of diverse set theories

Enables static validation of set terms

Bridges gap between formal set theory and mathematical practice

Abstract

Axiomatic set theory is almost universally accepted as the basic theory which provides the foundations of mathematics, and in which the whole of present day mathematics can be developed. As such, it is the most natural framework for Mathematical Knowledge Management. However, in order to be used for this task it is necessary to overcome serious gaps that exist between the "official" formulations of set theory (as given e.g. by formal set theory ZF) and actual mathematical practice. In this work we present a new unified framework for formalizations of axiomatic set theories of different strength, from rudimentary set theory to full ZF. It allows the use of set terms, but provides a static check of their validity.