What features of a logic make possible the proof of Downward Lowenheim-Skolem?

The Downward Lowenheim-Skolem Theorem asserts that if a countable first-order theory has an infinite model, then it has a countable model.

Although associated with first-order logic, the result also applies to second-order logic with Henkin semantics, and this is typically explained by the fact that a second-order logic with Henkin semantics behaves identically with a many-sorted first-order logics, and the LS theorem holds in that latter, along with Compactness and Completeness.

My general question is whether it is possible to precisely identify the boundary between logics that allow for proof of downward LST and those that do not. (I suspect that it might come down to the ability to prove the Tarski-Vaught criterion).

My specific question is whether the following theory would have a countable model (as given by a construction similar to the one for downward LST). The theory consists of the axioms of second-order ZFC except with Separation restricted to "definite" subsets. A subset is "definite" if it is defined by a "definite" property as axiomatized in Zermelo 1929a (p. 362 of Collected Works Vol I, Springer 2010) The set of definite propositions is the smallest set containing all "fundamental relations" (A "fundamental relation" is one of the form $a \in b$ or $a = b$) and closed under the operations of negation, conjunction, disjunction, first-order quantification, and second-order quantification.

The axioms of this theory are Extensionality, Pairing, Second-order Separation (modulo the definiteness restriction), Powerset, Union, Foundation, and Second-order Replacement, and Choice.

Here's a partial answer showing that your question consistently has a negative answer (and Andreas Lietz showed the consistency of the opposite):

Under $ZFC+V=L$, your theory does not have any countable models.

Basically, this comes down to the fact that $V=L$ gives us a very nicely definable well-ordering of the reals, and we can leverage that to pin down a specific bijection between $\omega$ and any fixed countable set.

(EDIT: This isn't actually true - as Asaf Karagila commented, you've omitted the axiom of infinity and so $V_\omega$ satisfies your theory. I'm assuming you meant to include it, though. I'm also assuming that by "Powerset" you mean first-order powerset, that is "$\forall x\exists y\forall z(z\in y\leftrightarrow z\subseteq x)$" rather than "$\forall x\exists y\forall A(A\subseteq x\leftrightarrow\exists z(z\in y\wedge z=A))$," admitting the appropriate abbreviations, since second-order powerset trivially requires uncountability.)

First, note that any model of your theory is transitive (this is a good exercise). Now suppose $M$ were a countable model of your theory. Note that we can quantify over countable levels of $L$ in second-order logic over $M$ ("There is a binary relation on $\omega$ coding a structure such that ..."). Since $V=L$ we have that $M\in L_\alpha$ for some countable ordinal $\alpha$, and therefore inside $M$ (in second-order logic) we can talk about the least ordinal $\beta$ such that $L_\beta\models ZFC+V=L$ and there is a structure $N\in L_\beta$ with $L_\beta\models\vert N\vert=\aleph_0$ which is isomorphic to $M$.

Now note that there is in $L_\beta$ an "$L$-least" bijection $b$ between $N$ and $\omega$. The key point now is that such an $N$ is uniquely isomorphic to $M$ since $M$ is transitive, so we can use $b$ to second-orderly define in $M$ a well-ordering of $M$ of ordertype $\omega$ (which is a clear contradiction), roughly as follows:

$x\trianglelefteq y$ iff there is a structure $X$ with domain $\omega$ such that

• $X\models ZFC+V=L$,

• there is some $N\in X$ which is isomorphic to $M$,

• $X$ is minimal with the above two properties, and

• $x$ precedes $y$ in the $L$-ordering according to $X$.

(In fact since the $L$-ordering is appropriately absolute we don't need $X$ to be minimal here, but it makes the picture nicer.)

In fact, the above approach shows that more generally under $ZFC+V=L$ we have that any model of your theory is correct about cardinality (if $\kappa\in M$ is not a cardinal in reality, think about the $L$-least map witnessing that ...). As a consequence, assuming $ZFC+V=L$ we have that any model of your theory is extremely large: roughly speaking, if we can define an ordinal $\alpha$ in a reasonably simple way then any model of your theory must have cardinality $>\aleph_\alpha$.

Of course, this all breaks horribly if we work in an ambient model of ZFC with no nicely-definable well-ordering of the reals, and Lietz's above-mentioned answer shows that there's no getting around that.