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

Question

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<x\to y\in_1C)) \to \\ \exists z(z<x\to z\in_1C \wedge\forall w(w<z\to w\not\in_1C)))$

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

Answer 1

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.