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.
Best Answer
Here's a partial answer showing that your question consistently has a negative answer (and Andreas Lietz showed the consistency of the opposite):
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:
(In fact since the $L$-ordering is appropriately absolute we don't need $X$ to be minimal here, but it makes the picture nicer.)
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.