MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

## Formulaic definitions

In Jech's Set Theory, p. 194, I read - as a comment on the definition of ordinal-definable sets ("A set X is ordinal-definable if there is a formula such that [...]") -:

It is not immediate clear that the property "ordinal-definable" is expressible in the language of set theory.

Just to show that there is an equivalent definition that is.

a) Cannot every formulaic definition be translated into a set theoretic one by gödelization?

b) If gödelization is not what Jech means: Are there "working" formulaic definitions (working = used in practice) that cannot be translated into a set set theoretic one?

-

Definability is a slippery concept (see this previous MO answer), and the subtle fact here is that although the class of ordinal-definable sets is definable, in general we have no way to define the class of definable sets.

The answer to your questions (a) and (b) is to realize that the crucial difference is whether you have just one formula, which is no problem, or whether you intend to quantify over all formulas, which is where the problems arise.

For any given fixed formula $\varphi$, of course, the class $\{\ x\ \mid\ \varphi(x)\ \}$ is definable, since it is the formula $\varphi$ that defines it. Thus, the notion of "being defined by the formula $\varphi$" is a first-order expressible property of $x$ in a direct way, and this is probably what you are thinking.

But the class of hereditarily ordinal definable sets wants to include the sets that are definable from ordinal parameters using any formula, not just one fixed formula. In this case, it turns out that one may not easily generalize the direct approach above. Indeed, the collection $\{\ \langle x,{\ulcorner}\varphi{\urcorner}\rangle\ \mid\ \varphi(x)\ \}$ is never a definable class in any model of set theory. This fact is known as Tarski's theorem on the non-definability of truth. There is an easy proof using the Gödel fixed point lemma: if truth were definable, then we could make a sentence asserting its own non-truth, and this is self-contradictory.

One way to think about it is that as $\varphi$ increases in complexity, the assertion that $\varphi(x)$ holds of a set $x$ becomes increasingly complex. If we had a single formula that could assert "$\varphi(x)$ is true," then this formulas would have some fixed complexity, and the complexity hierarchy would collapse. But we can prove that the complexity hierarchy is strict, and so there can be no such formula defining truth.

Meanwhile, for a fixed set $M$, we may define the class $\{\ \langle x,{\ulcorner}\varphi{\urcorner}\rangle\ \mid\ M\models\varphi(x)\ \}$, since satisfaction in a set is defined by induction on formulas. It is a curious situation that Tarski is credited both with defining truth (by this inductive definition) and with proving that truth is not definable (in the non-definability of truth theorem above). Note that when $M$ is a fixed set, the complexity of saying $M\models\varphi(x)$ is merely $\Delta_0(x)$, since all quantifiers have been bounded by the set $M$, or if one thinks of $\varphi$ varying, then it is $\Delta_1(x,{\ulcorner}\varphi{\urcorner})$, since one must quantify to get access to the satisfaction-in-$M$ relation. (Note that in non-standard models, the inductive definition applies to non-standard $\varphi$.)

The observation of the previous paragraph is the key to showing that HOD is a definable class, since if $x$ is definable in $V$ by a formula with ordinal parameters, then by the reflection theorem it is definable in some large $V_\alpha$ by the same definition, and so

• $\text{HOD}=\{\ x \ \mid\ \exists \alpha\ x\text{ is definable in }V_\alpha\ \}$

Perhaps this way of thinking about HOD accords a little better with the way you want to think about HOD.

-
 @Joel, thanks for the elucidating answer! Could you please be a bit more specific with regard to "as $\phi$ increases in complexity, the assertion that $\phi(x)$ holds of a set $x$ becomes increasingly complex". Do you mean that the complexity of "$\phi(x)$ holds for $x$" must be greater than that of $\phi(x)$? – Hans Stricker May 23 2011 at 6:33 No, I just mean that the complexity of saying "$\varphi$ holds of $x$" has the same complexity as $\varphi$. So if you think of this as an assertion about $x$ and about ${\ulcorner}\varphi{\urcorner}$, then we should expect it to be more complex than any one formula. And indeed, this is why it is not expressible. – Joel David Hamkins May 23 2011 at 15:24

a) Yes. For example, "definable" cannot be translated into a set theoretic definition.

b) Yes, see (a).

-
 "definable" = there exists a set which is the gödel number of a formula $\phi$ such that $X = \lbrace x\ |\ \phi(x)\rbrace$? – Hans Stricker May 21 2011 at 8:10 Now you would need to define $\{x\; |\; \phi(x)\}$. – Ricky Demer May 21 2011 at 8:35 I believed that's an unproblematic abbreviation: $\Phi(\lbrace x\ |\ \phi(x)\rbrace)$ abbreviates $(\exists ! X) \Phi(X) \wedge (x)\ x \in X \equiv \phi(x)$ – Hans Stricker May 21 2011 at 10:48 Are there supposed to be parentheses around everything after $(\exists ! X)$? In either case, that only defines $\Phi(\{x\; |\; \phi(x)\})$, not $\{x\; |\; \phi(x)\}$. – Ricky Demer May 21 2011 at 18:10 Why isn't my definition enough? Where else would you want to use the term $\lbrace x | \phi(x)\rbrace$ than in a formula? – Hans Stricker May 23 2011 at 6:54
show 1 more comment