Language: first order logic with equality and its axiom and additionally the extra-logical primitives: $ ``\tau, < , \in"$, the first is a total unary function denoting is the type of, the rest are binary relations denoting, is lower than and set membership respectively.


Extensionality: $\forall z (z \in x \Leftrightarrow z \in y) \to x=y$

Define: $t \text{ is a type} \equiv_{df} \exists x: t=\tau(x)$

Well ordering: $< \text {is a well-order on types } $

Idempotence: $\tau(\tau(x))=\tau(x)$

Infinity: $ \exists t: \lim^< t$

Atomicity: $\forall \text{type } t: \forall y \, (y \in t \iff y=t)$

Typed Comprehension: $\forall t \, \exists x \, \forall y \, (y \in x \iff \tau(y) < t \land \phi)$

Typing: $ \neg (x \text { is a type}) \to \tau(x)= \min t: \forall y \in x ( t > \tau(y))$

Inaccessibility: if $f$ is a definable function, then:

$ \forall x : \neg \, \forall \text{type } t \, \exists y \, \in x \, (t \leq f(y))$

Where: $a \leq b \equiv_{df} a < b \lor a=b$.

Note: the expression $``< \text{ is a well order on types}"$ is the following axioms:

$\begin{align} \forall x \forall y \, (& x < y \to x,y \text { are types } \\& x \not < x \\ & x < y < z \to x < z \\ & x,y \text { are types} \land x \neq y \iff x < y \lor y < x )\end{align}\\ \exists \, \text{type } x (\phi(x)) \to \exists \, \text {type } x: \phi(x) \land \neg \exists y \, (\phi(y) \land y < x) $

the expression $``\lim^< t"$ is:

$\exists a (a < t) \land \forall a < t \exists b < t \, (a < b)$

the expressions $``\forall \text{type } x ..; \exists \text { type } x .."$ stands for $ \forall x \, (x \text{ is a type } \to ..)$ and $\exists x \, (x \text{ is a type } \land .. )$ respectively.

Now is ZFC interpretable in this theory?

  • $\begingroup$ Everything seems to allow for an interpretation of "types" as ordinals -- except for Atomicity, which I would expect to say $(y\in t \iff y < t)$ [$<$ not $=$]. $\endgroup$
    – BrianO
    Apr 25, 2021 at 9:36
  • $\begingroup$ @BrianO, if I follow you correctly then you would by then interpret $\tau$ as the rank function on sets, that is $\tau(x)=\alpha$ is interpreted as $rank(x)=\alpha$. My philosophical belief is that Types are not sets, that's why I prefer to axiomatize them as extensional Ur-elements $\endgroup$
    – Zuhair
    Apr 25, 2021 at 10:34
  • $\begingroup$ That was the other interpretation it seems the axioms offer. Is the logic one-sorted or two-sorted? If you want types to not be sets, I'd think 2-sorted. If not, then the variable $y$ in Atomicity ranges over both sets and types, and it follows that $t\in t$ for every type $t$. $\endgroup$
    – BrianO
    Apr 25, 2021 at 18:05
  • $\begingroup$ @BrianO, it's mono-sorted. Yes, we do have $t \in t$ for every type $t$ still that doesn't make it a set, even though it is extensional, and even though it is an "element" of itself; the reason is because its identity is dependent only on a relationship with itself, so to me this is not a set. Of course we can use two sorts, but I just want to make matters easiers this way. $\endgroup$
    – Zuhair
    Apr 25, 2021 at 20:10

1 Answer 1


I think the answer is to the positive. I was just wondering if Replacement can follow from inaccessibility of types, which happens to be the case! A point that I didn't see clearly at the begining. This shows that naive conception about types with sets constructed thereof is a strong notion! Since it can easily interpret set theory.

The proof is actually almost straighforward.

Lemma: there is no maximal type:

$\not \exists t^{max}: \forall \text{type } t \, (t < t^{max})$

Proof: suppose there is a maximal type $t^{max}$. Define the fixed function $f(y)=t^{max}$. Now take any set $x$ such that $y \in x$ and we'll have every type $t \leq f(y)$; contradicting Inaccessibility.

The proof of Replacement: for any definable function $f$ (not using symbol $B$) for any set $A$, there exists a set $B$ that is a set image of $A$ under $f$.

Proof: Define the function $i$ from $A$ as $i(x)=\tau(f(x))$ for each $x \in A$, so $i$ is the restriction of the composition $\tau \circ f$ to $A$. Now assume that for every type $t$ there exists some $i(x)$ for an $x \in A$ such that $t \leq i(x)$; by then we'd violate Inaccessibility. So there must exist a type $t$ that is strictly higher than the type of every $f(x)$ when $x \in A$, use this type in Typed Comprehension, and construct the set image of $A$ under $f$.

The proofs of Power and Set Union are straighforward also, since simply we take a type $t > \tau(x)$ and simply we can construct $P(x)$ and $\bigcup(x)$ by substituting this type in Typed comprehension with the relevant formulas.

The proof of Infinity is easy also, take $t$ in Typed comprehension to be the first limit type, and we can easily construct the set of all naturals. We can easily prove that no natural can have an infinite type, since otherwhise the types of all naturals with infinite types would constitute a descending type chain! Thus violating the Well Ordering schema.

So all axioms of $\sf ZF \text{ - Reg.} $ are proved in this theory, so clearly this theory would interpret $\sf ZFC$.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .