# Exists-Forall Class (EPR, BSR) Definition

Also called Berneys-Schoenfinkel class and Effectively Propositional Logic (EPR).

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

## Examples

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.