If a set is defined with a well-defined formula whose free or bound variables are all bounded by already well-defined sets, then it is well defined.
(In a formula, a bound variable x is bound to a quantifier such as "for all x" or "there is at least one x". A variable is free when it is not bound.)
A set is not well defined if it is defined from sets which are not themselves well defined. The truth of a set-theoretic formula that contains one or more unbounded variables depends on the domain of all sets, but this domain is not a well-defined set and cannot be. It therefore seems that it is necessary to limit the variables in the definition of the sets for them to be well defined.
The axiom of unrestricted comprehension (Frege 1893) does not respect this obligation: for any well-defined formula with one free variable F(x) there exists a set of all x such that it is true that F(x). The free variable x is not bounded. Russell showed that this axiom leads to a contradiction for the well-defined formula "x is not an element of x", because the set of all sets which are not elements of themselves should be an element of itself and not be (Russell's paradox 1905).
Zermelo's axiom of separation (1908) which can also be called the axiom of restricted comprehension, respects the obligation to limit the variables for the free variable: for any well-defined formula with one free variable F(x) and any already well-defined set S, there exists a set of all elements x of S such that it is true that F(x). The free variable x is bounded by S. But Zermelo did not specify what is a well-defined formula, so he said nothing about unbounded bound variables in these formulas.
The separation axiom formulated by Fraenkel (1922) does not respect the obligation to limit the variables for bound variables: for any formula with a free variable F(x) of first-order logic applied to set theory and any set S, there exists a set of all x elements of S such that it is true that F(x). First-order logic formulas can contain unbounded bound variables. If we want to be sure that a set whose existence we prove with the axiom of separation is well defined, it is better to dispense with unbounded bound variables in the formula which is used to define it.
The sum set axiom (Zermelo 1908) respects the obligation to limit the variables, or nearly so: for any set S, the set of all the elements of elements of S exists. For any set S, the set of all x such that x is an element of y for at least one y in S exists. In "x is element of y for at least one y in S", the bound variable y is bounded by S, the free variable x is bounded by y which is not a set already defined but which is bounded by a set already defined.
The axiom of the pair does not respect the obligation to limit the variables: for all sets x and y, there exists a set of all z such that z=x or z=y. The free variable z in "z=x or z=y" is not bounded. But in this case, it would be senseless to require it to be, because the pair {x,y} is obviously well-defined if x and y are both well defined.
The power set axiom does not respect the obligation to limit the variables: for any set S, the set of all its parts exists. For any set S, there exists the set of all sets x such that for all y, if y is an element of x then y is an element of S. Neither the free variable x nor the bound variable y in the formula "for all y, if y is an element of x then y is an element of E" are bounded by already defined sets, y is only bounded by x. But in this case, it would be senseless to impose the obligation to limit the variables, because the set of parts of a well-defined set is always well-defined.
Fraenkel's replacement axiom (1922) does not respect the obligation to limit the variables: for any functional relation R(x,y) and any set S there exists a set of all y such that R(x, y) for at least one x in S. A set is obtained by replacing all the elements x of S by their companion y in the relation R. In "R(x,y) for at least one x in S" the bound variable x is bounded by S. The free variable y is not bounded by an already defined set, but this is not a problem, because y is implicitly bounded by the set of all sets already defined when the set E and the relation R are already defined. On the other hand the functional relation R(x,y) poses a problem, because it can be defined with a formula which contains unbounded bound variables. If we want to be sure that the sets whose existence we prove with the replacement axiom are well defined, we must first ensure that the functional relation we use is well defined.
To found the theory of sets, we start with two fundamental sets, the empty set and the set of natural numbers. The axiom of the empty set affirms the existence of the first: there exists a set x such that for all y, y is not an element of x. We prove that this set is unique with the axiom of extensionality: if x and y are sets which have the same elements then they are the same set. For all sets x and y, x=y if for all z, z is an element of x if and only if z is an element of y.
We can define the natural numbers by identifying 0 with the empty set { }, and n+1 with {0, ... n} for any natural number n. This is the von Neumann convention. With this convention a natural number n is always identified with a set which contains n elements. 1={0}, 2={0,1}, 3={0,1,2}... n+1 is the union (the sum of the pair) of n and {n}. To prove the existence of the set of all natural numbers, we can use an axiom of infinity. For example: there is a set which contains the empty set and which always contains the pairs and sum sets of its elements. There exists a set x such that { } is element of x and for all y and z, if y and z are elements of x then the sum set of y and the pair {y,z} are also elements of x. We can also postulate directly that the set of natural numbers exists. It is the smallest set which contains 0 and which always contains n+1 if it contains n. A precise formulation of the axiom of existence of the set of natural numbers is given as a complement below.
We define the other sets from the two fundamental sets with the axioms of the pair, of the sum set, of the power set, of separation and of replacement. We postulate that the empty set and the set of natural numbers are well defined. We also postulate that the pair, the sum set and the power set of well-defined sets are well-defined. From there we can define new sets with which we can limit the variables in the axiom of separation. We postulate that a set is well-defined if we can prove its existence with the axiom of separation, and a formula of first-order logic applied to set theory, whose free or bound variables are bounded by sets already well defined. We also postulate that a set is well-defined if we can prove its existence with the replacement axiom, provided that it is applied to a well-defined functional relation. By proceeding in this way, we obtain a set theory in which all the sets are well defined.
Note: mathematicians do not always know that we can do without unbounded quantifiers in the definitions of sets, because they often use them without realizing that they are not necessary. Unbounded quantifiers can always be replaced by quantifiers bounded by large enough sets, the existence of which is proven with the axiom of infinity and the power set axiom.
The axiom of existence of the set N of natural numbers
There exists a set N which contains 0, which always contains n+1 if it contains n, and which is included in all the sets which contain 0 and which always contain n+1 if they contain n.
(0 is the empty set { }, n+1 is the union of x and {x})
In other words:
There exists a set N such that 0 is element of N, for all x, if x is element of N, then x+1 is element of N, and for all y , if (0 is element of y and for all z, if z is element of y then z+1 is element of y) then for all w, if w is element of N then w is element of y.
We can prove with the axiom of extensionality that this set N is unique if it exists. We can prove that it exists from an axiom of infinity and the axiom of separation, by limiting all the variables to the infinite set initially postulated or to the set of its parts.
The truth about sets
The truth of a mathematical theory is generally defined with respect to a model of the theory, or to a class of models. Theorems are true because they are true of the models. To prove the truth of the theorems, it suffices to prove the truth of the axioms for the models, because the logical consequences of true axioms are necessarily also true. In this case, models, not axioms, are our ultimate criterion of truth. But this conclusion does not apply to the most fundamental mathematical theories. The axioms of set theories are our ultimate criterion of truth, not the models.
A model of a set theory is defined with a domain of all the sets whose existence the theory recognizes. If the model is well-defined, its domain of sets is a well-defined set. But the domain of all sets cannot itself be a well-defined set, because for any well-defined set, one can always define a larger set. The domain of sets with which a model is defined can therefore never be the domain of all sets, so it cannot serve as a criterion of truth for all theorems. Some formulas about sets may be true for some models and false for others.
The models of set theories are not their criterion of truth. But then what is the criterion? Why say of a set theory that it is true? We recognize the truth about sets by directly recognizing the truth of the axioms, without having to establish that they are true for one or more models. We recognize the truth of the axiom of extensionality as soon as we understand the concept of sets: sets are equal if they have exactly the same elements. We recognize the truth of the axioms of existence of sets as soon as we understand that the sets whose existence we affirm are well defined. The correctness of our definitions when we define sets is therefore the ultimate criterion of mathematical truth.
Fraenkel, Abraham, Abstract set theory (1953)