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 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?


1 Answer 1


Since there are no answer I think it may be useful to post what I've found:

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.