Why are all well-defined properties allowed in the Axiom schema of specification in ZFC in FOL?

In first order logic, well-formed formulas are formulas that can be written down using the quantifiers with their bounded variables, free variables, connectives, negation, equality and predicates (in this case: $$\in$$).

ZFC can be formulated in first-order logic (or in second-order logic, but my problem only occurs in the first-order formulation).

The axiom of pairing of ZFC is an example of such a well-formed FOL formula. It says that given sets A and B there exists a set C which is the pair of A and B:

$$\forall A \forall B \exists C \forall D \left[ D \in C \Leftrightarrow (D = A \vee D = B) \right]$$

Note that the negation of this formula is also a well-formed formula (albeit false in a model satisfying ZFC):

$$\neg \forall A \forall B \exists C \forall D \left[ D \in C \Leftrightarrow (D = A \vee D = B) \right]$$

Further, we can enumerate all well-formed formulas in FOL.

The axiom schema of specification is now instantiated once for each well-formed formula $$\phi$$. It is a countably infinite list of axioms, that states for each well-formed formula $$\phi$$ that the following is true:

$$\forall w_1, \ldots, w_n . \forall A . \exists B . \forall x . \left( x \in B \Leftrightarrow \left[ x \in A \wedge \phi (x, w_1, \ldots, w_n) \right] \right)$$

A simpler version with well-formed formulas without free variables is enough for my question, so let's look at this instead:

$$\forall A . \exists B . \forall x . \left( x \in B \Leftrightarrow \left[ x \in A \wedge \phi (x) \right] \right)$$

You may also know it as set comprehension where the existence of B is written as: $$\{x \in A : \phi(x) \}$$.

My question is, what makes us confident, that these axioms of specification are true?

Consider the following instantiation of the axiom scheme of replacement:

$$B = \{x \in \{ \{\} \} : \phi(x) \}$$, where $$\phi(\{\}) = true \iff$$ Goldbach conjecture is true.

The set B is either empty $$\{\}$$ (Goldbach conjecture is false) or is $$\{\{\}\}$$ (Goldbach conjecture is true).

It seems a little crazy to me that the previous statement is an axiom of ZFC. It has to be true since we can construct both {} and {{}} in other ways. But an axiom? Further, what prevents us from using well-defined formulas $$\phi$$ that are independent of ZFC in the axiom scheme?

This problem vanishes in the second-order logic formulation of ZFC, since we don't have a schema over the set of well-defined formulas.

My question is a bit open ended, since it's a question about axioms: Why are all well-defined properties allowed in the Axiom schema of specification in ZFC in FOL?

Is there a FOL theory where only provable FOL formulas are allowed in the axiom of separation?

Or better, do we have a proof or a notion that ZFC under FOL is equivalent to ZFC under 2OL?

• You may not allow arbitrary formulas to appear in the separation schema: Then we will get restricted form of separation, which results in weaker set theories. Second-order logic formulation does not eradicate a pathology you mentioned since second-order formulation of ZFC can also define $\{0\mid \text{Goldbach Conjecture is true}\}$. Commented May 12 at 20:38
• Regarding: You may not allow arbitrary formulas to appear in the separation schema. Can you point me to a list of permissible formulas? Regarding the second point: I thought in 2OL you don't have the axiom schema of separation. Instead you can just quantify over subsets of A. Commented May 12 at 21:04
• True where? In a model of ZFC? It's true since these are axioms of ZFC. Commented May 12 at 22:35
• "Permissible formulas" depend on the customary choice of the system. For example, Kripke-Platek set theory has Separation only for $\Delta_0$-formulas. I do not understand the meaning of 2OL not having Separation. Second-order set theories usually have their own version of Separation, and some types of second-order logics have separation-like rules as a part of logic. Commented May 12 at 23:20
• You may not have a proper understanding for second-order set theories. Second-order quantifiers are quantified over predicates. In the case of second-order arithmetic, the domain is usually deemed as the set of natural numbers, so the predicates are interpreted as subsets of $\mathbb{N}$, so some literatures simply say "second-order quantifiers quantify over sets." In set theory, first-order quantifiers quantify over sets, and second-order quantifiers quanfity over classes. Commented May 12 at 23:23

