<p>Since there are no answer I think it may be useful to post <a href="http://collegepublications.co.uk/logic/mlf/?00009" rel="nofollow noreferrer">what I've found</a>:</p>
<p>Dov M. Gabbay, Renate A. Schmidt, Andrzej Szalas<br />
<em>Second-Order Quantifier Elimination - Foundations, Computational Aspects and Applications</em>.<br />
Studies in logic : Mathematical logic and foundations 12, College Publications 2008,<br />
ISBN 978-1-904987-56-7, pp. I-VIII, 1-308</p>
<p>It seems quite complete and well-written. That's what I was looking for.</p>

CC BY-SA 4.0
2023-09-10T20:03:09.063Z
2023-09-10T20:03:09.063Z
Nicola Gigante
<p>I was wondering whether something like elimination of second-order quantifiers exist, and indeed it seems it does. I've found there's a workshop on this topic, and <a href="http://2021.soqe.org" rel="noreferrer">the webpage</a> describes exactly what I need:</p>
<blockquote>
<p>Second-order quantifier elimination (SOQE) is the problem of
equivalently reducing a formula with quantifiers upon second-order
objects such as predicates to a formula in which these quantified
second-order objects no longer occur.</p>
</blockquote>
<p>Unexpectedly (at least for me) the topic seems to be related to a lot of other things that I need for what I'm doing: Craig interpolants, uniform interpolants, Beth definability.</p>
<p>So is there a reference (maybe a survey?) about second-order quantifier elimination and its connections with the topics above?</p>

<reference-request><first-order-logic>
References on second-order quantifier elimination and related topics
Nicola Gigante
# References on second-order quantifier elimination and related topics

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

I was wondering whether something like elimination of second-order quantifiers exist, and indeed it seems it does. I've found there's a workshop on this topic, and [the webpage](http://2021.soqe.org) describes exactly what I need:

> Second-order quantifier elimination (SOQE) is the problem of
> equivalently reducing a formula with quantifiers upon second-order
> objects such as predicates to a formula in which these quantified
> second-order objects no longer occur.

Unexpectedly (at least for me) the topic seems to be related to a lot of other things that I need for what I'm doing: Craig interpolants, uniform interpolants, Beth definability.

So is there a reference (maybe a survey?) about second-order quantifier elimination and its connections with the topics above?

**Tags:** reference-request, first-order-logic

---

## 1 answers

### Answer by username_0 on 2023-09-10. Score: 3 | Accepted answer

Since there are no answer I think it may be useful to post [what I've found](http://collegepublications.co.uk/logic/mlf/?00009):

Dov M. Gabbay, Renate A. Schmidt, Andrzej Szalas  
*Second-Order Quantifier Elimination - Foundations, Computational Aspects and Applications*.  
Studies in logic : Mathematical logic and foundations 12, College Publications 2008,  
ISBN 978-1-904987-56-7, pp. I-VIII, 1-308

It seems quite complete and well-written. That's what I was looking for.


---

