"Quantifying" over properties and "operations" in ZFC and transfinite recursion: clarifying confusion

Question

In the book "Introduction to Set Theory" by Hrbacek and Jech, there is a concept of an operation defined for a special type of a fomula, or a property.

Given a property $P(x,y)$ such that $\forall x \exists! y: P(x,y)$ holds, one can defined an "operation" $G$ by settings $\forall x: G(x) = y \Leftrightarrow P(x,y)$ holds

This is really an informal concept, trying to formalize a notion of a function between classes in ZFC, where all objects are sets, so "classes" do not exist. It's easy to extend this "definition" to a general case of a formula with arbitrary many (free) variables:

Given a property $\phi(x,y,w_1,...,w_n)$ such that $\forall x,w_1,...,w_n \exists!y: \phi(x,y,w_1,...,w_n)$ holds, we can define an operation $G$ for any $w_1, ..., w_n$ such that $G(x) = y \Leftrightarrow \phi(x,y,w_1,...,w_n)$ holds.

Obviously, given a set $A$, we can define a restriction of $G$ as a function $G|_{A}$ from $A$ via the axiom schema of replacement: let $Y = \{ G(x) \ | \ x \in A \}$, and let $G|_{A} = \{(x,y) \in A \times Y \ | \ y = G(x) \}$

Hrbacek and Jech use these concepts in their version of the transfinite recursion theorem:

For any operation $G$ there is an operation $F$: for all ordinals $\alpha$, $F(\alpha) = G(F|_{\alpha})$

However, I've recently heard that you can't quantify over anything other than a set in ZFC (as it's a first-order theory). I must confess, I have only a vague understanding of that statement, but I suspect that you can't quantify over formulas, or "operations". Thus, the aforementioned version of the transfinite recursion is not well-defined as far as ZFC is concerned.

However, the axiom schema of specification is also stated for arbitrary formulas/properties:

Given a formula $\phi(x,w_1,...,w_n)$, $\forall w_1,...,w_n\forall A\exists B = \{x \ | \ x \in A, \phi(x, w_1,..., w_n) \}$

I would be grateful to a clarification of my confusion regarding those two questions:

$(1)$ Can we quantify over formulas in ZFC? That is, can we talk about arbitrary formulas such as "for every formula $\phi$, or "there exists a formula $\phi$"?

$(2)$ Is the concept of an operation in Hrbacek-Jech is well-defined, and if not, what is a workaround?

Answer 1

No, we can't quantify over formulas. We can use some tricks (for example, we could quantify over Godel numberings of formulas) but they don't turn out to work very well. That's why the axiom schema are schema, not axioms - a "scheme" is a (usually infinite) collection of axioms. For example, the Axiom Schema of Specification you mentioned should be thought of as an infinite collection of axioms, one for each formula $\phi$.

The concept of an operation as given is not well-defined within ZFC - so, for example, no statement like "for every operation $G$..." can be a theorem of ZFC. But it can be that for each formula $\phi$, "such-and-such holds of the operation defined by $\phi$" is a theorem of ZFC. So, for example, the transfinite recursion theorem should be thought of as a single theorem in the meta-theory, but infinitely many separate theorems within the theory of ZFC (one for each formula $\phi$ defining an operation).

Answer 2

The point is that set theory does not happen in a vacuum. It happens inside some meta-theory, and inside one which is suitable for doing things like induction and applying deduction rules.

We, as mathematicians, are not bound inside one system. We can—as long as we understand the subtleties and differences—operate within the theory, the meta-theory, the meta-meta-theory, and so on. These things only depend on our choice of setting. And the only caveat is to understand fully what can be done in the theory, and what requires going to the meta-theory.

Quantifying over formulas is something that cannot be done in the theory.^(*) But it can be done in the meta-theory. So what this means, for example, when we talk about the Replacement and Subset schemata, is that we have a pattern which has a parameter, and the axiom looks "the same" except that we vary the parameter over all possible instances. This usually results in an infinite list of axioms, but one that we can recognize algorithmically. That is important for the development of a proof verification process.

The same goes here. When we say that for every $G$ there is some $F$, we actually stating infinitely many theorems, but we sort of say "All these proof look the same, modulo the fact that the formulas for $G$ are different". Or rather, what we prove is that "given a formula which provably defines an operation, there is an algorithm for writing a formula for another operation with such and such provable properties".

---

_{(*) I won't make it more confusing by talking about bounded truth predicates, these will turn up later on, but first it would be a good idea to learn about the incompleteness theorem in depth, since that would help to alleviate some of the conceptual difficulties.}