Two-Variable Logic

Origin. Dana Scott (1962) showed that FO² without equality reduces to the Gödel prefix class ∀∀∃*, and so is decidable; the reduction is what is now called Scott normal form. Michael Mortimer (1975) extended the result to FO² with equality, proving the finite model property with a doubly exponential bound on model size. Erich Grädel, Phokion Kolaitis and Moshe Vardi (1997) sharpened the bound to exponential and settled the complexity: FO² satisfiability is NEXPTIME-complete. The fragment then acquired a second life as the explanation of why description logics and modal logics are decidable, since the standard translation of modal logic lands inside it.

Models. The restriction is on variable names, not on quantifier depth. Only x and y exist, so a formula of any depth must recycle them, and an inner quantifier rebinds a name its outer occurrence was using — ∀x∃y(R(x,y) ∧ ∀x(…)) is legitimate, and the inner ∀x shadows the outer. What this costs is the ability to relate three objects at once, since no atomic formula can mention a third name. What it gains is that satisfiability is decidable and every satisfiable sentence has a model of size exponential in its length, so the search space is bounded in advance.

Formalism.

Syntax: φ ::= R(x,y) | x=y | ¬φ | φ∧ψ | ∃x.φ | ∃y.φ Only x and y, reused arbitrarily.

Example: ∀x∃y(R(x,y) ∧ ∀x(R(y,x) → P(x))) Note: inner ∀x rebinds x.

Scott normal form: ∀x∀y.α(x,y) ∧ ⋀ᵢ ∀x∃y.βᵢ(x,y) α, βᵢ quantifier-free. Every FO² sentence has an equisatisfiable one of this shape, computable in polynomial time with fresh predicates.

Modal standard translation: □p ↦ ∀y(R(x,y) → p(y)), swapping x and y at each nesting. Two names suffice for any modal depth. This is why K, and ALC, are decidable.

Counting extension C²: ∃^{≥n}x.φ, ∃^{≤n}x.φ: at least, at most n witnesses. Decidable — Grädel, Otto and Rosen (1997). NEXPTIME-complete even with numbers in binary — Pratt-Hartmann (2005). Captures number restrictions in description logic (ALCQ).

Failure of the finite model property in C²: "R is an injective function that is not surjective" is C²-expressible. Only infinite models satisfy it. Satisfiability and finite satisfiability are therefore different problems — both decidable, but separately.

Adding transitivity: Transitivity is not FO²-expressible; imposing it externally is destructive. Grädel, Otto and Rosen (1999): undecidable with transitive relations. Two equivalence relations: decidable. Three: undecidable (Kieroński and Otto).

Symbols.

Symbol	Unicode	Name	Meaning
FO²	—	Two-variable fragment	First-order logic with equality over the names x and y only
FO³	—	Three-variable fragment	The next fragment up; undecidable
C²	—	Counting two-variable fragment	FO² with counting quantifiers
∃^{≥n}	—	Counting quantifier	"At least n witnesses"; ∃^{≤n} is the dual
x, y	—	Individual variables	The only two names available
α, β	—	Schematic formulas	Quantifier-free parts of Scott normal form
∃	U+2203	Existential quantifier	Rebinding is permitted and essential
∀	U+2200	Universal quantifier	Rebinding is permitted and essential
¬	U+00AC	Negation	Boolean connective of the fragment
∧	U+2227	Conjunction	Boolean connective of the fragment
⋀	U+22C0	N-ary conjunction	Indexed conjunction of the ∀x∃y conjuncts
→	U+2192	Conditional	Used in the modal standard translation
=	U+003D	Identity	Present in FO²; Scott's original result omitted it
□	U+25A1	Box / Necessity	Modal operator whose translation lands in FO²
↦	U+21A6	Maps to	The standard translation

Metatheory. Scott (1962) proved FO² without equality decidable by reduction to the Gödel prefix class ∀∀∃*; Mortimer (1975) added equality and proved the finite model property, with a doubly exponential bound; Grädel, Kolaitis and Vardi (1997) improved the bound to exponential and showed satisfiability NEXPTIME-complete. Every sentence has an equisatisfiable Scott normal form ∀x∀y.α ∧ ⋀ᵢ∀x∃y.βᵢ, computed in polynomial time by naming subformulas, and the decision procedure works on that shape. The boundary is sharp on both sides: FO³ is undecidable, and so is FO² once relations are required to be transitive (Grädel, Otto and Rosen 1999), though FO² with two equivalence relations stays decidable and three do not (Kieroński and Otto). Counting is the one extension that survives — C² is decidable (Grädel, Otto and Rosen 1997) and NEXPTIME-complete even with numerical parameters coded in binary (Pratt-Hartmann 2005) — but it loses the finite model property, since an injective non-surjective function is C²-definable, so satisfiability and finite satisfiability become distinct problems and each needs its own algorithm.

Applies to. Description logic foundations. Complexity analysis. Decidable fragments. Ontology languages.

Limitations. Two names cannot relate three objects, so no ternary atom is usable at full arity and the fragment is confined to relational vocabularies of arity at most two. Transitivity, well-foundedness, being a linear order and reachability are all inexpressible, and the first cannot be imposed as a background condition without losing decidability — which excludes ordered and temporal structures, and excludes the transitive roles that real ontology languages need. Composition of relations is unavailable, so the relation algebra operations do not survive the restriction. Function symbols of arity greater than one cannot be used, since the term f(x,y) is admissible but nesting immediately requires a third name. The complexity is not low: NEXPTIME-completeness means the exponential-size models the theory guarantees are genuinely needed, and the guarded fragment, which is 2EXPTIME-complete but closed under higher arities, is the usual alternative when arity matters more than the exact bound.