Is bounded-$\mathcal L_{\omega_1,\omega_1}$ significantly different from $\mathcal L_{\omega_1,\omega_1}$?

Question

Take the language $\mathcal L(=,\in)_{\omega_1,\omega_1}$, if we restrict infinite quantification strings, i.e. of the forms $``(\forall v_i)_{i \in \omega}"; ``(\exists v_i)_{i \in \omega}"$, to bounded forms, that is $``\forall v_0 \in x, \forall v_1 \in x,..."$ and $``\exists v_0 \in x , \exists v_1 \in x,..."$ abbreviated as $``(\forall v_i \in x)_{i \in \omega}"; ``(\exists v_i \in x)_{i \in \omega}"$ respectively, or even if we further demand the bound to be a definable constant or the value of a function. Call the resulting language as "bounded-$\mathcal L(=,\in)_{\omega_1, \omega_1}$", and denote it by $\mathcal L(=,\in)_{\omega_1, [\omega_1]}$

How would $\mathcal L(=,\in)_{\omega_1, [\omega_1]}$ differ from $\mathcal L(=,\in)_{\omega_1, \omega_1}$ as regards basic properties of logic like Completeness, Compactness, etc..

As a clear example, if to $\mathcal L(=,\in)_{\omega_1, [\omega_1]}$ we add all axioms of $\sf ZFC$ written, as usual, in the fragment $\mathcal L(=,\in)_{\omega,\omega}$ and suppose we add an axiom of Foundation but in a bounded form, that is:

$\textbf{Foundation: } \\\forall \alpha \, (\forall v_i \in V_\alpha)_{i \in \omega} \, \exists x: \bigvee_{i \in \omega} (x=v_i) \land \bigwedge_{i \in \omega} (v_i \not \in x)$

Would that theory be different from theory written in $\mathcal L(=,\in)_{\omega_1,\omega_1}$, axiomatized by $\sf ZFC$ axioms in $\mathcal L(=,\in)_{\omega,\omega}$ , and Foundation written as above but unbounded.

Answer 1

Your new formulation of foundation is equivalent to the corresponding unbounded form. The reason is that every failing instance of the unbounded formulation will lead to a failing instance of the bounded formulation, since if there is a countable collection of $v_i$ with no $\in$-minimal element, then by the usual ZFC axioms it follows that $v_0$ is in some $V_\alpha$, and so the $v_i$ that appear within this $V_\alpha$ will fall under the bounded form, and an $\in$-minimal for that part of the family will be $\in$-minimal for the whole family since $V_\alpha$ is transitive.