Meaning Confused " Theorem Schema"

Question

I was reading Enderton's "Elements of Set Theory", and came upon,

Transfinie Recrursion Theorem Schema: For any formula $\gamma(x,y)$ the following is a theorem. Assume $<$ is a well ordering on $A$. Assume that for any $f$ there is a unique $y$ such that $\gamma (f,y)$. Then there exists a unique function $F$ with domain $A$ such that $$ \gamma (F \upharpoonright \text{seg }t , F(t)) $$ for all $t \in A$.

I am confused what is meant by Theorem Schema here. Enderton explains this as an "infinite package of theorems". But what is the point?

When we write out a theorem, don't we just write a statement? Why restrict ourselves to a specific form? I feel like the Theorem Schema is limiting our scope rather than helping - or maybe I completely misunderstood its purpose.

May someone explain? Thanks!

Answer 1

The passage you quoted asserts that a certain infinite family of set-theoretic statements are all provable from the axiom system under consideration, probably ZFC. So it's describing an infinite family of set-theoretic theorems. The family contains one statement for each choice of the formula $\gamma(x,y)$. Namely, once you choose a formula $\gamma(x,y)$, the associated theorem is the part of your quotation from "Assume $<$ is $\dots$" to the final "$\dots$ for all $t\in A$."

It's reasonable to ask why Enderton doesn't just state a single theorem, that begins with "For all formulas $\gamma(x,y)$, if $<$ is a well-ordering $\dots.$" There are two reasons for that, but they both boil down to: That single statement wouldn't be a statement of set theory so it couldn't be proved in ZFC (or whatever axiom system is under consideration).

The first reason is a temporary one: I don't think Enderton's book contains any formal, set-theoretic definition of "formula", so "For all formulas" isn't formalized in the language of set theory. I said that this reason is temporary, because the notion of "formula" could be formalized in set theory (like just about any other mathematical notion); Enderton just hasn't done so.

The second reason, however, is permanent. Even if you formalize, in set theory, the notion of "formula" and then try to express Enderton's schema as a single statement, with $\gamma$ now being a bound variable (since it begins "For all $\gamma$") you'll need to express what it means for such a $\gamma$ to be true of particular sets $x,y$. This cannot be formalized in set theory. That is, the general notion of truth for set-theoretic formulas is not itself expressible as a set-theoretic formula. This fact is Tarski's "undefinability of truth" theorem, and it applies not only to set theory but to any sufficiently strong (and consistent) mathematical theory.

Because of this second reason, it's hopeless to try to convert Enderton's theorem schema into a single theorem of set theory; we're stuck with a schema.

Answer 2

What I wondered when I encountered an "axiom schema" in this same book is why they don't just call it an "axiom", and the same would apply to any "theorem schema". Certainly each of the statements provable within the axiom system is a theorem, but why isn't the statement that all of them are provable not also a "theorem", but instead a "theorem schema"?

Enderton is calling something a theorem or an axiom only if it can be written in a certain formal language. But why? The answer is that for things written in that language, one has a system of proof enjoying the following properties:

• soundness, i.e. every model satisfying the axioms also satisfies every statement that can be proved;
• completeness, i.e. every statement that is true in every model satisfying the axioms can be proved; and
• effectiveness, i.e. there is a proof-checking algorithm. (And it's a very efficient algorithm.)

However, he doesn't explain that since it's not a logic course. And how would one prove that a "theorem schema" is not expressible as a statement in the formal language? Again, that's not explained since it's not a book on logic.

(Enderton also wrote a book on logic in which the first really substantial theorem is on page 128. That can be tiresome.)

Answer 3

In short, what is being proven is a meta-theorem that says:

Take any $2$-parameter sentence $γ$ over ZFC such that ZFC proves "$\forall f\ \exists! y\ ( γ(f,y) )$".

Then ZFC proves $φ_γ$, which is the sentence ...

This meta-theorem can be applied (in the meta-system) to all formulae over ZFC, giving a whole schema of theorems over ZFC. Incidentally, this meta-theorem is itself provable in ZFC, but that is not what you want, because it would be one level deeper. Specifically, within ZFC you cannot from "ZFC proves $φ_γ$" derive "$φ_γ$". So when you are working within ZFC you do not want to invoke the theorem schema inside, because then you are stuck with a statement about ZFC and not $φ_γ$ alone. Instead you go outside to the meta-system, observe there that ZFC proves $φ_γ$, and then go back inside where you now have $φ_γ$.

In other words, the meta-theorem shows that we can for any particular such $γ$ write down a proof over ZFC of "$φ_γ$", and so it is valid for us to use "$φ_γ$" as an axiom anywhere in a proof over ZFC. It is then just like the ZFC axiom schemas where each schema cannot be expressed as a single axiom over ZFC.