# A axiomatization of (full) Second Order Logic with a decidable proof system cannot be complete; is this true if we only require semi-decidability?

My understanding is that, unlike first order logic, no "effective" (sound, consistent) axiomatization of second order logic is complete; there will always be statements true in all models, but not provable from the axioms. "Effective" here means that there exists a terminating algorithm that tells you whether or not a given string is a valid proof. First of all, is this understanding correct?

Second of all, does anything change if we only require semi-decidability? That is, if there is an algorithm that (1) always terminated with the correct answer when given a valid proof string, but (2) either terminates with correct answer or doesn't terminate at all when given an invalid proof string. I have a hard time imagining what undecidable deductive systems would even look like, including semi-decidable ones, so I can't figure out if the answer to this question is obvious, though I sort of suspect that it is...

I assume here that you mean second-order logic with the standard, as opposed to Henkin, semantics.

It turns out the answer is no - the situation is far, far worse than may be obvious at a first glance.

Let's ignore deductive systems entirely, and just look at the set of second-order validities - that is, the set $Val_2$ of second-order validities (= second-order sentences which are true in every model according to the standard semantics). Intuitively, these are the ones which should be provable if our proof system is to be complete, and if you have a proof system of the type you describe then by searching through all possible proofs we would have that $Val_2$ is recursively enumerable. So your question is really an aspect of:

What is the computability-theoretic complexity of the set $Val_2$?

The answer turns out to be: really really huge. For example, it's not even in the arithmetic hierarchy at all (so in particular, Post's theorem tells us that the answer to your question is no), or even hyperarithmetic, so in a sense you can't figure out whether a second-order sentence is valid even if you could iterate the Turing jump "as many times as you want."

At this point it's a good exercise to prove a small fragment of the above claim: show that there is a computable sequence of second-order sentences $\psi_i$ such that for each $i$, $\psi_i$ is valid iff $i$ is not in the Halting Problem. Since the complement of the Halting Problem is not c.e., this will give a negative answer to your question. HINT: first show that there is a second-order sentence $\varphi$ which characterizes $(\mathbb{N}; +,\times)$ up to isomorphism, then think about how to describe Turing machines in the language of arithmetic ...

Another important aspect of the terribleness of second-order logic (with the standard semantics) - not directly related to your question, but important for developing an intuition for the subject - is its dependence on set theory (which has led to a debate over whether it even qualifies as a proper logic; I'm not going to get into that here, but if you're interested you can search for work of Quine, Shapiro, and Vaanaanen on the subject). Specifically, whether a second-order sentence is valid can depend on set-theoretic principles which are neither provable nor disprovable from the usual axioms of set theory!

The standard example is that there is a second-order sentence $\chi$ which is valid iff the continuum hypothesis holds. Constructing $\chi$ takes a bit of work but is ultimately not too hard, and reveals the "set-theoretically contingent" quality of second-order logic (especially in light of forcing, which shows that we can change whether a second-order sentence is valid or not by altering the set-theoretic universe, while first-order logic is much more$^1$ "absolute").