# Is the class of all hereditarily transitive definable sets a model of ZFC?

Is it the case that every transitive definable set is also ordinal definable?

Formal definition of the former would be:

$$TD^M=\{u\in M: \exists \tau_1,...,\tau_n\in Trs^M, \varphi\in Formula (M\models\forall x(\varphi(x,\tau_1,...,\tau_n)\leftrightarrow x=u))\}$$

A element $$u$$ of $$M$$ is transitive definable in $$M$$ iff $$u \in TD^M$$

where $$TD^M$$ is the class of all transitive definable sets in $$M$$. $$Trs^M$$ is the class of all transitive sets in $$M$$.

IF the answer to the above question is to the negative, then is the class of all hereditarily transitive definable sets a model of ZFC?

To see why, note that $$x$$ is the unique maximal element of $$\operatorname{tcl}(\{x\})$$. Therefore the formula $$\varphi(x,p)$$ defined as $$x\in p\land\forall y(y\in p\to y=x\lor\exists z(z\in p\land y\in z))$$ defines $$x$$ with the parameter $$\operatorname{tcl}(\{x\})$$. The formula simply states that $$x$$ is the unique element of $$p$$ which is not an element of any other member of $$p$$, which is easily the case if we use the right parameter.
So the class you define is just $$V$$ itself, even if choice is not assumed.
• I understand the argument, but I don't understand the formula. I think your formula must be $x \in p \wedge \not \exists y (y \in p \wedge x \in y)$ – Zuhair May 21 at 4:56