Is second-order logic with full semantics effectively checkable?

Question

My question is simple. Is second-order logic with full semantics (not Henkin semantics) effectively checkable? That is, are the inference rules of second-order logic effective?

Answer 1

Your question ultimately mixes two very different objects: the "full inference relation" $\models_{II}$ for second-order logic with the standard semantics, and any of the many "effective approximations" to this, which I'll denote by "$\vdash_{II}^i$" (the "$i$" emphasizing that there are lots of these: $\vdash_{II}^1,\vdash_{II}^2,\vdash_{II}^3,...$, which are in general not equivalent in any sense).

It's easy to check that $\models_{II}$ is not effective in any sense: the set of validities (= those sentences $\varphi$ satisfying $\emptyset\models_{II}\varphi$) is not r.e., or even arithmetically definable, or even hyperarithmetic, or ... etc. However, each of the $\vdash_{II}^i$s is indeed effective.

So as before, we run into the question: what do you mean by inference? You emphasize here and at your other question that you're interested in the full semantics, but the restricted entailment relations $\vdash_{II}^i$ are not complete with respect to that semantics; if they're what you're actually interested in, then you're not actually looking at the full semantics at all. It is true of course that each of the $\vdash_{II}^i$s are essentially first-order, but when explicitly talking about the full semantics they're not what people mean by "second-order inference." It's in this latter sense, by the way, that people (correctly) say that second-order logic can't be reduced to first-order logic, and this in no way contradicts the effectiveness of the much, much weaker $\vdash_{II}^i$s.

It's worth noting that some authors take "inference" or "proof" to presuppose a fixed effective deductive system (like this quora answer, which in my opinion is misleading in an important way). In that case you need to tell us what "second-order logic" is in this context, since - unlike FOL - there are many natural effective deductive systems which are sound (but not complete) for the full semantics but which are non-equivalent.

I think the quora answer linked above is misleading precisely because glides over this point - it assumes that "second-order proof" is already something we've settled on a meaning for ("there are an infinite number of statements in second order logic that are universally valid and can be proved to be so"), while missing the point that as soon as we abandon the full semantics we don't have a default deduction relation anymore and need to pick one before we can say anything useful.

---

And lest one try to bootstrap: while (trivially) $\models_{II}$ is indeed the union of all its effective fragments - or at least, when we restrict attention to finite theories - the task of determining whether a proposed effective deduction system $\vdash_{II}^i$ is sound for the full semantics is just as complicated as (actually, strictly more complicated than) the "true" relation $\models_{II}$ itself.