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.IsLomega1omegaIndiscernible.toOn {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : IsLomega1omegaIndiscernibleOn a Γ

Full indiscernibility implies restricted indiscernibility on any family.

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.reindex {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) Γ

Reindexing an On-indiscernible sequence by an order isomorphism 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.IsLomega1omegaIndiscernibleOn.iff_realize {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 Γ) {n : ℕ} (φ : L.BoundedFormulaω Empty n) (hφ : ⟨n, φ⟩ ∈ Γ) {s t : Fin n → I} (hs : StrictMono s) (ht : StrictMono t) : φ.Realize Empty.elim (a ∘ s) ↔ φ.Realize Empty.elim (a ∘ t)

Restricted form of the calling-convention lemma: the restricted indiscernibility hypothesis restated with the formula preceding the tuples.

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.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.unary_const {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) (φ : L.BoundedFormulaω Empty 1) (i j : I) : (φ.Realize Empty.elim fun (x : Fin 1) => a i) ↔ φ.Realize Empty.elim fun (x : Fin 1) => a j

For a 1-variable formula, truth is the same at any two indices.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.iff_realize {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) {n : ℕ} (φ : L.BoundedFormulaω Empty n) {s t : Fin n → I} (hs : StrictMono s) (ht : StrictMono t) : φ.Realize Empty.elim (a ∘ s) ↔ φ.Realize Empty.elim (a ∘ t)

The indiscernibility hypothesis, restated with the formula φ preceding the tuples (a more natural calling convention than the universal form used by the underlying definition).

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.iff_realize_of_orderEmbedding {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) {n : ℕ} (φ : L.BoundedFormulaω Empty n) (s t : Fin n ↪o I) : φ.Realize Empty.elim (a ∘ ⇑s) ↔ φ.Realize Empty.elim (a ∘ ⇑t)

The indiscernibility hypothesis, stated for bundled increasing tuples s t : Fin n ↪o I. This is the natural form for working with order embeddings of Fin n into the index set.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.reindex {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)

Pre-composing an indiscernible sequence by an order isomorphism yields an indiscernible sequence. A direct corollary of restrict via OrderIso.toOrderEmbedding.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.pair_const {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) (φ : L.BoundedFormulaω Empty 2) {i₁ i₂ j₁ j₂ : I} (hi : i₁ < i₂) (hj : j₁ < j₂) : φ.Realize Empty.elim (a ∘ ![i₁, i₂]) ↔ φ.Realize Empty.elim (a ∘ ![j₁, j₂])

For a 2-variable formula, truth is the same on any two strictly increasing pairs from the indiscernible sequence. The binary analogue of unary_const.