# Is the set of ordinals in Double Extension Set Theory really a set?

We got stuck on the definition of ordinals when we built the DEST(Double Extension Set Theory) checker on Cubical Agda and reproduced the theorem in [1].

The following concepts are all taken from [1], which defines the Transitive, Trichotomy, Singleton and Well-found:

• $$\mathrm {Trans}_1(x):=\forall y\in_1x \forall z\in_1 y(z\in_1x)$$

• $$\mathrm {Trichotomy}_1(x):=\forall(y,z)\in_1x ( y\in_1z \vee y=z \vee z\in_1y)$$

• $$S_1(x):=\exists y\forall z(z\in_1y \leftrightarrow z=x)$$

• $$\mathbf{S}_1:= \{x:S_1(x)\}$$

• $$\mathrm {wf}_1(A):= \forall C (\forall x (x \in_1A\wedge x\in_1C\wedge \exists y(y

The problem is in the section "the set of ordinals":

$$\mathbf{ORD}:=\{\alpha: \\ \forall\beta\in_1\alpha(\beta\color{red}{\in_2}\mathbf{S}_1)\wedge \\ \mathrm {Trans}_1(\alpha)\wedge\forall\beta\in_1\alpha(\mathrm {Trans}_1(\beta))\wedge \\ \mathrm {Trichotomy}_1(\alpha)\wedge\mathrm {wf}_1(\alpha)\}$$

The definition of $$\mathbf{ORD}$$ uses two different membership relations and is therefore not a uniform formula. By Axiom Scheme of Comprehension[1], $$\mathbf{ORD}$$ is not a DEST set.

[1]: Holmes, M.R. The Structure of the Ordinals and the Interpretation of ZF in Double Extension Set Theory. Stud Logica 79, 357–372 (2005). https://doi.org/10.1007/s11225-005-3611-x or https://randall-holmes.github.io/Papers/doubleZF2.pdf

• I corrected what seemed to me to be a grammatical issue in the title---I hope that is what you meant. Jan 12 at 21:29

Perhaps I'm misunderstanding something, but it should be the case that $$\beta \in_2 \mathbf{S}_1$$ is equivalent to $$S_1(\beta)$$. Therefore the defining formula of $$\mathbf{ORD}$$ can be written as $$\mathbf{ORD}:=\{\alpha: \forall\beta\in_1\alpha(S_1(\beta))\wedge \mathrm {Trans}_1(\alpha)\wedge \\ \forall\beta\in_1\alpha(\mathrm {Trans}_1(\beta))\wedge \mathrm {Trichotomy}_1(\alpha)\wedge\mathrm {wf}_1(\alpha)\}.$$ Since $$S_1(x)$$ is a uniform formula, this set exists by Axiom 2.8.