Exists-Forall Class (EPR, BSR) Definition
Notation according to Classical Decision Problem classification:
That means: first-order logic sentences of the form where is quantifier-free formula with equality, with arbitrary relation symbols and constants, but without function symbols.
Summary of restrictions:
- only universal quantifiers (the initial existential ones get skolemized in satisfiability checking)
- no function symbols
For binary relations to express , we can introduce binary relation symbols , , and write formula
To express we would write
List contains no duplicates:
Relation is a partial function
We cannot express in this class that is a total function, or property like because we need an existential quantifier after a universal one.