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?