One of the most notable features of $ZFC$ is that it builds up sets in recursively defined $V_i$ stages (where $i$ is an ordinal), however the usual formulation of $ZFC$ has infinitely many stages. The rank of a set $X$ is the ordinal index $i$ of the stage $V_i$ where $X$ first appears as a subset of. So in $ZFC$ we can have a set having an infinite rank.

The question is: can we define a theory $T$ in the language of set theory and choice (i.e. choice can be added as a primitive function symbol to the language of set theory) such that $T$ speaks of sets that are built up in stages in generally a similar manner to the buildup of sets in $ZFC$ such that $T$ can interpret $ZFC$ but provided that $T$ has only ** finitely** many stages?

I think that the answer is to the positive, the following is a definition of a theory having only 5 stages and in which all of the $\beth_i$ numbers definable in ZFC are definable in it.

We add to the language of set theory (first order logic with equality and membership) a primitive unary choice function $c$, and stipulate the following axioms:

Identity axioms +

Axiom of Choice: $(\exists y \in X) \implies c(X) \in X$.

Weak Extensionality: non empty sets having the same elements are equal

Base: There exists a set $B$ (for base) of all empty sets

Power: There exists $P(B)$, $PP(B)$, $PPP(B)$; ($P$ signifies power set)

Axiom schema of Separation (as in Zermelo)

Infinity: $N < B$

Accessibility by power: $X \subset B \wedge \exists x \in X \wedge X< B \implies P(X)\backslash B < B$

Accessibility by union:$ X\subset P(B) \wedge X\not\subset B \wedge X < B \wedge \forall Y \in X (Y < B) \implies U(X) < B$

Where $N$ is the set of all natural numbers; $A < B$ is defined as "strictly subnumerous to" in the usual manner using Kuratowski's ordered pairs; $"\backslash"$ signifies: except, and $"U"$ signifies: set union.

A natural number is defined as the choice set of an equivalence class of finite sets of empty sets under equivalence relation bijection, where bijection is defined in the usual manner using Kuratowski ordered pairs; and finite is defined after Dedekind's also using Kuratowski ordered pairs.

Now sets belonging to the first rank are the empty sets, those belonging to the second rank are subsets of $B$ that do not belong to lower ranks, those belonging to the third rank are subsets of $P(B)$ that do not belong to lower ranks, and so on sets belonging to the $i^{th}$ rank are subsets of $P_{i-2}(B)$ that do not belong to lower ranks.

/Theory definition finished.

Now to understand what's going on here, the trick is to code each third rank set that is strictly subnumerous to $B$ down to a second rank set that is equinumreous to it (i.e. to that third rank set), this is done by defining the set of all unordered injections (denoted as injection* defined below) from the rank3 set to $B$, and then take the choice set of those injection*s and take the range of the selected injection* which would be a rank2 set that is equinumerous to the rank3 set, and it stands as its code, we'll denote it by putting ' after the symbol for the rank3 set.

$Define: F \text{ is injective* from A to B } \iff \\ \forall X \in F \exists a \in A,\exists b \in B (X=\{a,b\}) \wedge \\ \forall X \in A \exists! Y \in B (\{X,Y\} \in F) \wedge \\ \forall a,b \in A \forall x \in B (\{a,x\} \in F \wedge \{b,x\} \in F ⟹ a=b)$

$Define: X \text{ is a cardinal } \iff \exists Y (Y \text{ is an equivalence class of "sets of empty sets" under bijection } \wedge X= c(Y))$

$Define: X=|Y| \iff \exists K (\forall Z (Z \in K \iff Z\subset B \wedge ( ( Y \not\subset B \wedge Z \text{ equinumerous to } Y') \lor (Y \subset B \wedge Z \text{ equinumerous to Y }))) \wedge X=c(K))$

$Define: X \text{ is an ordinal } \iff \forall Y \in X (Y \text { is a cardinal }) \wedge (X \text{ is a finite non empty set of natural numbers closed under relation < } \lor (X \text { is infinite } \wedge \forall \text{ natural number } Y (Y \in X) \wedge \forall Y(Y \in X \wedge Y \text { is not a natural number } \implies Y=N \lor \exists Z \in X (Y= |P(Z)\backslash B |)))) $

$ Define: \text{ For every ordinal }X:\\ X+1=\{x| x \in X \lor x=|X|\} \text{ if X is finite }\\ X+1= \{x| x \in X \lor x=|P(U(X))\backslash B|\} \text{ if X is infinite }$

Now for any ordinal $i$ we can define an injection* $S_i$ from $i$, such that for every element $\{j,x\}$ of $S_i$ where $j \in i$ there exists an element $\{j+1, |P(x)\backslash B|\}$ of $S_i$, and such that $\{0,N'\}$ is in $S_i$.

Now we can easily interpret the $\beth_i$ numbers as the cardinality of the set union of the range of $S_i$ (where the range of $S_i$ is the set of all non-ordinal elements of the set union of $S_i$)

Now as long as $i < B$ then $\beth_i < B$, according to the last two axioms.

To show that we can get to $\beth$ fixed points, first we need to define the least ordinal that is equinumerous to $\beth_i$, we call that $Ord(\beth_i)$, then we define a sequence of unordered pairs whose domain (the set of all ordinal elements of its union) is $N$, starting with $\{0,\beth_0\}$ and such that for every $\{j, \beth_i\} $ in it ,we have $\{j+1, \beth_{Ord(\beth_i)}\}$ in it. Now the union of the range of that sequence is the first $\beth$ fixed point $k=\beth_k$. All other $\beth$ fixed points of $ZFC$ are definable here.

Actually $B$ itself is inaccessible, and so it proves the consistency of $ZFC$.