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.

• I don't quite understand your specific question. Downward LST for first-order logic is provable in usual ZFC. Or are you asking whether every model of your version of ZFC has a countable elementary (in what sense?) submodel? (Also you probably also want to make the same modification to Replacement as you do to Separation ...) Also, I don't see why the logic for your version of ZFC would be intermediate. If you're allowing your second-order quantifiers to quantify over all subsets of a model, then its the full semantics; the fact that the elements of the first-order part are sets is irrelevant. Jan 7, 2019 at 16:53
• The general question is totally reasonable (if a bit imprecise). But the specific question doesn't make any sense. "All axioms of second-order ZFC except..." is not a logic, it is a theory in some logic. If you specify precisely what logic you want to consider this theory in, you can ask whether that logic satisfies downward LST. Or you can ask whether this particular theory has a countable model (assuming it's consistent). But as written, it's not at all clear what you mean. Jan 7, 2019 at 22:26
• Ah - so all the axioms are the usual first-order axioms of ZFC, except that separation applies to formulas of second-order logic, and replacement applies to all functions with no definability requirement. And you consider this theory with the full semantics. Correct? Jan 10, 2019 at 1:48
• If I've understood that correctly, then the second-order replacement is already a problem for having a countable model. Any model $M$ will contain a set called $\omega^M$ with infinitely many elements. Now for any infinite subset $X$ of these elements, there is a function $F: \omega^M\to \omega^M$ with range $X$. So the replacement axiom says that $M$ contains a set whose elements are exactly $X$. And of course there are continuum-many infinite subsets of $\omega$. Jan 10, 2019 at 1:52
• Your theory lacks Infinity. In which case $V_\omega$ is a model and it is countable. Feb 1, 2020 at 20:23

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.