2
$\begingroup$

In my search for some type-set motivated line of thought that might prove axiom of choice, I was thinking of a concept that looks like $\sf V=HOD$, but in terms of types instead of ordinals, that is we think informally along the following lines:

$X \text{ is type definable } \iff \\ \exists \alpha_1,.., \exists \alpha_n \exists \phi : \forall y (y \in X \iff \phi(y,\alpha_1,..,\alpha_n))$

However, this is known not to be done in first order logic since it involves quantification over all formulas. So, I'll resort to the alterantive approach, which I'll write, paralleling comments by Hamkins, as:

Type-Definability: $\forall X \, \exists \theta \, \exists \alpha < \theta \, \exists \varphi : X=\{y \in V_\theta\mid V_\theta\models\varphi(y,\alpha)\}$

Where $V_\theta$ is the set of all sets of type $< \theta$

Note: all term symbols in Greek denote types as explained in the linked posting on type-set theory.

We'd label that by "type-definable" even though this term had been used in other contexts.

I'd label the above axiom as: $\sf V=HTD$.

That is, all sets are Hereditarily Type-Definable.

Is this formalisable in the language of Type-Set Theory?

Would adding it to axioms of Type-Set Theory prove Axiom of Choice?

How this would relate to $\sf V=HOD$? Would adding it over the aformentioned Type-Set theory have the same consequences as adding $\sf V=HOD$ over $\sf ZF$?

Improve this question
$\endgroup$
10
  • 1
    $\begingroup$ "Type-definable" has a standard (and totally different) meaning in model theory, so I would recommend choosing different terminology. $\endgroup$
    – Alex Kruckman
    Commented May 1, 2021 at 15:17
  • $\begingroup$ @Alex Kruckman, hmmm..., but this is so legitamate here that it's very hard to deviate from? It is at the heart of the matter! One needs to be cautious not to confuse both, the contexts are different. $\endgroup$
    – Zuhair Al-Johar
    Commented May 1, 2021 at 15:29
  • 3
    $\begingroup$ Your definition seems to use a truth predicate. This is not how we define HOD. It is a motivating idea, but that idea (because it uses a truth predicate) is not formalizable in ZFC. Rather, the definition of HOD employs reflection and the definability of the $V_\alpha$ sets. $\endgroup$
    – Joel David Hamkins
    Commented May 1, 2021 at 16:17
  • 2
    $\begingroup$ In ZFC, the statement V=HOD can be expressed by saying: for every set x, there is an ordinal $\theta$ and an ordinal $\alpha<\theta$ and a formula $\varphi$ such that $x$ is the unique object in $V_\theta$ for which $V_\theta\models\varphi(x,\alpha)$. This does not use a truth predicate in $V$, but only in $V_\theta$, which we can prove exists in ZFC. The proof that this agrees with the external idea of definable in $V$ with ordinal parameters, however, is quite subtle. $\endgroup$
    – Joel David Hamkins
    Commented May 1, 2021 at 16:39
  • 1
    $\begingroup$ You could alternatively (equivalently) say: V=HOD iff for every $x$ there is $\theta$ and $\alpha<\theta$ and $\varphi$ such that $x=\{a\in V_\theta\mid V_\theta\models\varphi(a,\alpha)\}$. $\endgroup$
    – Joel David Hamkins
    Commented May 1, 2021 at 17:21

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .