An abstract logic satisfies the LS property for single sentences if each satisfiable sentence has a countable model. Similarly, the LS property for countable sets of sentences holds if every satisfiable countable set has a countable model.

Lindström's first theorem is usually stated in terms of the weaker LS property (for single sentences). This makes the coding of partial isomorphisms, a crucial step in the proof, more complicated. In fact, it is straightforward to codify partial isomorphisms with a countable family of predicates $I_n(\overline{x},\overline{y})$, for $n\geq 1$, and a countable set of sentences asserting that $I_n(\overline{x},\overline{y})$ holds iff the natural matching of the $n$-tuples $\overline{x}$ and $\overline{y}$ of individuals in $U$ and $V$, respectively, preserves the relevant predicates and the back-and-forth property holds:

$\forall\overline{x}\forall\overline{y}(I_n(\overline{x},\overline{y})\rightarrow \forall x(U(x)\rightarrow \exists y I_{n+1}(\overline{x},x,\overline{y},y)))$

and similarly for the "back" part.

Now, this could simplify the proof of Lindström's theorem if we could independently prove that the weaker LS property implies the strongest for an apropriate class of logics. (We know that a compact regular logic satisfying the weaker LS property also satisfies the stronger, because this logic must be equivalent to first-order logic. That would be enough if we could prove this directly, without using Lindström's theorem).

Incidentally, every logic satisfying the LS property for single sentences that I know also satisfies the property for countable sets. What is known about this?