If we coin a theory in $\mathcal L\_{\omega\_1, \omega}$ that begins with constructing pure true well founded finite sets, then the set of all true well founded hereditarily finite sets, then builds up stages of $L$ on top of it using the infinitary machinery (depicted below), then restrict iteration to be secured only below the first weakly inaccessible cardinal. Then would there be finitary first order sentences that this theory cannot decide upon?


Language $\mathcal L(=,\in)\_{\omega\_1, \omega}$.


$\textbf{Extensionality: } \forall z (z \in x \leftrightarrow z \in y) \to x=y$


$\textbf{Empty: } \exists x \forall y (y \not \in x)$


$\textbf{Define: } x=\varnothing \iff \forall y (y \not \in x)$


$\textbf{Finite construction: } \bigwedge\_{n \in \omega} \forall v\_0..\forall v\_n \exists x: x=\{v\_0,..,v\_n \} $


Define the finite stages of $L$ as:


$L\_0 = \varnothing$


$L\_{n+1} = \{ x \mid x=\varnothing \lor \bigvee\_{n \in \omega} (\exists v\_0,..,v\_n \in L\_\alpha: x=\{v\_0,..,v\_n\} ) \} $


Now the first infinite stage is:


$L\_\omega= \{x \mid \bigvee\_{n \in \omega} x \in L\_n\}$


$\textbf{Finite Foundation: } \\ \forall x \in L\_\omega: \neg [ \bigwedge\_{n \in \omega} (\exists v\_0..\exists v\_n: \bigwedge\_{i \in n} (v\_{i+1} \in v\_i) \land v\_0 \in x)]$


Up till now this $L\_\omega$ is the set of all true well founded hereditarily finite sets, its one (up to isomorphism) in all models of this theory. This entails that this theory is *arithmetically complete*.


Now we proceed to build the rest of stages of $L$:


$\textbf{Bounded Separation: } \forall A \exists x: x= \{y \in A \mid \phi^A \} $; where $\phi^A$ is formula bounded by $A$, in which "$x$" doesn't occur, and $y$ is its sole free variable.


$\textbf {Constructible Power: } \forall A \exists B:\\ B=\{x \mid \bigvee x=\{y \in A \mid \Phi^A \}\} $


Where $ \Phi^A$ is all formulas bounded by $A$ having $y$ as their sole free variable.


Now we come to define successor stages:


$\textbf {Define: } L\_{\alpha+1} = \{x \mid \bigvee x= \{y \in L\_\alpha \mid \Phi^{L\_\alpha}(y) \} \} $


Where $ \Phi^{L\_\alpha}(y)$ is all formulas bounded by $L\_\alpha$ having $y$ as their sole free variable.


$\textbf{Replacement: }$ if $f$ is a function from ordinals to ordinals, then: $\forall \lambda \exists x: x=\{y \in L\_{f({\alpha})} \mid \alpha \in \lambda \}$


Now, we come to define limit stages of $L$ as:


$\textbf{Define: } (\not \exists \kappa: \lambda=\kappa+1) \to L\_\lambda= \{y \in L\_\kappa \mid \kappa \in \lambda \}$


$\textbf{Cardinals: } \forall \kappa \exists \lambda: \kappa < \lambda$


Where $<$ is for cardinal strict smaller than.


$\textbf{Size: } \not \exists \kappa: \operatorname {inaccessible}(\kappa)$


Where inaccessible means a regular limit of regular ordinals.


$\textbf {Restriction: } \forall x \exists \alpha: x \in L\_\alpha$


My point is that we've achieved $V=L$ here so all models of this theory are constructible, there are no models of this theory that prove existence of an inaccessible set. So it answers to all large cardinal properties in the negative. We cannot have inner models since $L$ is the minimal inner model. Forcing fails here. Also we have this theory arithmetically complete so we cannot have statements like Godels or Rossers or the alike, also being arithmetically complete it settles all question about consistency of theories since those are arithmetical statements.



> 
> So, does this theory decide on every sentence in $\mathcal L\_{\omega, \omega}$? That is, is it finitary first order complete?
> 
> 
> 



Is this theory finitary first order complete?
Let $\mathbb{K}$ be the class of well-founded models of $\mathsf{ZFC+V=L}$ + "There is no inaccessible cardinal." This is a subclass of the model class of your theory, but under mild hypotheses its associated theory $$Th(\mathbb{K}):=\bigcap\_{\mathfrak{M}\in\mathbb{K}} Th(\mathfrak{M})$$ is not complete. For example, suppose $\kappa$ is inaccessible. Then by by downward Lowenheim-Skolem + condensation, there is a countable $\alpha$ such that $L\_\alpha\models\mathsf{ZFC}$. But since $L\_\alpha\in L\_\kappa$, this means that $L\_\kappa\models$ "$\mathsf{ZFC}$ has a countable transitive model," whereupon by elementarity $L\_\alpha$ satisfies the same. This, plus well-foundedness of the ordinals, gives us lots of non-elementarily-equivalent elements of $\mathbb{K}$: for each $n\in\omega$, let $\alpha\_n$ be the unique ordinal whose corresponding level of $L$ satisfies $\mathsf{ZFC}$ "There are exactly $n$ levels of $L$ satisfying $\mathsf{ZFC}$." (And of course we can do lots more along the same lines.)


* Of course, it takes some work to see that "There are exactly $n$ levels of $L$ satisfying $\mathsf{ZFC}$" can be expressed in the language of set theory. This is however a standard result/technique in set theory which you should definitely spend time mastering if you're interested in this topic. If memory serves, Kunen's book (specifically, the section "Defining definability") gives a good summary of the topic.


Note, though, that - again under mild hypotheses - your theory has more models than just those in $\mathbb{K}$. This is because $\mathcal{L}\_{\infty,\omega}$ cannot capture well-foundedness; in particular, if there are arbitrarily large levels of $L$ satisfying $\mathsf{ZFC}$, then there is a non-well-founded model of $\mathsf{ZFC}$ satisfying every well-foundedness principle $\mathcal{L}\_{\infty,\omega}$ can express.


