There is a second-order sentence that is valid in standard semantics but not valid in Henkin semantics?

Question

Let $\Sigma^\mathrm{ST}$ be a set of sentences that is valid in standard semantics and $\Sigma^\mathrm{Henk}$ be a set of sentences that is valid in Henkin semantics. Since $\Sigma^\mathrm{Henk}\subseteq \Sigma^\mathrm{ST}$ and $\Sigma^\mathrm{Henk}$ is r.e., but $\Sigma^\mathrm{ST}$ is not r.e. so there is a sentence $\sigma$ that is valid in standard semantics but is not valid in Henkin semantics.

However, there is a concrete example of such sentence? I think an analogue of Replacement $$ \forall X\forall f \exists Y \forall x : Y(x)\leftrightarrow X(f(x)) $$ (where $X$ and $Y$ are unary predicate symbol and $f$ is a unary function symbol) is a such sentence, but I don't know how to prove it. Thanks for any help.

Answer 1

For a very simple case of a sentence that is a valid on standard semantics and not in Henkin semantics (broadly understood), take the sentence

$$\exists X\forall x(Xx \equiv x \neq x)$$

which says that there is an empty property. That is valid on the standard semantics (since the quantifier $X$ over unary properties always ranges over all possible subsets of $D$ where $D$ is the domain of the first-order quantifier -- which always includes the empty subset). But it is not true in every Henkin model [since in Henkin models, the domain of the second-order quantifier is not constrained to included every possible subset of the the domain if the first-order quantifier.]

Which shows that not every instance of the comprehension scheme holds in Henkin models (broadly understood), though of course it does in full or standard models.

[The standard work on these matters is Stewart Shapiro's Foundations without Foundationalism: A Case for Second-Order Logic. A quick check confirms that your initial question is in fact answered on p. 89.]

---

Suppose however, to follow up Carl Mummert's observation, we restrict ourselves to so-called faithful Henkin models (models which don't falsify any instance of the usual second-order comprehension schema or falsify choice). Indeed, talk of Henkin models often just means such faithful models. Then we can refine the original question: what is an example of a second-order sentence which is valid on full semantics, but not on true in all faithful Henkin models?

Well, a fancy but quite cute example, assuming the continuum hypothesis is true, is the second-order sentence which formulates the continuum hypothesis which comes out true on the standard semantics, but which can fail in faithful Henkin models.

For a less exotic but perhaps more approachable example, see Carl Mummert's very helpful answer.

[Again, a quick check to confirm my increasingly fallible memory shows that I must have got that from Shapiro, p. 105. ]

Answer 2

Let $P_2$ be the conjunction of the finite set of Peano's postulates for second-order arithmetic. These have only one full model, which is the standard model of second-order arithmetic.

We know from the incompleteness theorems that, no matter what consistent, effective extension $X$ of $P_2$ we consider, there will be some sentence $\phi_X$ in the language of arithmetic that is true in the standard model but not provable in $X$.

In particular we can let $X$ include the complete deductive system for second-order logic, the full comprehension scheme for second-order arithmetic, and the full scheme for the axiom of choice in second-order arithmetic, and any other effective axioms schemes we like.

As long as we keep $X$ consistent and effective, $P_2 \to \phi_X$ will be true, and thus valid in full semantics, but $P_2 \to \phi_X$ will not be valid in Henkin semantics. Because we let $X$ include the entire deductive apparatus of second-order logic and the comprehension and choice schemes, we don't have to worry about Henkin models of $X$ that might not satisfy these schemes.

This suggests the right way to visualize the difference between full and Henkin semantics: full semantics, in many cases, are just another way of talking about truth in a canonical "standard" model, while Henkin semantics correspond to provability instead.

As one example of how strong $X$ could be, it could include the entire set of sentences of second-order arithmetic that are provable in ZFC (this is an r.e. set of sentences, so it makes an effective axiom scheme). Then $\phi_X$ will be a true sentence of second-order arithmetic, so $P_2 \to \phi_X$ is valid in full semantics, but $\phi_X$ (and also $P_2 \to \phi_X$) will remain unprovable even if we assume as an axiom every sentence of second-order arithmetic that is provable in ZFC.

In the previous paragraph, we could replace ZFC with any sufficiently strong, consistent, effective theory $X$. There will still be a sentence $P_2 \to \phi_X$ of second order arithmetic that is valid (in full semantics) but not provable in $X$. In this way, second order logical validity (in the language of second order arithmetic with full semantics) cannot be captured in any effective theory whatsoever. In contrast, logical validity in the language first order arithmetic with first order semantics can be captured by the effective theory $V$ that just enumerates all the logically valid sentences (which just means the provable sentences, in these semantics). But $V$ is derivable even from the empty set of axioms, so in this sense every effective theory captures first-order logical validity.