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?
 A: 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.
A: a)  Yes.  For example, "definable" cannot be translated into a set theoretic definition.
b)  Yes, see (a).
