Towards Elimination of Second-Order Quantifiers in the Separated Fragment
Marco Voigt · MPG.PuRe (Max Planck Society) · 2017
It is a classical result that the monadic fragment of secondorder logic admits elimination of second-order quantifiers.Recently, the separated fragment (SF) of first-order logic has been introduced.SF generalizes the monadic first-order fragment without equality, while preserving decidability of the satisfiability problem.Therefore, it is a natural question to ask whether SF also admits elimination of second-order quantifiers.Interestingly, already Ackermann answered this question in the negative as far as full SF with unrestricted occurrences of second-order quantifiers is concerned.However, with appropriate restrictions on the syntax of a second-order version of SF, one could hope to define a substantial extension of the monadic fragment that admits second-order quantifier elimination.The present note is about preliminary results of ongoing research in this direction.As a first positive result a restricted second-order version of SF is defined that admits the elimination of at least one existential second-order quantifier.The elimination of existential second-order quantifiers from a monadic sentence without equality constitutes a special case of the methods presented here.