On the Proof-Theoretic Foundations of Set Theory

Abstract

In this paper we discuss a proof-theoretic foundation of set theory that focusses on set definitions in an open type free framework. The idea to make Cantor’s informal definition of the notion of a set more precise by saying that any given property defines a set seems to be in conflict with ordinary modes of reasoning. There is to some extent a confusion here between extensional perspectives (sets as collections of objects) and intensional perspectives (set theoretic definitions) that the central paradoxes build on. The solutions offered by Zermelo-Fraenkel set theories, von Neumann-Bernays set-class theories and type theories follow the strategy of retirement behind more or less safe boundaries. What if we revisit the original idea without making strong assumptions on closure properties of the theoretical notion of a set? That is, take the basic definitions for what they are without confusing the borders between intensional and extensional perspectives.