Ehrenfeucht–Mostowski templates for Lω₁ω

This file introduces the intermediate object that bridges Lω₁ω-indiscernible sequences and Ehrenfeucht–Mostowski (EM) stretching: a template assigns to each n and each formula φ : L.BoundedFormulaω Empty n the truth value of φ on increasing n-tuples drawn from an indiscernible sequence. A second sequence b : J → N realizes the template if its truth values on increasing tuples agree with the template's.

Main definitions

• Lomega1omegaTemplate L: a template for an Lω₁ω formula language L, i.e. an assignment φ ↦ Prop for every φ : L.BoundedFormulaω Empty n.
• Lomega1omegaTemplate.RealizesOn T b: a sequence b : J → N realizes the template T if every formula's truth value on every strictly increasing tuple from J agrees with T φ.
• IsLomega1omegaIndiscernible.template: the template induced by an indiscernible sequence, defined existentially (so well-defined without any extra assumption on the index set).

Main results

• IsLomega1omegaIndiscernible.template_truth_iff: well-definedness — the template's value at φ agrees with φ.Realize (a ∘ s) for any strictly increasing tuple s. Uses iff_realize from Indiscernible.lean.
• IsLomega1omegaIndiscernible.realizesTemplate: an indiscernible sequence realizes its own template.
• IsLomega1omegaIndiscernible.realizesTemplate_restrict: restricting the index set along an order embedding still realizes the same template.
• IsLomega1omegaIndiscernible.template_reindex: reindexing along an order isomorphism produces a definitionally equal template.

This file does not prove anything about EM stretching itself; it only sets up the template object and its basic invariance properties.

structure FirstOrder.Language.Lomega1omegaTemplate (L : Language) : Type (max u v)

A template for the language L of Lω₁ω formulas: an assignment of a truth value to every Lω₁ω formula in every arity, with no free variables. Intended to record the "common truth value on increasing n-tuples" of an indiscernible sequence.

• truth {n : ℕ} : L.BoundedFormulaω Empty n → Prop

  The truth value assigned to a formula.

theorem FirstOrder.Language.Lomega1omegaTemplate.ext {L : Language} {x y : L.Lomega1omegaTemplate} (truth : @truth L x = @truth L y) : x = y

theorem FirstOrder.Language.Lomega1omegaTemplate.ext_iff {L : Language} {x y : L.Lomega1omegaTemplate} : x = y ↔ @truth L x = @truth L y

def FirstOrder.Language.Lomega1omegaTemplate.RealizesOn {L : Language} {N : Type u_1} [L.Structure N] {J : Type u_2} [LinearOrder J] (T : L.Lomega1omegaTemplate) (b : J → N) : Prop

A sequence b : J → N realizes a template T if for every formula φ and every strictly increasing n-tuple t : Fin n → J, the truth value of φ on b ∘ t agrees with T.truth φ.

Equations

• T.RealizesOn b = ∀ {n : ℕ} (φ : L.BoundedFormulaω Empty n) {t : Fin n → J}, StrictMono t → (T.truth φ ↔ φ.Realize Empty.elim (b ∘ t))

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

Template associated with a bare sequence a : I → M — same body as IsLomega1omegaIndiscernible.template but without the indiscernibility hypothesis (the existing definition discards that hypothesis in its data anyway). Used by the restricted-indiscernibility API (_on variants).

Equations

• FirstOrder.Language.templateOfSeq a = { truth := fun {n : ℕ} (φ : L.BoundedFormulaω Empty n) => ∃ (s : Fin n → I), StrictMono s ∧ φ.Realize Empty.elim (a ∘ s) }

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

The template induced by an indiscernible sequence: the truth value at φ is the existential statement that some strictly increasing n-tuple in I makes φ true. By indiscernibility (see template_truth_iff) this is equivalent to "every such tuple makes φ true", and to "any specific witness makes φ true".

Equations

• x✝.template = { truth := fun {n : ℕ} (φ : L.BoundedFormulaω Empty n) => ∃ (s : Fin n → I), StrictMono s ∧ φ.Realize Empty.elim (a ∘ s) }

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.template_eq_templateOfSeq {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) : h.template = templateOfSeq a

The hypothesis-bearing template equals the bare templateOfSeq. Proof is rfl because the existing template discards its indiscernibility argument in its data.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.template_truth_iff {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 : Fin n → I} (hs : StrictMono s) : h.template.truth φ ↔ φ.Realize Empty.elim (a ∘ s)

Well-definedness of template: the template's value at φ equals the truth value of φ on any specific strictly increasing tuple. This is the existential-vs-universal collapse provided by indiscernibility.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.realizesTemplate {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) : h.template.RealizesOn a

An indiscernible sequence realizes its own template.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.realizesTemplate_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) : h.template.RealizesOn (a ∘ ⇑e)

Restricting an indiscernible sequence to a sub-order along an order embedding e : J ↪o I produces a sequence that realizes the same template as the original. (The template object is built from h, not h.restrict e.)

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.realizesTemplate_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) : h.template.RealizesOn (a ∘ ⇑e)

Reindexing an indiscernible sequence by an order isomorphism e : J ≃o I produces a sequence that realizes the same template.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.template_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) : ⋯.template = h.template

Reindexing an indiscernible sequence by an order isomorphism produces a template equal to the original. (Restricting along a non-surjective order embedding generally does not produce an equal template — only the realisation direction is preserved; see realizesTemplate_restrict.)

Restricted-indiscernibility API for templateOfSeq

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.templateOfSeq_truth_iff {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 : Fin n → I} (hs : StrictMono s) : (templateOfSeq a).truth φ ↔ φ.Realize Empty.elim (a ∘ s)

Restricted template_truth_iff: the templateOfSeq's value at a formula φ ∈ Γ equals the truth value of φ on any strictly-increasing tuple, provided the source sequence is restricted-indiscernible on Γ.

This mirrors IsLomega1omegaIndiscernible.template_truth_iff but uses the weaker IsLomega1omegaIndiscernibleOn hypothesis and compares against templateOfSeq a (the hypothesis-free template).