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.