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

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

1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.