Return to Question

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 letters 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$?

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$?

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 : \forall Y \in V_\theta ( [V_\theta \models \varphi(X,\alpha)] \iff Y=X).$

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

Note: all letters 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 that 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$?

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 letters 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$?

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 : \forall Y \in V_\theta ( [V_\theta \models \varphi(X,\alpha)] \iff Y=X).$

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

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

I'd label that 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$?

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 : \forall Y \in V_\theta ( [V_\theta \models \varphi(X,\alpha)] \iff Y=X).$

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

Note: all letters 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 that 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$?