Formulaic definitions

2011-05-21T07:23:02Z

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?

Answer by Ricky Demer for Formulaic definitions

2011-05-21T07:48:22Z

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

b) Yes, see (a).

Answer by Joel David Hamkins for Formulaic definitions

2011-05-21T11:18:32Z

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.

Formulaic definitions - MathOverflow

Formulaic definitions

Answer by Ricky Demer for Formulaic definitions

Answer by Joel David Hamkins for Formulaic definitions