I know this sounds dumb, but I can't for the life of me remember how to expand "TC(x)" into a first-order term in the language of set theory (ZFC, not NBG) where epsilon is the only nonlogical symbol.
The obvious definition is an $\omega$-long sentence $x\cup (\bigcup x)\cup (\bigcup\bigcup x)…$, but that isn't in $L_{\omega\omega}$.
The definition given in Jech, p64 appeals to "the intersection of any class with a set is a set" (p8), which is really expressible only in NBG, right? I'm at a loss to figure out how to turn this into simple ZFC using separation and replacement.
I also don't have much trouble proving that for every set there exists some other set which is its transitive closure; I just can't seem to turn this proof of $(\exists y)\phi$ (for $\phi$ being "y is the transitive closure of x") into an explicit description of the $y$.
I'm starting to suspect that TC(x) isn't definable in ZFC, but that it can be defined as a class-function in NBG (which is a conservative extension of ZFC, so being able to define TC(x) doesn't actually get you any new theorems about sets).
Thanks!
Best Answer
As Mike Shulman and François G. Dorais correctly point out, the official language of set theory has only the binary relation ε, and so there are no terms to speak of in that language beyond the variable symbols.
But no set theorist remains inside that primitive language, and neither is it desirable or virtuous to do so. Rather, as in any mathematical discourse, we introduce new terminology, define notions and introduce terms. What gives? I think the substance of your question is really:
The answer is quite general. In any first order theory T, if one can prove that there is a unique object with a certain property, then one may expand the language by adding a term for that object, plus the defining axiom that that term has the desired property. The resulting theory T+ will be a conservative extension of T, meaning that the consequences of T+ that are expressible in the old language are exactly the same as the consequences of T. The reason is that any model M of T can be (uniquely) expanded to a model of T+, simply by interpreting the new term in M by its definition. This is why we may freely introduce symbols for emptyset or ω (or Q and R) and so on to set theory. Similarly, if T proves that for every x, there is a unique object y such that φ(x,y), then we may introduce a corresponding symbol fφ(x), with the defining axiom ∀x φ(x,fφ(x)). This new theory, in the expanded language with fφ, is again conservative over T.
This is what is going on with the term TC(x) for the transitive closure of x. Although there is no official term for the transitive closure of x in the basic language of set theory, we may introduce such a term, once we prove that every set x does indeed have a transitive clsoure. And once having done so, the term becomes officially part of the expanded language.
To see that every set x has a transitive closure, one needs very little of ZFC, and as Dorais mentions in the comments to your question, you don't need to build the Vα hierarchy. For example, every set has a transitive closure even in models of ZF- (and much less), where the power set axiom fails and so the Vα hierarchy does not exist. Simply define a sequence x0 = x and xn+1 = U xn. By Replacement, the set { xn | n ε ω } exists, and the union of this set is precisely TC(x).
In summary, we should feel free to introduce defined terms, and there is absolutely no reason not to write TC(x) on the chalkboard, as you mentioned. In particular, we should not feel compelled to express our beautiful mathematical ideas in a primitive language with only ε, like some kind of machine code, just because it is possible in principle to do so.