Bernays–Schönfinkel Class

Origin. Paul Bernays and Moses Schönfinkel, "Zum Entscheidungsproblem der mathematischen Logik" (Mathematische Annalen 99, 1928, 342–372), proved satisfiability decidable for relational prenex sentences with prefix ∃∀, without equality. Frank P. Ramsey, "On a Problem of Formal Logic" (read to the London Mathematical Society in December 1928, published in its Proceedings 30, 1930, 264–286), extended the result to equality, proving as his combinatorial lemma the theorem now called Ramsey's theorem; the class with equality is the Bernays–Schönfinkel–Ramsey class. Harry R. Lewis (1980) proved satisfiability NEXPTIME-complete. The solvable-cases program it belongs to is codified in Egon Börger, Erich Grädel and Yuri Gurevich, The Classical Decision Problem (Springer, 1997).

Models. Relational sentences whose quantifier prefix puts every existential before every universal: witnesses are chosen once, and a model need contain nothing beyond them and the constants. The shape is the decidability: a universal sentence holds in every substructure of its model, so restricting any model to the witnesses and constants yields a model, and nothing larger needs to be searched. Grounding the universal variables over that finite set turns the sentence into a propositional formula, which is why the class's modern name is effectively propositional logic, EPR. Over relational vocabulary without equality there are exactly three maximal decidable prefix patterns, ∃∀ among them; the map below records the whole classification.

Formalism.

Shape: ∃x₁ … ∃xₘ ∀y₁ … ∀yₙ. φ, φ quantifier-free, relational, no function symbols. With equality: the Bernays–Schönfinkel–Ramsey class (BSR).

Small model property: Satisfiable → model of size ≤ max(1, m + number of constants). Universal sentences pass to substructures; restrict any model to the witnesses and constants.

Grounding: Instantiate the universal variables over the witnesses and constants: a propositional formula of size |φ|·(m+c)ⁿ, c the number of constants. Effectively propositional: decide by any SAT method after the expansion.

Complexity: NEXPTIME-complete (Lewis 1980). The exponential grounding is worst-case unavoidable.

The prefix-class map (relational vocabulary, no equality, no function symbols): ∃∀ — decidable (Bernays–Schönfinkel 1928). ∃∀∃ — decidable, finite model property (Ackermann 1928); EXPTIME-complete. ∃∀∀∃ — decidable, finite model property (Gödel 1933; also Kalmár and Schütte) — the Gödel–Kalmár–Schütte class. ∀∃∀ — undecidable (Kahr–Moore–Wang 1962); minimal, since ∀∃, ∃∀ and ∀∀ each fit a decidable pattern. ∀∀∀∃ — the other minimal undecidable prefix: one universal more than the Gödel pattern's ∀∀∃ core. A prefix class is decidable iff its prefixes all match one of the three decidable patterns (Börger–Grädel–Gurevich 1997). Scott's 1962 reduction lands the two-variable fragment in the Gödel class, so the map reaches beyond prenex syntax.

Equality: ∃∀ with equality — decidable, finite model property (Ramsey 1930). ∃∀∃ with equality — finite model property persists (Dreben–Goldfarb 1979). ∃∀∀∃ with equality — undecidable, already at ∀∀∃ (Goldfarb 1984), refuting Gödel's claim that his argument covered identity.

Function symbols: ∃∀∃ admits arbitrary function symbols without equality (Gurevich; Maslov–Orevkov), and with equality plus a single unary function stays decidable while the finite model property fails (Shelah). ∃∀ admits none.

Symbols.

Metatheory. Decidability rests on the substructure argument and nothing deeper: the model found is linear in the sentence, the strongest form of the finite model property, so infinity is inexpressible and satisfiability coincides with finite satisfiability. Ramsey (1930) carried the argument through equality, and the combinatorial theorem he proved to control the equality types of tuples founded Ramsey theory as a byproduct. Satisfiability is NEXPTIME-complete (Lewis 1980). In complexity the class is interchangeable with dependency quantified Boolean formulas: DQBF is NEXPTIME-complete and translates to EPR by Skolemization, making the class the first-order counterpart of Henkin quantification over propositions (quantified Boolean formulas; branching quantifiers). Against its neighbours: equality leaves ∃∀ decidable (Ramsey 1930) and leaves the Ackermann class its finite model property (Dreben–Goldfarb 1979), but makes the Gödel class undecidable already at ∀∀∃ (Goldfarb 1984); and the minimal undecidable prefixes show how tight each decidable pattern is — appending one universal to the Ackermann pattern's ∀∃ core gives ∀∃∀ (Kahr–Moore–Wang 1962), prefixing one universal to the Gödel pattern's ∀∀∃ core gives ∀∀∀∃.

Applies to. SMT solving and first-order theorem proving, where EPR is the decidable target of grounding and instantiation-based methods. Verification of parameterized systems and protocols whose axioms avoid function symbols. Finite model finding. Complexity theory, as a natural NEXPTIME-complete problem. The classical decision problem.

Limitations. No function symbols, and none can be smuggled in: Skolemizing a ∀∃ dependence produces exactly the functions the class forbids, so "every node has a successor" — any sentence whose witnesses vary with a universally quantified element — is outside it, and a specification with an unbounded datatype or an arithmetic operation is already outside EPR. Infinity is inexpressible, so nothing whose models are all infinite can be stated: orders the class can axiomatize, since transitivity and totality are purely universal, but not a discrete order without endpoints. Grounding is exponential in the number of universal variables, and the NEXPTIME lower bound (Lewis 1980) makes that intrinsic; instantiation methods succeed by instantiating selectively. Because every satisfiable sentence has a model of linear size, the class cannot force models larger than its witness count, so cardinality constraints beyond pairwise-distinct witnesses are out of reach.

© 2026 Lingenic LLC