Second-order logic as the basis for set theory

Question

Currently, the most common definition of set theory is built from first-order logic, which means that to include substitution requires an infinite schema of axioms for every possible case because of first-order logic's limitations to scope of variables.

Would basing set theory in second-order logic mean we can rewrite the schema of substitution as a single axiom? Are there practical benefits to this? Are they worth losing completeness and compactness from first-order logic, or are they equivalent (as in we just switch the 'problem' from sets to the language)?

Answer 1

The thing about the second-order of $\sf ZFC$ is that $M$ is a model of second-order $\sf ZFC$ if and only if $M$ is isomorphic to $V_\kappa$ for an inaccessible $\kappa$. So right off the bat you start with a much stronger consistency assumptions. Okay, that might not be a real problem. I mean, we believe $\sf ZFC$ is consistent, what's one more inaccessible cardinal, eh? But wait, there's more!

Not only that we lose a bunch of useful tools from first-order logic, we also seemingly determine things like the truth value of $\sf CH$ (since every model must contain all the reals and sets of reals, so they must agree on the truth value of $\sf CH$), and so we lose the ability to use forcing as a tool for proving certain statements.

Moreover, there is an inherent problem basing set theory on second-order logic: the notion of a set is more or less required for the development of second-order logic, so your meta-theory should already include some version of set theory to begin with.

Now, normally this is not a terrible thing where your meta-theory is the same as your theory (in principle, anyway), since we often treat the meta-theory of $\sf ZFC$ as $\sf ZFC$ itself again. But therein lies the rub: first-order is nice and recursive and we can replace the meta-theory from $\sf ZFC$ to something stupendously weak like $\sf PRA$, and all the proofs remain more or less the same (except schemata of proofs done in the meta-theory which are now slightly more complicated); whereas with second-order logic you cannot really weaken your theory too much.

And even if you could, you lose the whole point for which we fight for first-order logic. You lose the ability to recursively identify and check the correctness of proofs. This is one of the good reasons that a set theoretic foundation is useful. Since second-order logic does not have a nicely algorithmic proof theory to it, moving from second-order things (like analysis and topology which are even of higher-order) to first-order statements like "$\sf ZFC$ proves bla bla bla" allows us to compensate for this problem.

On top of all this, second-order $\sf ZFC$ can have multiple models and it is not complete in any sense of the word (for example, if $\kappa<\lambda$ are two inaccessible cardinals, then $V_\kappa$ and $V_\lambda$ are both models of second-order $\sf ZFC$, but only one of them satisfies "There exists an inaccessible cardinal").

---

To sum up, here are the main problems:

1. Second-order $\sf ZFC$ requires a stronger consistency assumptions to produce models of the theory.
2. Second-order logic requires a notion of "set" from the get-go, so some set theoretic meta-theory is needed.
3. Second-order $\sf ZFC$ forces us to accept whatever the meta-theory decided on a variety of statements like $\sf CH$, making the role of the meta-theory much greater than we would have liked to in our mathematics.
4. Second-order logic has a lousy proof theory to it, so you lose all that you wanted to gain in terms of automatic proof verification for "everyday mathematics" which is often done in high-order logic and using $\sf ZFC$ we translate it back to first-order logic.