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?

2more comments