Satisfiability of Second-Order Logic: Is this Decision Problem Complete for Some Level of the Arithmetical Hierarchy?

Question

Consider the following decision problem defined in terms of input/output:

• Input: a second order logic [1] theory $\mathcal{T}$ (i.e., $\mathcal{T}$ is a set of second order logic formulas)
• Output: yes if and only if $\mathcal{T}$ is satisfiable (i.e., there is a model that satisfies all of the formulas in $\mathcal{T}$)

Is this decision problem complete for some level of the arithmetical hierarchy [2]?

[1] https://en.wikipedia.org/wiki/Second-order_logic

[2] https://en.wikipedia.org/wiki/Arithmetical_hierarchy

Answer 1

The satisfiability question for second-order logic (with the standard semantics, anyways) is way way way beyond the arithmetical hierarchy. In fact, it's even beyond the analytical hierarchy:

The set of (Godel numbers of) satisfiable second-order sentences in the language of arithmetic is not second-order definable in the standard model of arithmetic $\mathfrak{N}=(\mathbb{N};+,\times)$.

This is an immediate consequence of two facts:

1. There is a second-order sentence $\theta$ which characterizes $\mathfrak{N}$ up to isomorphism.

2. Tarski's undefinability theorem, while usually stated simply for first-order logic, is actually much broader than that: the same argument shows for example that the second-order theory of $\mathfrak{N}$ is not second-order definable in $\mathfrak{N}$.

Combining 1 and 2, we get the claim above: for $\sigma$ a second-order sentence we have $\mathfrak{N}\models\sigma$ iff $\theta\wedge\sigma$ is satisfiable, so the second-order theory of $\mathfrak{N}$ is reducible to the satisfiability problem for second-order sentences $\mathsf{Sat}_2$.

(Contrast this with the situation for first-order arithmetic: the satisfiability of a first-order sentence is first-order definable in $\mathfrak{N}$, indeed $\Pi_1$, the difference being that compactness for first-order logic prevents point 1 above from holding for first-order logic.)

It's a good exercise meanwhile to show the following:

For every $U\subseteq\mathbb{N}$ which is second-order-definable in $\mathfrak{N}$, we have $U\le_T\mathsf{Sat}_2$.

You'll want to use point 1 above here.

---

In fact this is only the start of the disaster. For example, $\mathsf{Sat}_2$ encodes the set $$A=\{\langle m,n\rangle\in\mathbb{N}^2: 2^{\aleph_m}=\aleph_n\},$$ which is consistently as complicated as one wants: for any $X\subseteq\mathbb{N}$ there is a forcing extension of the universe in which $X\le_TA$.