<p>Consider the following decision problem:</p>
<ul>
<li>Input: a second-order logic formula <span class="math-container">$\psi$</span> of the form <span class="math-container">$\forall X_1 . \ldots . \forall X_n . \phi$</span> where <span class="math-container">$X_1, \ldots, X_n$</span> are a second-order variables and <span class="math-container">$\phi$</span> is a first-order logic formula.</li>
<li>Output: yes iff <span class="math-container">$\psi$</span> is satisfiable.</li>
</ul>
<p>Is this problem <span class="math-container">$\Pi_1^1$</span>-complete? If so, can you explain why or point me to some reference to learn more about it? Thanks!</p>

CC BY-SA 4.0
2023-10-16T09:14:08.893Z
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”.
Emil Jeřábek
CC BY-SA 4.0
2023-10-16T22:57:42.723Z
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.
Anupam Das
CC BY-SA 4.0
2023-10-18T06:31:45.600Z
Emil: Can you point me to some reference that explains your comment a bit further? I am afraid that I cannot understand your answer.
David Carral
CC BY-SA 4.0
2023-10-18T07:19:00.843Z
See https://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.
Emil Jeřábek
CC BY-SA 4.0
2023-10-19T09:02:11.520Z
Thanks loads! That's a very useful pointer : )
David Carral
<lo.logic>
Deciding Satisfiability of a "Universal" Second-Order Logic Formula
David Carral
# Deciding Satisfiability of a "Universal" Second-Order Logic Formula

(Asked by: username_0 on 2023-10-16)

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!

**Tags:** lo.logic

> **Comments:**
> **username_1**: 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”.  
> **username_2**: 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.  
> **username_0**: Emil: Can you point me to some reference that explains your comment a bit further? I am afraid that I cannot understand your answer.  
> **username_1**: See https://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.  
> **username_0**: Thanks loads! That's a very useful pointer : )  

---

## 0 answers

