Can we have ZF + Definability + True Foundation + True Finiteness? Can it be Categorical?

Question

Lets extend $\mathcal L_{\omega_1, \omega_1}$ with axioms of equality and of:

$\sf ZF + Definability+Ture$-$\sf Foundation+True$-$\sf Finiteness $

Where $\sf ZF$ is written, as usual, in $\mathcal L_{\omega, \omega}$

$\sf Definability$ axiom is written in $\mathcal L_{\omega_1, \omega}$ as:

$\textbf{Define: } Dx \iff \bigvee x= \{ y \mid \Phi \}$

where $\Phi$ range over all formulas in $\mathcal L_{\omega, \omega}$ in which only the symbol "$y$" occurs free, and the symbol "$y$" never occurs bound.

${\sf Definability\!: } \ \forall x Dx$

$\sf True$-$\sf Foundation$ axiom is written in $\mathcal L_{\omega_1, \omega_1}$ as:

$ (\forall v_n)_{n \in \omega} \, \exists x: \bigvee_{n \in \omega} (x=v_n) \land \bigwedge_{n \in \omega} (v_n \not \in x)$

and $\sf True$-$\sf Finiteness$ axiom written in $\mathcal L_{\omega_1, \omega}$ as:

$\operatorname {finite}(x) \iff \\ \bigvee_{n \in w} [\exists v_0,.., \exists v_n : x=\{y \mid y \neq y \lor \bigvee_{i \in n } ( y = v_i)\}]$

Where $\operatorname {finite}(x)$ is defined in $\mathcal L_{\omega,\omega}$, as usual, by $x$ having a bijection with an initial set of naturals, i.e. naturals closed under predecessor relation.

Now, this should be arithmetically complete, since it captures the standard model of arithmetic, also it captures the set $\sf HF$ of all standard hereditarily finite sets.

Is this theory consistent?

Is this theory complete?

Is this theory categorical?

Answer 1

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. Really, given your questions I strongly recommend reading that paper carefully, I think it will clarify many things!)