EPR, the umbrella #
Satisfiability of an ∃*∀* sentence – the Bernays–Schönfinkel–Ramsey class:
the instance encoding and its semantics
(DescriptiveComplexity.Problems.Epr.Defs), the small-model property
(DescriptiveComplexity.Problems.Epr.Small) and the membership in NEXPTIME
(DescriptiveComplexity.Problems.Epr.Membership).
The two halves of the membership are the two halves of the classical argument:
a satisfiable ∃*∀* sentence has a model on the instance itself, and checking
such a model is one Σ₁ sentence read over an expansion whose points are the
relations on the instance – an assignment of the universal variables being one
of them. Hardness is not formalized yet.
Satisfiability of an ∃*∀* sentence is in NEXPTIME.