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?
> 
> 
> 



Can we have ZF + Definability + True Foundation + True Finiteness? Can it be Categorical?
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](https://arxiv.org/pdf/1105.4597.pdf) for more on this. Really, given your questions I strongly recommend reading that paper carefully, I think it will clarify many things!)


