Elementary Equivalence

Origin. Tarski's notion of arithmetical equivalence (1936) and its development with Vaught (1957); Fraïssé's back-and-forth characterization (1954) and Ehrenfeucht's game formulation (1961), which made the relation checkable. Same first-order theory. Indistinguishable by FOL. Ehrenfeucht-Fraïssé games. Foundation for model comparison.

Models. Structures satisfy same sentences. Isomorphism implies, not converse. Game characterization. Back-and-forth systems.

Formalism.

Definition: M ≡ N iff for all φ ∈ FOL: M ⊨ φ iff N ⊨ φ. Same first-order theory.

Isomorphism implies: M ≅ N → M ≡ N Isomorphic structures equivalent. Converse fails!

Counterexample: (ℚ, <) ≡ (ℝ, <) Both dense linear orders without endpoints. Not isomorphic (cardinality).

Ehrenfeucht-Fraïssé games: EF_n(M, N): n-round game. Spoiler picks element in one structure. Duplicator responds in other. Duplicator wins if partial isomorphism.

Game theorem: M ≡ N iff Duplicator wins EF_n for all n. Finite approximations.

n-equivalence: M ≡_n N: same sentences up to quantifier rank n. Duplicator wins n rounds. Finer classification.

Back-and-forth: Set of partial isomorphisms. Forth: extend in M. Back: extend in N. Existence implies equivalence.

Types: tp(a/M) = {φ(x) : M ⊨ φ(a)} Type of element. Realized types match in equivalent structures.

Symbols.

Symbol	Unicode	Name	Meaning
≡	U+2261	Equiv	Same theory
≅	U+2245	Isomorphic	Same structure
≡_n	—	n-equiv	Rank n
EF_n	—	Game	n rounds

Metatheory. EF games characterize equivalence. Decidability via games. Quantifier elimination connections. Preservation theorems.

Applies to. Model comparison. Decidability proofs. Database query equivalence. Descriptive complexity.

Limitations. Only first-order. Infinite games. Higher-order distinguishes more.