Ehrenfeucht-Fraïssé theorem
ID: ehrenfeucht-fraisse-theorem
For a finite relational first-order language, with finitely many constants allowed, the Duplicator wins the -round game exactly when the structures are rank-n equivalent. Game-winning implies rank equivalence in arbitrary languages; the converse needs a finiteness condition and can fail even for an infinite unary vocabulary. Over a finite relational vocabulary, winning every announced finite horizon is equivalent to elementary equivalence.
New to topics? Read the docs here!