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.
Stefan's original idea is realized in the following observation, which shows that one $\mathbb{Z}$-chain is elementary equivalent to two such chains.
Theorem. The theory of nontrivial cycle-free graphs where every vertex
has degree $2$ is complete.
Proof. All models of uncountable size $\kappa$ consist of
$\kappa$ many $\mathbb{Z}$ chains, and hence are isomorphic. Thus,
the theory is $\kappa$-categorical, and hence complete. QED
Thus, all cycle-free graphs with every vertex of degree
$2$ have the same first order theory. In particular, the graph consisting of one $\mathbb{Z}$-chain is
elementary equivalent to the graph consisting of any number
of such $\mathbb{Z}$ chains. Since the first graph is connected and
the latter are not, it follows that neither connectivity
nor disconnectivity are first-order expressible as theories
in the language of graph theory.
Best Answer
Essentially, yes. An old result of Kleene [1], later strengthened by Craig and Vaught [2], shows that every recursively axiomatizable theory in first-order logic without identity, and every recursively axiomatizable theory in first-order logic with identity that has only infinite models, has a finitely axiomatized conservative extension. See also Mihály Makkai’s review, Richard Zach’s summary, and a related paper by Pakhomov and Visser [3].
Let me stress that the results above apply to the literal definition of conservative extension, i.e., we extend the language of $T$ by additional predicate or function symbols, and we demand that any sentence in the original language is provable in the extension iff it is provable in $T$. If we loosen the definition so as to allow additional sorts, or extension by means of a relative interpretation, then every recursively axiomatizable first-order theory has a finitely axiomatized conservative extension.
But back to the standard definition. I’m assuming logic with identity from now on. What happens for theories that may also have finite models? First, [2] give the following characterization (they call condition 1 “f.a.${}^+$”, and condition 2 “s.f.a.${}^+$”):
Following Dmytro Taranovsky’s comments, we have the following necessary condition (which is actually also mentioned in [2], referring to Scholz’s notion of spectrum instead of NP, which was only defined over a decade later):
Indeed, the truth of a fixed $\Sigma^1_1$ sentence in finite models can be checked in NP.
It is not known if this is a complete characterization: if $T$ is a r.e. theory whose finite models are NP, then $T$ is equivalent to a $\Sigma^1_1$ sentence on infinite models by [1,2], and $T$ is equivalent to a $\Sigma^1_1$ sentence on finite models by Fagin’s theorem, but it is unclear how to combine the two to a single $\Sigma^1_1$ sentence that works for all models. This is mentioned as an open problem in the recent paper [3].
References:
[1] Stephen Cole Kleene: Finite axiomatizability of theories in the predicate calculus using additional predicate symbols, in: Two papers on the predicate calculus. Memoirs of the American Mathematical Society, no. 10, Providence, 1952 (reprinted 1967), pp. 27–68.
[2] William Craig and Robert L. Vaught: Finite axiomatizability using additional predicates, Journal of Symbolic Logic 23 (1958), no. 3, pp. 289–308.
[3] Fedor Pakhomov and Albert Visser, On a question of Krajewski’s, Journal of Symbolic Logic 84 (2019), no. 1, pp. 343–358. arXiv: 1712.01713 [math.LO]