FirstOrder.Language.Substructure.isElementary_of_exists

theorem FirstOrder.Language.Substructure.isElementary_of_exists : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.Substructure M), (∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥S) (a : M), φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)) → S.IsElementary

The Tarski-Vaught test for elementarity of a substructure theorem, in the context of first-order languages, states that for any language `L`, any type `M` that has a structure instance `inst` in `L`, and any substructure `S` of `M`, if for all natural numbers `n`, all bounded formulas `φ` of `L` that have `n + 1` variables, and all functions `x` mapping from a `n`-sized finite set to elements of `S`, and any element `a` of `M`, if the formula `φ` holds true when we append `a` to the end of the sequence generated by `x`, then there exists an element `b` in `S` such that the formula `φ` also holds true when we append the element `b` to the end of the same sequence. If this condition is satisfied, then `S` is an elementary substructure of `M`.

More concisely: If for all bounded formulas with `n+1` variables in a first-order language `L` and for all functions mapping from an `n`-sized finite set to `M` and all elements `a` in `M`, if `φ(x\_1, ..., x\_n, a)` holds in `M`, then there exists `b` in `S` such that `φ(x\_1, ..., x\_n, b)` also holds in `M`, then `S` is an elementary substructure of `M`.