# Does this logic have the downward Skolem-Löwenheim theorem?

Let $\mathcal L_Q$ denote the logic obtained from adding the quantifier $\newcommand{\almost}{\forall^\infty}\almost$ to the usual first-order logic, where the semantic interpretation of $\almost x\varphi$ is "All but finitely many $x$ satisfy $\varphi$", or formally: $$M\models\almost x\varphi(x)\iff\Big|\{m\in M\mid M\not\models\varphi[m]\}\Big|\text{ is finite}.$$

It's not very hard to show that this logic is not compact$^*$, and does not satisfy the upward Skolem-Löwenheim theorem (e.g. the order $(\Bbb N,\leq)$ has a categorical axiomatization). But what about its downward counterpart?

According to Lindström theorem either compactness fails, or the downward Skolem-Löwenheim theorem should fail. One fails, what about the other?

(*) Please don't discuss the failure of the compactness theorem for $\mathcal L_Q$ here before June 17th, 2013. I gave that part as a homework assignment to my students - some of whom are reading this site.

I think the following idea should give a proof of the downward Löwenheim-Skolem theorem for this logic, but I haven't checked it carefully, so I apologize if it contains a stupid mistake. Suppose I have an uncountable structure $\mathfrak A$ for a countable language and I want a countable substructure that is elementary with respect to your logic $\mathcal L_Q$. For each $\mathcal L_Q$-formula $\phi(\vec x)$ where $\vec x$ represents a sequence of free variables, create a new predicate symbol $P_\phi$ with arity equal to the length of $\vec x$, and let $\mathfrak A^+$ be the expansion of $\mathfrak A$ to the enlarged language, obtained by interpreting $P_\phi$ as synonymous with $\phi$. Note that the enlarged language is still countable, so $\mathfrak A^+$ has a countable elementary substructure $\mathfrak B^+$, where "elementary" means in the usual sense of just first-order logic. Now it seems to me that the reduct of $\mathfrak B^+$ to the original language serves as an $\mathcal L_Q$-elementary substructure of the original $\mathfrak A$. The point is that any specific use of $\forall^\infty$ amounts to first-order information. More precisely, suppose $\phi(x)$ is $(\forall^\infty y)\,\psi(x,y)$. Then whenever $\phi$ holds in $\mathfrak A$ of a particular element $a$, the number of values for $y$ that don't satisfy $\psi(a,y)$ is a specific finite number, and it is expressible in first-order logic in $\mathfrak A^+$ that the number of values of $y$ violating $P_\psi(a,y)$ is this specific number. So that information remains true in $\mathfrak B^+$. Similarly, if $\phi(a)$ fails in $\mathfrak A$, then for every natural number $n$ it is true in $\mathfrak A^+$ that there are more than $n$ values of $y$ violating $P_\psi(a,y)$; this is, for each $n$, first-order information and therefore still true in $\mathfrak B^+$. These observations should yield an inductive proof that the interpretations in $\mathfrak B^+$ of all the new $P_\phi$ predicates agree with the corresponding $\mathcal L_Q$-formulas $\phi$, just as in $\mathfrak A^+$. And that should imply that $\mathfrak B$ is an $\mathcal L_Q$-elementary submodel of $\mathfrak A$.

Another way to approach this is to mimic the proof of downward Löwenheim-Skolem theorem for first order logic. Note that adding $\forall^\infty$ quantifier is the same as adding $\exists^\infty$ quantifier that says that there exist infinitely many solutions. Indeed we have $\forall^\infty x \phi(x) \leftrightarrow \lnot \exists^\infty \lnot \phi(x)$. I find $\exists^\infty$ quantifier easier to work with.

Tarksi-Vaught test can now be reformulated as follows: $A \preceq_{L_Q} B$ iff for any formula $\phi(\bar x, \bar y)$ and $\bar a \in A$ the following two conditions hold

• if $\{b \in B : B \models \phi(\bar a, b)\} \neq \emptyset$, then $\{b \in A : B \models \phi(\bar a, b)\} \neq \emptyset$;
• if $\{b \in B : B \models \phi(\bar a, b)\}$ is infinite, then $\{b \in A : B \models \phi(\bar a, b)\}$ is infinite.

Now given a structure $B$ and $A \subseteq B$, we know how to get an $L_Q$-elementary substructure of $B$ containing $A$: we just need to add witnesses to quantifiers. So construct a chain of length $\omega$ $$A = A_0 \subseteq A_1 \subseteq A_2 \subseteq ...$$ where $A_i \subseteq B$ and $|A_i| = |A_0| + \aleph_0$ as follows. Let $A_i$ be given. Construct $A_{i+1}$ by adding to $A_i$ the following. For every formula $\phi(\bar x, y)$ and $\bar a \in A_i$, let $Z_{\phi, \bar a} = \{b \in B : B \models \phi(\bar a, b)\}$. If $Z_{\phi, \bar a}$ is finite, then add it to $A_{i+1}$, otherwise add a countable subset of $Z_{\phi, \bar a}$ to $A_{i+1}$.

Then take $C = \cup_{i \in \omega} A_i$. Now $|C| = |A| + \aleph_0$ and by Tarski-Vaught test $C \preceq_{L_Q} B$.

There's a cute nuke which works here:

Given a structure $$\mathfrak{A}$$ of arbitrary cardinality in a language $$\Sigma$$, fix $$\theta$$ large enough that $$\Sigma,\mathfrak{A}\in H_\theta$$ and $$H_\theta$$ satisfies "enough set theory." Now by downward Lowenheim-Skolem for first-order logic, let $$M$$ be an elementary submodel of $$H_\theta$$ with $$\mathfrak{A},\Sigma\in M$$, $$\Sigma\subseteq M$$, and $$\vert M\vert=\aleph_0+\vert\Sigma\vert$$. Set $$\mathfrak{B}=\mathfrak{A}\cap M$$; since finiteness is absolute to $$M$$, it's not hard to show that $$\mathfrak{B}\preccurlyeq_{\mathsf{FOL\forall^\infty}}\mathfrak{A}$$ as desired.

And of course this functions as a general recipe for proving appropriate downward Lowenheim-Skolem properties for "concrete" logics.