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.
 A: 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$.
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$.
A: 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.
