Yhyjyk

So I was reading about the ZFC axioms, and apparently some of them are actually "axiom schemas." For example, there is the "axiom schema of specification," which basically says that give a set $A$ and a formula $phi(x)$, a subset of $A$ exists where all the elements satisfy $phi(x)$.

This is apparently not one axiom, but a schema of infinitely many axioms, because there is one axiom for every $phi(x)$. So that must mean that for whatever reason, just letting $phi(x)$ be an arbitrary formula does not make a valid axiom. So are there rules for what an axiom can say?

So my questions are: Why is this not allowed to be one axiom? What are the rules for what an axiom is allowed to be? And why?

This is just the choice of underlying logic. ZFC is a theory in first-order logic, and the strictures of that logical system rule out certain kinds of expressions. There are other logics, and their study comprises abstract model theory.

Very roughly, there are two competing hopes for a logical system:

• It should be expressive: things we intuitively want to be able to say, should be say-able in the system.




• It should be not too wild: e.g. there should be a well-behaved notion of proof.

It turns out that these are fundamentally in tension. For example, if we want proofs to be finite, then our logical system can't capture infinite structures up to isomorphism (this is the compactness theorem, essentially).

So why did we pick first-order logic after all, given that it forces us to use axiom schemata (and other inefficiencies)? Well, first-order logic seems to sit at a sweet spot here: it's fairly expressive, but also has a very well-behaved notion of proof and a more technical property called the "Lowenheim-Skolem property" which roughly says that it doesn't interact too much with set theory (indeed, it's the most expressive logic with these properties - this is due to Lindstrom).

This paper of Ferrairos may be of interest with regard to how first-order logic emerged as "the" primary logic of mathematics.

In ZF, all expressions must ultimately be a syntactically valid, finite combination of variable names, the $forall$ quantifier, parentheses, the logical operations $lnot$ and $lor$, $=$ and finally $in$. That's it.

Of course, in practice we have a lot of other symbols, like $subseteq$ and $exists$, but technically they are all defined as specific shorthands for combinations of the symbols above.

There is no way to use these to say $forall phi(phitext is a formulatoldots)$, the way one might want to do to make the axiom schema into actual axioms.

Noah Schweber pointed out that there is a tension between expressiveness of a logic and having a nice proof theory. There is another tension, between expressiveness and inconsistency.

More expressive logical systems were developed in the early 1930s by Church (a form of $lambda$ calculus) and separately by Curry (a form of combinatory logic, essentially a different kind of $lambda$ calculus). These logics were more expressive in the sense that they could refer to their own formulas more directly than in first-order logic, essentially by allowing variables to refer to terms or formulas.

Unfortunately, both of these systems were shown to be inconsistent by Kleene and Rosser in a joint paper in 1935. (Church had already tried to modify his system to avoid inconsistency, but they showed his revised system was inconsistent as well as Curry's system of the time.) More information is available in the article "Paradoxes and Contemporary Logic" by Andrea Cantini and Riccardo Bruni in the Stanford Encyclopedia of Philosophy. (Recall that other, earlier logics systems that tried to be very strong, such as Russell's original system for Principia Mathematica, were also found to be inconsistent.)

After the inconsistencies were found, Church and Curry both turned their attention to weaker systems, including the simply typed $lambda$ calculus developed by Church. The inconsistent systems slipped into history, but they are still important examples on the limits to what can be put into a logic.

We now realize that there is a limit on how much a logic can refer to itself. Variations of Richard's paradox and Curry's paradox arise easily with too much self-reference. In a sense, first-order logic and theories such as Peano Arithmetic and ZFC stay just inside this limit. The result is that PA and ZFC are consistent but are subject to Gödel's incompleteness theorems. Adding just slightly more self-reference - which seems to be very hard to avoid in systems that can quantify over and manipulate their own formulas - tends to create systems that are inconsistent or where some terms are undefined or some formulas have undefined truth values. You can't have it all in a consistent logic.

First-order logic avoids all of this by having no direct way for formulas or terms to refer to or quantify over other formulas or terms. We don't have to worry about undefined terms or undefined truth values, and the logic itself is consistent. A side effect is that infinite lists of formulas sometimes have to be included as infinite lists of axioms, rather than as a single axiom that quantifies over the formulas. This is usually viewed as an acceptable cost, given the other nice properties of the logic.