Language: Mono-sorted first order logic with equality and additional primitives of $\xi$ signifying is the order of, and the binary relation $ [ \ ] $ signifying predication that is $P[x]$ to be read as $P$ predicates $x$, or equivalently as $x$ is predicated by $P$. The domain of this theory only range over predicates, which would be called as object predicates. So, this theory is a first order theory speaking about a sort of high order logic. An order of an object predicate in this theory can be as big as any ordinal provable to exist in ZF. Care to be exercised not to confuse $P[x]$ for $P(x)$.
[Note]: If the notation using $[ \ ]$ seems confusing, then one can use an infix dyadic symbol to represent predication by object predicates, I'd suggest "$ \lfloor $", so $P \lfloor x$ would stand for $P$ predicates $x$.
Define: $Q \subseteq P \iff \forall X (Q[X] \to P[X])$
Define: $Q \subsetneq P \iff Q \subseteq P \land P \neq Q$
Define: $\operatorname {preord} (\alpha) \iff \forall \beta \, (\alpha [\beta] \to \beta \subsetneq \alpha \land \forall \gamma \, (\beta[\gamma] \to \gamma \subsetneq \beta))$
In English: $P$ is a preordinal if and only if its a properly transitive (whatever predicated by it is a proper subpredicate of it) predicate predicating properly transitive predicates.
Define: $\operatorname {ext}(\alpha) \iff \forall \gamma \, (\gamma \equiv \alpha \to \gamma = \alpha)$
Where $\equiv$ is the co-predication relation, that is predicating the same objects.
Define: $\operatorname {ord}(\alpha) \iff \operatorname {preord}(\alpha) \land \operatorname {ext}(\alpha)$
Define: $\alpha < \beta \iff \operatorname {ord} (\alpha) \land \operatorname {ord}(\beta) \land \beta [ \alpha]$
Axioms:
Orders: $\forall P \exists \alpha: \operatorname {ord} (\alpha) \land \xi(P) =\alpha$
Comprehension: $\forall \alpha: \operatorname {ord} (\alpha) \to \exists P \, \forall q \, (P [q ] \leftrightarrow \xi (q) \leq \ \alpha \land \psi)$
Ordering: $\xi (P) = \min \alpha: \forall q \,( P [q] \to \xi (q) < \alpha)$
Inaccessibility:$\neg \,\exists P: \forall \alpha \, ( \operatorname {ord} (\alpha) \to \exists q \, (P [q ]\land f(q)\geq \alpha)) $
Infinity: $\exists \operatorname {ord} \lambda > \varnothing: \forall \alpha < \lambda \, \exists \beta \, ( \alpha < \beta < \lambda)$
One can easily add axioms of Extensionality, and Choice. By then we can interpret $\in$ membreship relation of set theory as $$ x \in y \iff y[x]$$, and this would provide a direct interpretation of ZFC.
The theory with just the above five axioms would also interpret ZFC over some subdomain of it but over another membership and equality relations.
Since the primitives of this theory are about ordered predication, then this theory is in some sense a theory about LOGIC. So, the above establishes that ZFC would be interpretable in a theory about logic, somewhat supporting the program of logicism in philosophy of mathematics.
Is this theory (+ Extensionality, + Choice) bi-interpretable with ZFC?
