1
$\begingroup$

The separation axiom of ZFC states

Suppose some set $x$ exists, and let $C$ be any condition. Then there exists a set $y$ consisting of all and only the members of $x$ that satisfy $C$.

To translate this into FOL, and since they can't quantify over $C$s, people employ an axiom schema, an infinite set (?!) of axioms.

This seems circular to me (using sets to define sets?), but perhaps I'm misunderstanding something here.

Is it fair to say that ZFC axioms can not even be stated in FOL?

$\endgroup$
16
  • $\begingroup$ Look at the separation scheme precisely ... $C$ is a formula (in the language of set theory) and an instance of the scheme is "For any $z$, there exists $y$ such that for all $x$, [ ($x$ is in $y$) if and only if ($x$ is in $z$ and $C$) ]" where $y$ and $z$ are not free in $C$ (I'm not sure if I have the restrictions on the free variables of $C$ correct). The intuitive idea is that $y$ separates out the elements of $z$ which satisfy the formula $C$, but that intuition is not part of the axiom. $\endgroup$ – Ned Sep 17 '20 at 21:16
  • 3
    $\begingroup$ Incidentally, if for some reason you really care about having only finitely many axioms, you can always just work with $\mathsf{NBG}$ instead; it's a conservative extension of $\mathsf{ZFC}$, which is to say that any statement about sets (as opposed to sets and classes) which you can prove in $\mathsf{NBG}$ can be proved in $\mathsf{ZFC}$ and vice versa. $\endgroup$ – Noah Schweber Sep 17 '20 at 22:29
  • 1
    $\begingroup$ Compare that with the arithmetic situation: second-order vs. first-order Peano arithmetic. Again we have a higher-order principle in the former - namely, the induction principle - replaced with a first-order scheme in the latter which, while vastly weaker, is still sufficient for proving the vast majority of results in arithmetic outside of mathematical logic. The strongest claim one may make in either case is that the scheme version is somehow the "most natural" way to first-orderize the higher-order principle; I've said a bit about that here. $\endgroup$ – Noah Schweber Sep 17 '20 at 22:53
  • 1
    $\begingroup$ I don't know why people are voting to close - I didn't. I do think though that it's somewhat unclear what exactly you're asking: how is the issue of "using sets to define sets" related to the shift to an infinite set of axioms? I'm not sure I see the circularity you're getting at here. $\endgroup$ – Noah Schweber Sep 18 '20 at 3:17
  • 1
    $\begingroup$ My point is that I don't need to use the phrase "infinite set" to give you a description of the ZFC axioms - say, in the form of an algorithm which determines whether a given sentence is one of those axioms. So in what sense do I run into a circularity in using those axioms? $\endgroup$ – Noah Schweber Nov 5 '20 at 4:23
11
$\begingroup$

No, that's not true at all.

Let's start with the most basic of meta-theories: $\sf PRA$, the theory of Primitive Recursive Arithmetic. Here we have the natural numbers, and the primitive recursive functions.

This theory is strong enough to internalise FOL, so we can just assume that we're manipulating strings. The point of an axiom schema is that it is a predicate that lets us recognise all the axioms which have a certain form. And any reasonable schema, including those of $\sf ZFC$, are in fact primitive recursive. In other words, there is a primitive recursive function $f_{\rm Sep}(n)$ which takes in $n$, and if $n$ is the Gödel number of a formula with some basic properties $\varphi$, then $f_{\rm Sep}(n)$ is the Gödel number of the axiom obtained from the schema by putting $\varphi$ into it. If $n$ is not the Gödel number of a suitable formula, just return the axiom for the formula $\varphi$ given by $x=x$ or something like that.

Since $\sf ZFC$ is presented as finitely many axioms and one or two schemata (Separation and Replacement, but Replacement is generally enough to prove Separation, making it redundant), then the collection of Gödel numbers of axioms of $\sf ZFC$ is in fact primitive recursive. So we can really talk about the first-order theory that is $\sf ZFC$.

To recap, the point of the schemata is to allow us to have infinitely many axioms with the same structure—that we can recognise mechanically—so that when we need to use any such axiom in a proof, we can always be sure that it is part of this or not.


Another way to approach this is by saying that our foundation is in fact $\sf ZFC$. We use set theory to discuss set theory. This sounds circular, but how is this any different than using $\sf PRA$ to study the logical consequences of $\sf PRA$? It's not. Mathematics is not something that we do in vacuum, some assumptions are needed. And it is perfectly fine to study $\sf ZFC$ inside $\sf ZFC$.

There, we have the notions of sets already existing, so we can talk about a set of axioms. Of course, we need to argue why a certain set exists, which is to say that we need to be able to prove that the set of these axioms actually exists. And again we use the fact that a schema is a function which takes formulas and returns axioms, so we may replace the schema with the axioms, as it is the range of this function.

So again, we have that $\sf ZFC$ is a set of first-order axioms in the language of set theory.

$\endgroup$
2
  • 4
    $\begingroup$ Let me add a few words regarding what I imagine is part of the intent behind the question: First-order logic is one way of formalizing certain intuitions regarding provability, and stating a theory in first-order logic is sometimes just a way of making the ideas behind the theory precise while providing a robust mathematical framework to analyze it. One could argue that formalizing ZFC in first order fails to capture the "true extent" of our set-theoretic intuitions. I certainly have felt this way at times. $\endgroup$ – Andrés E. Caicedo Sep 17 '20 at 23:25
  • $\begingroup$ Thanks, Andrés. Good addition. $\endgroup$ – Asaf Karagila Sep 17 '20 at 23:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.