Second order ZFC, intuition required

Question

Here it is explained that the second order ZFC is the first order ZFC with second order variants of its axioms. I would like to see what second order variants look like and what intuitively they say. In particular, what in particular the second order replacement, regularity, comprehension and infinity are, and what do they say? What is the language of the second order ZFC?

Answer 1

EDIT: in light of Carl Mummert's comments below, I've decided to add a clarification re: semantics of second-order logic to this answer. It's a bit long, so it's at the end.

---

The language of second-order ZFC is still just $\{\in\}$. The only thing that changes is the underlying logic. There is a syntactic change, but it's at the logical level: the logical symbols now include second-order quantifiers and variables, in addition to the usual first-order ones. Note that this shift has nothing to do with ZFC in particular.

Incidentally, the syntax of second-order logic varies slightly from presentation to presentation. For example, some texts explicitly allow variables for (and hence quantification over) arbitrary-arity relations and functions, while others disallow function variables since functions can be coded by relations. Below I'm going to commit a grievous sin, and only use unary relation variables. In general this results in monadic second-order logic, which is a strictly weaker beast. In the ZFC context, however, since we have a definable ordered pairing operator we can quantify over $n$-ary relations as soon as we can quantify over unary relations.

Since ZFC itself is a theory talking about sets, a bit of linguistic convention is helpful here. In addition to using capital letters for second-order variables, I'll call elements of the model "objects," and relations on the model "collections." (Using the word "set" would just be confusion.)

Now let's think about what the axioms look like!

• Extensionality, Pairing, Union, and Choice are unchanged (that is, we use their usual first-order forms).

• Separation. Second-order separation will ultimately be redundant. However, I think it's intuitively useful to state at the outset: $$\forall x\forall Y\exists z\forall w[w\in z\iff w\in x\wedge Y(w)].$$ This says that every subcollection of a set is a set. A possibly more intuitive form of this axiom is $$\forall x\forall Y[(\forall u(Y(u)\implies u\in x))\implies(\exists z\forall w(w\in z\iff Y(w)))].$$ This formulation explicitly takes $Y$ to denote a subcollection of $x$, rather than implicitly looking at $Y\cap x$.

