Which second-order theories have a model?

Question

A first-order theory has a model if and only if it's consistent.

If a second-order theory has a model then it's consistent, but the converse doesn't hold.

So I'm wondering if there's some condition, stronger than consistency, that tells you when a second-order theory does have a model. Is there some purely syntactic property that a theory has if and only if it has a model?

---

Obviously I'm talking about the full semantics here rather than Henkin semantics, since theories have a Henkin model if and only if they're consistent.

Answer 1

Such a property cannot exist, at least if

• a "purely syntactic" property means something that can be expressed as a first order arithmetical property of the Gödel numbers of the theory's axioms (which does not seem unreasonable).
• we're supposed to be able to prove that the property works, using ordinary ZFC as our metatheory.

Consider that we can write down a finitely axiomatized second-order theory that has a model if and only if the continuum hypothesis is true at the metalevel. (Start with the second-order Peano axioms, add a new sort for sets of integers, and claim that every set of sets of integers has either an injection into the naturals or a surjection onto the entire universe).

However, if we take a model of ZFC+¬CH, and also take its constructible universe, then we have two models of ZFC where one satisfies the continuum hypothesis but the other doesn't, yet the two models have the same integers (and the same arithmetic on them). So any proposed "purely syntactic" criterion would give the same answer in both of them, yet that answer would be wrong in one of them.

Answer 2

For simplicity, it is common to work just with the language of equality. Let $V^2$ be the set of second-order validities in this language. It is also somewhat common to look at the set $V^2$ instead of the set of consistent sentences. Of course a sentence is consistent if and only if its negation is not a validity, so there is no real difference in studying $V^2$.

The answer by Henning Makholm shows that $V^2$ is not definable in first-order arithmetic.

This can be extended to show that $V^2$ is not definable in second-order arithmetic. The proof is essentially just Tarski's theorem on the undefinability of truth.

Because each $n$th-level higher order arithmetic is interpretable in second-order arithmetic in a well-known way, this shows that $V^2$ is not definable in $n$th order arithmetic for any $n$.

I don't have a copy at hand of "Set Theory and Higher-Order Logic", Richard Montague, 1965, in Formal Systems and Recursive Functions, Studies in Logic and the Foundations of Mathematics v. 40, pp. 131-148. DOI 10.1016/S0049-237X(08)71686-0. Shapiro attributes to this paper an extension that $V^2$ is not definable even in a collection of transfinite levels of higher-order arithmetic.

As an upper bound, it appears Montague proved that if $\lambda$ is the Lowenheim number of second-order logic then $V^2$ is definable in $(\lambda + 1)$th order arithmetic. The Lowenheim number is the smallest cardinal $\lambda$ so that if a theory $T$ has a model then it has a model of size less than $\max(|T|,\lambda)$.

For second order logic in standard semantics the Lowenheim number is known to be extremely large - it is larger than the first measurable cardinal if there is a measurable cardinal. For more discussion of $\lambda$, which they call $\text{LS}(L^2)$, see Menachem Magidor and Jouko Väänänen, "On Löwenheim-Skolem-Tarski numbers for extensions of first order logic", J. Math. Log. v. 11, 2011, DOI 10.1142/S0219061311001018,