Is there a FOL theory where only provable FOL formulas are allowed in the axiom of separation?

To this I ask, what is a "provable FOL formula"? For instance, is "$$x$$ is finite" a provable FOL formula? What about "$$x \ne \emptyset$$"? In both cases, we can write definitions of sets that for which the formula is provable true or provable false. But we can also write definitions of sets for which we currently know no proof either way. (Example: the set of odd perfect numbers.)

Now the axiom of separation allows us to form the sets $$\{x \in \mathcal{P}(\mathbb{N}) : x\text{ is finite}\}$$ and $$\{x \in \mathcal{P}(\mathbb{N}) : x \ne \emptyset\}$$, even though there are values for $$x$$ we could substitute for which we don't know whether the property holds.

Further, what prevents us from using well-defined formulas $$\phi$$ that are independent of ZFC in the axiom scheme?

Nothing, but this is not a problem. A formula "independent of ZFC" is necessarily a sentence, having no free variables. Let's say $$P$$ is such a formula, like Goldbach's conjecture. Then, for any set $$A$$, the set $$\{x \in A : P \}$$ is either $$A$$ or $$\emptyset$$, both of which exist. So, this instance of separation is harmless. Removing it would not affect the theory at all.

We can be more general. Suppose $$\psi$$ is a formula that mentions $$P$$ at some point. Let $$\psi^T$$ be $$\psi$$ with $$P$$ replaced with an always true formula, and let $$\psi^F$$ be $$\psi$$ with $$P$$ replaced with an always false formula. Now define the sets

\begin{align} B &= \{x \in A : \psi(x) \} \\ C &= \{x \in A : \psi^T(x) \} \\ D &= \{x \in A : \psi^F(x) \} \end{align}

Then, a proof by cases shows that $$B = C$$ or $$B = D$$. Again, the set we form using $$P$$ is equal to one we can form without using $$P$$, we just don't know which. To look at this another way, consider the following three instances of Separation:

\begin{align} \forall A\,\exists B\,\forall x\,&( x \in B \Leftrightarrow [ x \in A \wedge \psi (x) ] ) \tag{1} \\ \forall A\,\exists B\,\forall x\,&( x \in B \Leftrightarrow [ x \in A \wedge \psi^T (x) ] ) \tag{2} \\ \forall A\,\exists B\,\forall x\,&( x \in B \Leftrightarrow [ x \in A \wedge \psi^F (x) ] ) \tag{3} \end{align}

Then, $$[(2) \land (3)] \implies (1)$$. Thus, $$(1)$$ is a redundant axiom, and removing it would not change the theory. (These results depend crucially on the fact that $$P$$ has no free variables!)

To sum up, the instances of Separation you are concerned about are logical consequences of the other instances. So while we could make a rule forbidding them, it would ultimately make no difference: we can just prove them anyway.

• Thanks Eric! You brought the example of P(N) which is uncountably big. Therefore, there are subsets of P(N) that can't be expressed by any well-formed formula $\phi$, since there are only countably many well-formed formulas. What gives us the confidence, that there is a well formed formula, that filters the sets in a non-sense way? You only convinced me of well-formed formulas that are either always true or always false. Commented May 20 at 16:47
• I don't understand the source of your concern. Do you have a specific example of an instance of Separation that you doubt the truth of? Commented May 21 at 1:46
• Yes, for example: $\{x \in \mathcal{N} : collatzsequenceterminatesto1(x) \}$ This set is equivalent to $\mathcal{N}$ if the collatz conjecture is true, but who knows what the set looks like if it turns out that the collatz conjecture is false. I struggle that we can create an arbitrary subset of $\mathcal{N}$ of which we aren't sure of its existence. Assume that collatzsequenceterminatesto1 is independent of ZF. Now we are in big trouble, since the set can be both, $\mathcal{N}$ and whatever other interpretation there is. Commented May 21 at 14:36
• Okay. Do you believe that the Collatz conjecture has a truth value independent of any axioms? Do you believe that the Collatz conjecture could be true but unprovable in ZF? Commented May 24 at 5:29
• There could be non standard models of ZF in which Collatz conjecture is false and some models in which they are true. The collatz conjecture would be unprovable in ZF assuming ZF is consistent. Commented May 26 at 17:00