<p>I'm trying to understand what is currently known to be possible regarding the elimination of monadic second-order quantifiers. Many sources cite that monadic second-order logic supports elimination of second-order quantifiers, and while many cite directly Löwenheim, I've found this <a href="https://dblp.dagstuhl.de/rec/conf/tableaux/Wernhard15.html" rel="nofollow noreferrer">modern description</a> of how it works.</p>
<p>However, what is not clear to me, is if the inner first-order sentence has to be monadic as well. What I mean precisely is the following.</p>
<p>Let <span class="math-container">$\Sigma$</span> be a first-order signature of any kind, and let <span class="math-container">$\psi$</span> be a first-order sentence over <span class="math-container">$\Sigma\cup\{P_1,\ldots,P_n\}$</span> where <span class="math-container">$P_1,\ldots,P_n$</span> are <em>monadic</em> predicates. Consider <span class="math-container">$\phi\equiv \exists P_1\ldots P_n . \psi$</span>.</p>
<p>Can I eliminate the monadic second-order quantifiers from <span class="math-container">$\phi$</span>? Or is <span class="math-container">$\psi$</span> required to be a monadic first-order sentence as well?</p>
<p><strong>Edit</strong>: since the answer is likely just a single &quot;No&quot;, what I'd actually need is fragments of non-monadic FO where monadic second-order quantifiers put on top can be eliminated.</p>
<p>So which conditions have <span class="math-container">$\psi$</span> to satisfy to be able to eliminate the second-order quantifiers from <span class="math-container">$\phi$</span>?</p>

CC BY-SA 4.0
2023-09-23T20:37:16.270Z
You certainly have to assume $\psi$ is monadic, otherwise it does not hold in general. E.g., if the structure has a pairing function, then monadic second-order quantifiers have the same expressive power as *arbitrary* second-order quantifiers.
Emil Jeřábek
CC BY-SA 4.0
2023-09-23T20:57:48.910Z
Hm, I see... What about relational signatures or maybe only binary relations?
Nicola Gigante
CC BY-SA 4.0
2023-09-23T20:59:48.873Z
I've added a clarification on the question: what I actually need is to know if there are fragments where this is possible.
Nicola Gigante
CC BY-SA 4.0
2023-09-23T21:05:23.470Z
A single binary relation (or two unary functions) is enough to encode any structure in finite signature, hence the elimination of MSO quantifiers cannot hold for such signatures either. E.g., just think of the binary relation as the $\in$ of set theory.
Emil Jeřábek
CC BY-SA 4.0
2023-09-23T21:09:10.383Z
I see… bad news Emil. But thanks :)
Nicola Gigante
CC BY-SA 4.0
2023-09-23T21:11:17.453Z
Wait, but there can be fragments of FO where you cannot actually express anything with just a binary relation. What about FO^2 or other decidable fragments of FO?
Nicola Gigante
CC BY-SA 4.0
2023-09-24T07:13:52.160Z
I’m skeptical whether there is any useful fragment where you can do this. E.g., in the MSO definition of nonstandard numbers in $(\mathbb N+\mathbb Z,0,S)$, viz. $\exists X\,(0\in X\land x\notin X\land\forall x\,(x\in X\to S(x)\in X))$, the MSO quantifier cannot be eliminated on top of a universal $\mathrm{FO_2}$ formula (even if you consider $S$ to be a binary relation, in which case one needs a second FO quantifier).
Emil Jeřábek
<first-order-logic>
Elimination of monadic second-order quantifiers
Nicola Gigante
# Elimination of monadic second-order quantifiers

(Asked by: username_0 on 2023-09-23)

I'm trying to understand what is currently known to be possible regarding the elimination of monadic second-order quantifiers. Many sources cite that monadic second-order logic supports elimination of second-order quantifiers, and while many cite directly Löwenheim, I've found this [modern description](https://dblp.dagstuhl.de/rec/conf/tableaux/Wernhard15.html) of how it works.

However, what is not clear to me, is if the inner first-order sentence has to be monadic as well. What I mean precisely is the following.

Let $\Sigma$ be a first-order signature of any kind, and let $\psi$ be a first-order sentence over $\Sigma\cup\{P\_1,\ldots,P\_n\}$ where $P\_1,\ldots,P\_n$ are *monadic* predicates. Consider $\phi\equiv \exists P\_1\ldots P\_n . \psi$.

Can I eliminate the monadic second-order quantifiers from $\phi$? Or is $\psi$ required to be a monadic first-order sentence as well?

**Edit**: since the answer is likely just a single "No", what I'd actually need is fragments of non-monadic FO where monadic second-order quantifiers put on top can be eliminated.

So which conditions have $\psi$ to satisfy to be able to eliminate the second-order quantifiers from $\phi$?

**Tags:** first-order-logic
> **Comments:**
> **username_1**: You certainly have to assume $\psi$ is monadic, otherwise it does not hold in general. E.g., if the structure has a pairing function, then monadic second-order quantifiers have the same expressive power as *arbitrary* second-order quantifiers.  
> **username_0**: Hm, I see... What about relational signatures or maybe only binary relations?  
> **username_0**: I've added a clarification on the question: what I actually need is to know if there are fragments where this is possible.  
> **username_1**: A single binary relation (or two unary functions) is enough to encode any structure in finite signature, hence the elimination of MSO quantifiers cannot hold for such signatures either. E.g., just think of the binary relation as the $\in$ of set theory.  
> **username_0**: I see… bad news Emil. But thanks :)  
> **username_0**: Wait, but there can be fragments of FO where you cannot actually express anything with just a binary relation. What about FO^2 or other decidable fragments of FO?  
> **username_1**: I’m skeptical whether there is any useful fragment where you can do this. E.g., in the MSO definition of nonstandard numbers in $(\mathbb N+\mathbb Z,0,S)$, viz. $\exists X\,(0\in X\land x\notin X\land\forall x\,(x\in X\to S(x)\in X))$, the MSO quantifier cannot be eliminated on top of a universal $\mathrm{FO_2}$ formula (even if you consider $S$ to be a binary relation, in which case one needs a second FO quantifier).  

---

## 0 answers

