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.
Foundations of set theory relates to answers of the following two main questions:
(A) What is a set?
(B) What does it mean to reason with sets?
With respect to (A) Cantor's informal definition of the notion of a set seems perfectly intuitive.
It is natural to think of collection into a whole as an act of abstraction. The question is how to understand this. In view of the paradoxes by Russell and others, the idea to make this more precise by saying that any given property defines a set seemed to be in conflict with intended natural modes of reasoning. What was wrong with this idea?
It might be an issue of confusing extensional and intensional perspectives. The idea of a set as a gathering of given objects into a whole paints a picture of sets as collections (a, b,.. .). We have given objects and we collect them into a whole by so to speak bracketing them. This extensional view of sets has a clear expression in the cumulative hierarchy. Abstracting with respect to a given property introduces a more intensional perspective, i.e., the way in which we actually define a set with the intention to capture a collection of objects.
Russell's antinomy came as a veritable shock to those few thinkers who occupied themselves with foundational problems at the turn of the century. [4, p. 2]
There is something strange about this reaction. Why do we expect that such a, very general, more intensional characterisation will capture just sets as collections of objects in an intuitive extensional sense, i.e., as bracketing a given collection of objects? There is no reason to think that these two notions and perspectives should coincide, i.e., that the intensional characterisation would produce just nice sets, namely collections of given objects. It is in this respect of interest to note that
the definition, i.e., the defining property x ∈/ x of the Russell set R is a very ele-
mentary one. Its proof-theoretic behaviour can, for example, be observed already in
intuitionistic propositional logic .
So if we accept the idea of abstraction with respect to any given defining property, i.e., full comprehension, as a foundation for set theory, we have an answer to question (A), that is, what a set is. But how should we then understand the paradoxes? The Russell paradox for instance seems to show that something is wrong with respect to question (B). The paradoxical argument builds on several basic assumptions, where one of the most important ones is the assumption that 'R is a set' is a well-defined notion with respect to intended intuitive logical reasoning, which is a very strong assumption with respect to the given definition. So this is one way to view Russell's paradox; too strong assumptions on basic theoretical notions.
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 (see ). There are several ideas about proof-theoretically founded restrictions on the comprehension scheme , . Compare further the set theory of Fitch (see , ), the notion of a Frege structure  and notions of structural rules in relation to paradoxes .
Now 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 confounding intensional and extensional perspectives.