• Powerset. This axiom states that true powersets exist: $$\forall x\exists y\forall Z\exists w\in y\forall u(u\in w\iff Z(u)\wedge u\in x).$$ That is, for every $x$ there is some $y$ containing each set corresponding to a subcollection of $x$. (Again, we've implicitly passed to $Z\cap x$; we could tweak the expression above to instead restrict attention explicitly to subcollections of $x$.) Note that as written, we actually "overshoot" the powerset; but then just apply separation.

At this point, it's worth proving (note that this proof takes place inside first-order ZFC; usual ZFC is proving a statement about second-order ZFC, as understood by first-order ZFC):

Suppose $(M, \in^M)$ is a model of second-order ZFC, $a,b\in M$, and $M\models a=\mathcal{P}(b)$. (This is an abbreviation of course.) Then in fact $b$ really "is" the powerset of $a$: precisely, we have (in the "real" world) that for every subset $S$ of $\{e\in M: e\in^Ma\}$, there is some $c\in M$ such that $c\in^M b$ and $\{d\in M: d\in^Mc\}=S$.

In particular, we get as a corollary:

Suppose $(M, \in^M)$ is a model of second-order ZFC. Then $M$ is uncountable.

Proof. Think about what $M$ thinks is the powerset of $\omega$. $\quad\Box$

And of course we can show that $M$ is much bigger than just uncountable, by iterating this same argument.

Now, back to the axioms!

• Replacement. The only subtlety here is the use of quantification over functions. Intuitively, second-order Replacement says "If $x$ is an object and $F$ is a function with domain $x$, the range of $F$ exists as an object." Using only unary relational second-order quantifiers as per our convention above, this can be expressed as "For every $x$ and every collection $Y$ such that for each $y\in x$ there is exactly one $z$ with $Y(\langle y, z\rangle)$, there is some $w$ such that for each $y\in x$ there is some $z\in w$ with $Y(\langle y, z\rangle)$." Writing this out in symbols is a bit messy, but not hard.

• Regularity and Infinity. There are natural second-order versions of these axioms; however, in the presence of the axioms above, the usual first-order versions already give their full power! Let me outline why this is true in the case of Regularity; recall that Regularity itself emerged as a first-order approximation of the statement "The universe of sets is well-founded," which is not first-order by the Compactness Theorem. I claim that if $(M, \in^M)$ is a model of the axioms above, plus usual first-order regularity, then $(M,\in^M)$ is (in the "real" world) truly well-founded. To see this, for $a\in M$ let $b_a\in M$ denote (what $M$ thinks is) $a$'s transitive closure, and consider the collection $X_a\subseteq M$ consisting of all $x$ such that $x\in^M b$ and the transitive closure of $x$ is (truly) ill-founded. If $M$ is ill-founded, then for some $a$ we have $X_a$ nonempty; by second-order Separation we get a $c\in M$ corresponding to this $X_a$, but $X_a$ can never have an $\in^M$-minimal element, and so $c$ witnesses the failure of first-order Regularity in $(M, \in^M)$.

---

If you play around with the above, you'll see that we in fact have a lot of freedom; there are many ways to axiomatize second-order ZFC which all yield the same result. The same thing, incidentally, is true of first-order ZFC (think about Replacement versus Collection). Things get much dicier, though, when we look at weaker theories, and this is true even in the first-order case (e.g. see this paper on what ZFC without Powerset should be).

---

Some comments on second-order logic

There is a fundamental subtlety when discussing second-order logic. Unlike with first-order logic, there are (at least) two very different kinds of semantics which are natural and interesting: the standard semantics and the Henkin semantics. Under Henkin semantics, second-order logic is just a kind of repackaging of first-order logic - a structure for second-order logic in the Henkin sense is a first-order structure together with a family of subsets of (and relations on) that structure serving as the domain of the second-order quantifiers. In the standard semantics, we presuppose a background set-theoretic universe and assume that all second-order quantifiers always range over the "true" powerset of the domain.

The drawbacks of both semantics are probably clear. Henkin semantics, much of the time, misses the point of passing from first-order to second-order, namely that we want to bring set theory into the picture; I would argue that this is one of those times. On the other hand, of course the standard semantics immediately forces us to make a huge set-theoretic commitment. In particular, what axioms is the assumed ambient universe supposed to satisfy? (For instance, there is a second-order sentence $\varphi$ which is a tautology according to the standard semantics iff the Continuum Hypothesis is true in the background universe.) Relatedly, there can be no good (= sound, complete, and computable) proof system for the standard semantics.

For this answer, I'm assuming the standard semantics. My assumption is that the background universe of sets is a model of at least the usual first-order ZFC axioms. It turns out that this assumption, despite what one's immediate response might be, does not trivialize things. In particular, first-order ZFC proves nontrivial facts about second-order ZFC so conceptualized (e.g. that if $\kappa$ is inaccessible then $V_\kappa$ is a model of second-order ZFC).

To link things up with Carl Mummert's comments below, in the Henkin semantics a second-order structure in the language $\Sigma$ (which as usual is a collection of relation, function, and constant symbols) is a triple $\mathcal{A}=(A, I, P)$ where $(A, I)$ is a $\Sigma$-structure in the first-order sense, and $P$ is a family of relations on $A$ to be treated as the domain of the second-order quantifiers. The standard semantics can be thought of as restricting attention to models of the form $(A, I, P)$ where $P$ is the actual set of all relations on $A$; note that this also presupposes the existence of a background universe. The drawback, for me, of this approach is that the notion of "structure" has changed. I prefer to fold the set theory into the definition of $\models$ for second-order logic, and have my structures look just like first-order structures.