Two-Variable Logic

Origin. Mortimer (1975) proved decidability. FO² — first-order with only two variables. Reuse variables via requantification. NEXPTIME-complete. Foundation for description logic complexity.

Models. Only variables x, y available. Must reuse: ∃x∀y∃x... Variables rebind. Scott normal form. Decidable satisfiability.

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) α: universal part, β: existential witness.

Counting extension C²: ∃≥ₙx.φ: at least n witnesses. Still decidable (NEXPTIME).

With equivalence: FO² with equivalence relations. Decidable with care.

Graded extension: ∃≥ₙ, ∃≤ₙ quantifiers. Captures number restrictions in DL.

Symbols.

Symbol	Unicode	Name	Meaning
FO²	—	Two-variable	Fragment
C²	—	Counting	With counting
∃≥ₙ	—	At least n	Counting quantifier
x, y	—	Variables	Only two

Metatheory. Decidable (Mortimer). NEXPTIME-complete. Finite model property. Small model property. Extends to counting.

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

Limitations. Only two variables. Limited expressiveness. Complex encoding of natural statements. Extensions delicate.