Return to Revisions

The models of your theory are exactly the pointwise-definable (with respect to $\mathcal{L}_{\omega,\omega}$ as usual) well-founded models of $\mathsf{ZF}$; incidentally, your true finiteness axiom is unnecessary. Assuming such models exist of course, this means that your theory is consistent and incomplete (hence not categorical), since we can always force over a pointwise-definable well-founded model to get a new pointwise-definable well-founded model with e.g. a different belief about the truth value of $\mathsf{CH}$. (This isn't actually trivial since we need to carefully preserve pointwise-definability, but it is true; see Hamkins/Linetsky/Reitz for more on this.)