I am trying to solve a logic question from the Ebbinghaus book "Mathematical Logic".
Let $\mathcal{L}^{w}_{II}$ be the system corresponding to Weak Second-Order Logic, where quantification is only allowed over finite sets (and relations). $\mathcal{L}_{\omega_1 \omega}$ is first-order logic equipped with infinite disjunction.
Question 2.7 of Chapter IX - Extension of First-Order Logic says:
Show that for every $\mathcal{L}^{w}_{II}$-sentence $\phi$ there is an $\mathcal{L}_{\omega_1 \omega}$-sentence $\psi$ with the same models (that is, for all $S$-structures $\mathcal{A}$, $\mathcal{A} \vDash_{w} \phi$ iff $\mathcal{A} \vDash \psi$. Conclude from this that the Löwenheim-Skolem Theorem holds for $\mathcal{L}^{w}_{II}$.
Initially, I thought about doing a proof by induction on the structure of the sentence $\phi$ and remembered that this may be problematic: for instance, if $\phi := \exists x \phi'$, then $\phi$ is a sentence, but $\phi'$ may not be a sentence, thus blocking us from using the inductive hypothesis. My next attempt was to try to generalize the hypothesis for arbitrary formulas, but I don't know how to do that in this specific case: it appears to me that an assignment in $\mathcal{L}^{w}_{II}$ assigns standard variables AND relation variables, while an assignment in $\mathcal{L}_{\omega_1 \omega}$ just assigns standard variables.
How do I use induction in this case?
For the inductive step, I believe the difficulty of the problem is in the case where we want to express:
$\mathcal{I} \vDash_{w} \exists X^n \phi$ $\quad$ :iff there is a finite $C \subset A^n$ such that $\mathcal{I} \frac{C}{X^n} \vDash \phi$
using an infinite disjunction. I believe this can be done as:
C is finite $\iff$ C has one element $\lor$ C has two elements $\lor$ $\ldots$ $\lor$ C has $n$ elements $\lor \ldots$
Is this the correct path to take?
Thanks in advance.
You're right that you want to prove this by induction over arbitrary formulas, and you're right that free second order variables cause a problem.
So instead let's prove by induction on the number of second-order quantifiers that for every $\mathcal{L}^w_{II}$-formula $\varphi(x_1,\dots,x_n)$ with no free second-order variables, there is an equivalent $\mathcal{L}_{\omega_1,\omega}$-formula $\varphi'(x_1,\dots,x_n)$. Here equivalent means that $M\models \varphi(a_1,\dots,a_n)$ if and only if $M\models \varphi'(a_1,\dots,a_n)$ for every $S$-structure $M$ and every tuple $(a_1,\dots,a_n)\in M^n$.
The first-order formula building operations can be handled trivially, since $\mathcal{L}_{\omega_1,\omega}$ is also closed under these operations. So it suffices to consider the case of $\exists X\, \varphi(X,y_1,\dots,y_m)$, where $X$ is an $n$-ary relation variable. We can't apply induction to $\varphi(X,y_1,\dots,y_m)$ directly, since it has a free relation variable, so we have to rewrite our formula first. Here's were we can use your idea about cardinality.
We want to take a disjunction over all the possible sizes of $X$. For each size $k$ of $X$, we can replace $\exists X$ by $\exists \overline{x}_1\dots\exists \overline{x}_k$, where each $\overline{x}_i = (x_{i,1},\dots,x_{i,n})$ is an $n$-tuple of variables. Then we can go into the formula and look for atomic instances of $X$. Everywhere we see $X(t_1,\dots,t_n)$, we can replace this atomic formula by $\bigvee_{i=1}^k \overline{t} = \overline{x}_i$, by which I mean $$\bigvee_{i=1}^k \bigwedge_{j = 1}^n (t_j = x_{i,j}).$$ Altogether, we have $$\exists X\, \varphi(X,y_1,\dots,y_m) \iff \bigvee_{k\in \omega} \exists \overline{x_1}\dots\exists \overline{x_k}\, \varphi\left(\bigvee_{i=1}^k \overline{z} = \overline{x}_i,y_1,\dots,y_m\right)$$ Now each disjunct in this infinite disjunction is a $\mathcal{L}^w_{II}$-formula with no free second order variables and one less second-order quantifier, so we can apply the inductive hypothesis to each disjunct, and we're done.