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!