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?
Best Answer
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.)
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.