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!

-
If the class is definable, then the intersection with a set is a set by comprehension. If you can prove that $x$ is contained in a transitive set, then you don't need to talk about classes at all. You might do this by proving that $x \subseteq V_\alpha$ for some ordinal $\alpha$, for example. (By the way, this is a pretty standard homework exercise. You might want to reassure us that this is not the case.) – François G. Dorais Jan 20 '10 at 4:34
"If you can prove that x is contained in a transitive set" -- yes, exactly! But the problem is that now you have to say which $\alpha$, so now you need a "function symbol" for rank. I feel like I'm banging my head up against some missing assumption that is built in to everyday set-theoretical discourse... – Adam Jan 20 '10 at 5:01
You don't have to say which $\alpha$. Any one will do, so you can put an existential quantifier in front of it (so long as you know there is one). – François G. Dorais Jan 20 '10 at 5:08
I think the homework exercise is actually "prove that for any set x, TC(x) exists"; start from the textbook proof (from regularity) that $(\forall x\exists\alpha)x\in V\alpha$, show by transfinite induction that for every ordinal $\alpha$, the transitive closure of every member of $V_\alpha$ exists, exploiting the fact that each element of $V_{\alpha+1}$ is a subset $V_\alpha$; at limit stages the TC of the union is the union of the transitive closure. So, I can see how to define the "ISTC(x,y)" predicate meaning "x is the transitive closure of y"; that's not what has me confused. – Adam Jan 20 '10 at 5:10
@Adam: just a note, MathWorld makes a bad reference for non-experts; you have to read it very skeptically in general. They have idiosyncratic definitions that don't match the general literature, and other strange things. Two examples from the article you linked. (1) Their definitions don't include (∀ x)(y=y) as a well formed formula. (2) Their use of the word "closest" is confusing at best, and I would say wrong. Consider (∀ x)( (∀ x)(x=x) → x=x) . – Carl Mummert Jun 21 '10 at 11:42

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.

-
Wow, absolutely magnificent. Thank you for (1) stating with total clarity the question I was having such trouble formulating and (2) answering it in a completely satisfying and general manner. – Adam Jan 21 '10 at 18:46
Thanks for the kind remark! I'm glad to hear that you found the answer helpful. – Joel David Hamkins Jan 21 '10 at 19:00
Thanks, François, for fixing this error from long ago; and I apologize for the misspelling. – Joel David Hamkins Mar 16 '13 at 20:41

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.

-
Although "turning recursive definitions into explicit definitions may not be possible" is true, a very broad class of recursive definitions can be made explicit. Specifically, if $F$ is defined recursively by $F(x)=G(x,F\upharpoonright H(x))$ where $G$ and $H$ are definable in ZFC and where $H$ is well-founded (in the sense that every nonempty set $u$ has an element $x$ with $H(x)\cap u=\varnothing$), then $F$ admits an explicit definition in ZFC. In particular, recursions over (von Neumann) ordinals can be made explicit. [Continued in next comment] – Andreas Blass Mar 17 '13 at 0:42
That covers, in particular, the definition of $V_\alpha$ and the definition if iterated unions that leads (as in Joel's answer) to $TC$. Once one has $TC$, it can serve as the $H$ for definitions by $\in$-recursion. [Technical note: By using a definable function $H$ instead of a "predecessor" relation, I've built in the assumption that $H(x)$ is always a set, which otherwise would have to be added. Also, if $G$ and $H$ are $\Delta_1^{ZF}$-definable, then so is $F$; $\Delta_1^{ZF}$-definability cannot be replaced here with $\Delta_1^{ZF}$-definability of the predecessor relation.] – Andreas Blass Mar 17 '13 at 0:48

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$).

-
In the usual definitions, a variable is a term. I think you mean that the signature has no function symbols (no "term-forming operations"). – Carl Mummert Jun 21 '10 at 11:05
You're absolutely right. – Mike Shulman Jun 22 '10 at 3:24
Thanks for editing that, I like this explanation. – Carl Mummert Jun 25 '10 at 13:50

(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.

-
Thanks, but if I write a big expression involving "TC(x)", I cannot simply replace the "TC(x)" with what you have provided (which is otherwise perfectly accurate!) -- the result will not be a legitimate formula. In fact, what you write is the "$\phi$" mentioned in my question above -- it is the predicate which expresses the fact that its argument is the transitive closure of $x$. – Adam Jan 20 '10 at 3:28
Then what do you need? Something like existsunique w forallz,y (y in x) implies (y in w) and (y in w) and (z in y) implies (z in w) ? I could expand out exists unique if you like, and continue adding clauses, but I thought you would do that. Or am I misremembering, and Kunen does not have a first order expression? – Gerhard Paseman Jan 20 '10 at 3:36
Your statement $x = TC(x)$ (and the pseudoformula accompanying it) only says "$x$ is transitive." Adam wants to prove the existence of the transitive closure of set $x$, not a criterion for when $x$ is transitive. – François G. Dorais Jan 20 '10 at 4:50
OK. Am I misremembering what Kunen has? I won't attempt the exact syntax, but is there not a first order predicate something like the unique w such that w is transitive and x subset of w and for any y which is transitive and for which x subset y, we have w subset y? Or am I still missing something? – Gerhard Paseman Jan 20 '10 at 8:04