Return to Question

Revision in response to early comments. Users of set theory need an implementation (in case "model" means something different) of the axioms. I would expect something like this:

An implementation consists of a "collection-of-elements" $X$, and a relation (logical pairing) $E:X\times X\to \{0,1\}$. A logical function $h:X\to\{0,1\}$ is a set if it is of the form $x\mapsto E[x,a]$ for some $a\in X$. Sets are required to satisfy the following axioms: ....

The background "collection-of-elements" needs some properties to even get started. For instance "of the form $x\mapsto E[x,a]$" needs first-order quantification. Mathematical standards of precision seem to require some discussion, but so far I haven't seen anything like this. The first version of this question got answers like $X$ is "the domain of discourse" (philosophy??), "everything" (naive set theory?) and "a set" (circular). Is this a missing definition? Taking it seriously seems to give a rather fruitful perspective.

Revision in response to early comments. Users of set theory need an implementation (in case "model" means something different) of the axioms. I would expect something like this:

An implementation consists of a "collection-of-elements" $X$, and a relation (logical pairing) $E:X\times X\to \{0,1\}$. A logical function $h:X\to\{0,1\}$ is a set if it is of the form $x\mapsto E[x,a]$ for some $a\in X$. Sets are required to satisfy the following axioms: ....

The background "collection-of-elements" needs some properties to even get started. For instance "of the form $x\mapsto E[x,a]$" needs first-order quantification. Mathematical standards of precision seem to require some discussion, but so far I haven't seen anything like this. The first version of this question got answers like $X$ is "the domain of discourse" (philosophy??), "everything" (naive set theory?) "a set" (circular), and "type theory" (a postponement, not a solution). Is this a missing definition? Taking it seriously seems to give a rather fruitful perspective.

The extensionality axiom states that sets are the same if they contain the same elements, or conversely, sets are different if there is an element of one that is not an element of the other. This means the element operator $x\in A$ must be a logical function: it does not just produce elements, but must be able to recognize when something is not an element. Question: what is the domain of this function?

Essentially this asks for an a priori way to specify "all possible elements of all sets" in some implementation of the axioms, before defining sets. Worrying about domains is a mathematical thing. If set theory is to provide a foundation for mathematics then it seems to me this question needs a clear, unproblematic answer. Trying to define it in terms of sets or classes is circular. Naive unlimited comprehension is not satisfactory. Philosophical analysis of the question is unhelpful.

Perhaps there is a definition missing, of collections of elements weaker than sets but able to support logical functions. This could also clarify the relationship with categories and homotopy-type-theory. Question: has something like this already been explored?

Revision in response to early comments. Users of set theory need an implementation (in case "model" means something different) of the axioms. I would expect something like this:

An implementation consists of a "collection-of-elements" $X$, and a relation (logical pairing) $E:X\times X\to \{0,1\}$. A logical function $h:X\to\{0,1\}$ is a set if it is of the form $x\mapsto E[x,a]$ for some $a\in X$. Sets are required to satisfy the following axioms: ....

The background "collection-of-elements" needs some properties to even get started. For instance "of the form $x\mapsto E[x,a]$" needs first-order quantification. Mathematical standards of precision seem to require some discussion, but so far I haven't seen anything like this. The first version of this question got answers like $X$ is "the domain of discourse" (philosophy??), "everything" (naive set theory?) and "a set" (circular). Is this a missing definition? Taking it seriously seems to give a rather fruitful perspective.

The extension axiom states that sets are the same if they contain the same elements, or conversely, sets are different if there is an element of one that is not an element of the other. This means the element operator $x\in A$ must be a logical function: it does not just produce elements, but must be able to recognize when something is not an element. Question: what is the domain of this function?

Essentially this asks for an a priori way to specify "all possible elements of all sets" in some implementation of the axioms, before defining sets. Worrying about domains is a mathematical thing. If set theory is to provide a foundation for mathematics then it seems to me this question needs a clear, unproblematic answer. Trying to define it in terms of sets or classes is circular. Naive unlimited comprehension is not satisfactory. Philosophical analysis of the question is unhelpful.

Perhaps there is a definition missing, of collections of elements weaker than sets but able to support logical functions. This could also clarify the relationship with categories and homotopy-type-theory. Question: has something like this already been explored?

The extensionality axiom states that sets are the same if they contain the same elements, or conversely, sets are different if there is an element of one that is not an element of the other. This means the element operator $x\in A$ must be a logical function: it does not just produce elements, but must be able to recognize when something is not an element. Question: what is the domain of this function?

Essentially this asks for an a priori way to specify "all possible elements of all sets" in some implementation of the axioms, before defining sets. Worrying about domains is a mathematical thing. If set theory is to provide a foundation for mathematics then it seems to me this question needs a clear, unproblematic answer. Trying to define it in terms of sets or classes is circular. Naive unlimited comprehension is not satisfactory. Philosophical analysis of the question is unhelpful.

Perhaps there is a definition missing, of collections of elements weaker than sets but able to support logical functions. This could also clarify the relationship with categories and homotopy-type-theory. Question: has something like this already been explored?