Complete and correct deductive axiom for SOL

Well, that depends: what do you mean by "deductive system"? (Also, what do you mean by "second-order logic"? See below . . .)

Second-order logic is not compact: there is a set of sentences $\Gamma$ and a sentence $\varphi$ in second-order logic, such that $\Gamma\models\varphi$ - that is, every model of $\Gamma$ is a model of $\varphi$ - but $\Gamma_0\not\models\varphi$ for any finite subset $\Gamma_0\subseteq \Gamma$. So, any (complete and correct) deductive system for second-order logic would have to allow for proofs with infinitely many premises - this is arguably not a deductive system anymore!

It gets worse - the set of validities in second-order logic depends on set theory! For example, we can write down a single second-order sentence $\varphi$ - in the empty language, no less! - such that $\varphi$ is a tautology iff $2^{\aleph_0}=\aleph_1$. So even if we allow deductions to use infinitely many premises at once, we're going to have a bad day, since if $\mathcal{D}$ is a complete correct deductive system for second-order logic then (at least) one of the following must hold:

  • The property "$x$ is a proof (in the sense of $\mathcal{D}$) of $\varphi$" must not be set-theoretically absolute. In particular, this means that if we want proofs to be coded by sets of natural numbers (which seems reasonable, since individual second-order sentences can be coded as individual natural numbers quite nicely), then the relation "$x$ proves $\varphi$" must be hideously complicated - it cannot be $\Sigma^1_2$, for example, and in the presence of large cardinals it has to be even worse.

  • ZFC cannot prove that $\mathcal{D}$ is, in fact, a complete correct deductive system for second-order logic.

In fact, we can even show that the set of validities in second-order logic is arbitrarily complicated, in a precise sense: given any model $V$ of ZFC, and any real $r\in V$, there is a forcing extension $V[G]$ such that $V[G]\models$"The set of second-order validities computes $r$."

Basically, everything is bad forever.


There's a caveat here: by "second-order logic," I assume you mean second-order logic with the standard semantics. We could also adopt Henkin semantics, at which point second-order logic is really just first-order logic in disguise, so we do have a complete, consistent, recursive deductive system. But I assume you're not doing that here.


EDIT: Based on your response, I suspect that you view what I've written above as evidence that second-order logic isn't really "logic" at all. You're certainly in good company, there - Quine, for instance, famously called second-order logic "set-theory in sheep's clothing". There is work on set-theoretically-absolute logics, which you may prefer; see e.g. https://math.stanford.edu/~feferman/papers/InvCriteriaLogic.pdf or http://projecteuclid.org/download/pdf_1/euclid.pl/1235417283.

But my question to you, at the beginning of my answer, still stands: what do you mean by "deductive system"? There are logics which are not compact, but which are set-theoretically absolute - e.g. first-order logic together with a quantifier for "there are infinitely many $x$ such that . . ." Whether or not such a logic has a complete correct deductive system depends crucially on what you mean by "deductive system." So I think by focusing on the set-theoretic aspects of second-order logic, you're missing part of my point.


As Ben Millwood wrote in a comment, the answer is trivially "yes". Take all the statements you want to be provable, and make them axioms of your new deductive system, along with no rules of inference. Then this will be a complete deductive system, in whatever sense of "complete" you used to decide on the set of statements you'd like to be provable.

More generally, if you want to capture provability with hypotheses, consider the following construction. Suppose there is some satisfaction relation $R$ whose first argument is a set of sentences $\Gamma$ and whose second argument is a sentence $\phi$. For example, $\Gamma R \phi$ might mean that $\phi$ holds in every model of $\Gamma$, or in every model of some special form (as in full second-order semantics), or $R$ could be some other relation.

Consider a deductive system in which we have only one deductive rule: "Whenever $\Gamma R \phi$, the ordered pair $(\Gamma, \phi)$ is a deduction of $\phi$ from $\Gamma$". Of course, this is not likely to be an effective proof system -- it allows for infinitary sets of hypotheses, and even if we limit $\Gamma$ to be finite there is no reason $R$ needs to be computable. But it does give a deductive system in which, trivially, $\Gamma \vdash \phi$ if and only if $\Gamma R \phi$.