first-order definability transitive closure operator 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!
 A: As an addendum to Joel Hamkins answer: the weaker assertion (`Transitive Containment')
that every set x is contained in a transitive set 
(not necessarily its transitive closure) is not provable
in ZF - Replacement (sometimes known as Z Zermelo-set theory).
As Joel says in his answer we need to collect together the results of taking successive
$\bigcup$. For this $\Sigma_1$-Replacement is more than enough (if AxFoundation is formulated
in the right way for $\Pi_1$ classes).
As a second addendum (as the discussion continues) one should remark that we have in full ZF the $\in$-recursion theorem: thus we may define the class function $x\rightarrow TC(x)$  within ZFC (no need for NBG) via the recursion scheme
                  $$TC(x)= \bigcup [TC(y) : y\in x] \cup x $$.
The function defined has just the same status as $\alpha \rightarrow V_\alpha$ (which is also defined by such a recursion scheme). The former guarantees the existence of $TC(x)$ for any $x$, the latter of $V_\alpha$ for any $\alpha$. Neither function is problematic for the full ZF-set theorist. 
The original question seems to be spurred on by the fact that we do not have an obvious {\em explicit  definition} for $TC(x)$ in the way that we do for say ordered pairs. However that is often the case: turning recursive definitions into explicit definitions
may not be possible.
A: I think the "correct" answer is that the question is misguided, but I'm going to try to give lots of alternate answers in case one of them makes you happier.
In ZFC set theory as usually phrased, there are no terms at all in the sense of logic, other than variables (i.e. there are no function symbols in the logical signature).  There are only axioms which assert that sets satisfying certain properties exist (and are unique).  For instance, any expression involving $\bigcup x$ is shorthand for a statement about any (hence the unique) set which contains exactly those $y$ such that $y\in z\in x$ for some $z$.  That's even true about the empty set symbol $\emptyset$!  So any statement about "$TC(x)$" will also have to formally be a statement about any (hence the unique) set which is a transitive closure of $x$.
One might try to make all of the axioms of ZFC into term-forming operators, so that instead of saying "there exists a set with no elements" there would be a specified term $\emptyset$ and an axiom saying "$\emptyset$ has no elements," and likewise for pairings, unions, replacement, etc.  (Of course the operator for replacement will have to take a first-order formula as its input as well as a set.)  In that case you should be able to apply the "replacement operator" followed by the "union operator" in order to construct a term describing $x \cup \bigcup x \cup \bigcup\bigcup x \cup \dots$.
Alternately, one can add a choice operator such that for any formula $\phi$, the term $\varepsilon x. \phi(x)$ has the property that if there exists an $x$ with $\phi(x)$, then in fact $\phi(\varepsilon x.\phi(x))$.  Then you can define $TC(x) = \varepsilon y. ISTC(y,x)$.  In this case, one could even restrict to a unique choice operator which only applies to formulas $\phi$ such that there is at most one $x$ satisfying $\phi(x)$.
We can also write $TC(x)$ in the undergraduate's "set-builder notation:"
$$ TC(x) = \Big\lbrace y \;\Big\vert\; (\forall z)\; \Big( (\forall a,b)\; a\in b \wedge b\in z \Rightarrow a\in z\Big) \wedge x \subseteq z \Longrightarrow y\in z \Big\rbrace $$
but of course ZFC does not include general set-builder notation as a term-forming operation, nor can it be extended to do so, since not every set-builder notation forms a set (e.g. $\lbrace x \mid x\notin x\rbrace$).
A: 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: 


*

*How can a set theorist (or any mathematician) sensibly and legitimately use terms that are not expressible as terms in the official language of the subject?


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.
A: (Apologies to admins again for not yet registering. )
I believe Kunen's book on Independence Proofs in Set Theory has
a first order representation for TC(x)  (transitive closue, I'm guessing.)
Something like forall x,y,z, x=TC(x) iff {(z in y) and (y in x) implies (z in x)}.
I am being sloppy with the quantifiers, but assuming foundation, something like
the above should work.
Gerhard "Ask Me About System Design" Paseman, 2010.01.19
