# Deciding Satisfiability of a "Universal" Second-Order Logic Formula

Consider the following decision problem:

• Input: a second-order logic formula $$\psi$$ of the form $$\forall X_1 . \ldots . \forall X_n . \phi$$ where $$X_1, \ldots, X_n$$ are a second-order variables and $$\phi$$ is a first-order logic formula.
• Output: yes iff $$\psi$$ is satisfiable.

Is this problem $$\Pi_1^1$$-complete? If so, can you explain why or point me to some reference to learn more about it? Thanks!

• No, it’s much harder. It is as hard as satisfiability in unrestricted second-order logic (or even higher-order logic). To see this, given a second-order sentence, reconsider it as a two-sorted first-order sentence, and conjoin it with a universal second-order sentence saying “every subset of the first sort is represented in the second sort”. Oct 16, 2023 at 9:14
• The question seems underspecified: what language/logic are you working over (propositional, arbitrary predicate language, language of arithmetic,...)? Also what semantics are you considering (Henkin, full, intended)? If, for instance, you are over the language of arithmetic and considering only standard interpretations (i.e. SO variables vary over the full powerset of $\mathbb N$) then the problem is $\Sigma^1_2$-complete. Oct 16, 2023 at 22:57
• Emil: Can you point me to some reference that explains your comment a bit further? I am afraid that I cannot understand your answer. Oct 18, 2023 at 6:31
• See plato.stanford.edu/entries/logic-higher-order/#PropSecoOrdeForm (specifically, starting from “There is a sense in which ...”). There is an outline of the reduction and a few references for the original result. Oct 18, 2023 at 7:19
• Thanks loads! That's a very useful pointer : ) Oct 19, 2023 at 9:02