Indiscernible Sequences for Lω₁ω

A sequence (aᵢ)_{i ∈ I} in a model M is Lω₁ω-indiscernible if for every n-variable formula and every two strictly increasing n-tuples from I, the formula holds on one iff it holds on the other.

Standalone API — does not advance the Hanf boundary.

def FirstOrder.Language.IsLomega1omegaIndiscernible {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] (a : I → M) : Prop

A sequence a : I → M is Lω₁ω-indiscernible if for every n-variable formula φ (no free variables) and every two strictly increasing maps s t : Fin n → I, the formula holds on a ∘ s iff on a ∘ t.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.IsLomega1omegaIndiscernibleOn {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] (a : I → M) (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : Prop

IsLomega1omegaIndiscernibleOn a Γ is the Γ-restricted form: the indiscernibility equivalence is required only for formulas whose sigma-pair lies in Γ ⊆ Σ n, L.BoundedFormulaω Empty n. Strictly weaker than IsLomega1omegaIndiscernible a (which is the Γ = Set.univ case).

Motivation: the EM pipeline only uses indiscernibility on the countable family Set.range s for a chosen formula enumeration s, not on all Lω₁ω formulas. Weakening to the restricted form lets callers supply the genuinely-needed hypothesis rather than the stronger full indiscernibility.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.restrict {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] {a : I → M} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (h : IsLomega1omegaIndiscernibleOn a Γ) {J : Type u_2} [LinearOrder J] (e : J ↪o I) : IsLomega1omegaIndiscernibleOn (a ∘ ⇑e) Γ

Restricting an On-indiscernible sequence to a sub-order preserves restricted indiscernibility on the same family.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.mono {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] {a : I → M} {Γ Γ' : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (hΓ : Γ ⊆ Γ') (h : IsLomega1omegaIndiscernibleOn a Γ') : IsLomega1omegaIndiscernibleOn a Γ

Monotonicity: shrinking the formula family preserves restricted indiscernibility.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.restrict {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) {J : Type u_2} [LinearOrder J] (e : J ↪o I) : IsLomega1omegaIndiscernible (a ∘ ⇑e)

Restricting an indiscernible sequence to a sub-order.