Template-to-L[[J]]-theory bridge for Lω₁ω

For each Lω₁ω template T : Lomega1omegaTemplate L and each linearly ordered index type J, this file builds the set of L[[J]]-sentences whose models are exactly the L[[J]]-structures whose constants realize T. The bridge consists of:

• templateSentence φ t: the L[[J]]-sentence "φ holds on the constants indexed by the increasing tuple t : Fin n ↪o J".
• realize_templateSentence: the semantic bridge — realizing templateSentence φ t in an L[[J]]-expansion of an L-structure M (built from a function σ : J → M) is equivalent to realizing the underlying Lω₁ω formula φ on the tuple σ ∘ t.
• templateTheory T J: the set of L[[J]]-sentences obtained by including, for each (n, φ, t), either templateSentence φ t (if T.truth φ) or its negation (if ¬ T.truth φ).
• IsLomega1omegaIndiscernible.templateTheory_finitelySatisfiable: when the template comes from an indiscernible sequence indexed by an infinite linear order, every finite subset of the resulting template theory is satisfiable in the source model.

This file does not turn the template into a single model — that step is blocked both by uncountable J (the language L[[J]] has uncountably many constant symbols) and, even for countable J, by the fact that templateTheory T J inherits the continuum size of the Lω₁ω formula syntax. Any future model-realizing tranche will need to restrict to a countable sub-theory.

Section 1: a Fin n order-embedding into any infinite linear order

theorem FirstOrder.Language.Fin.exists_orderEmbedding_of_infinite {I : Type u_1} [LinearOrder I] [Infinite I] (n : ℕ) : Nonempty (Fin n ↪o I)

Any infinite linear order admits a strictly-increasing tuple of every finite length. Constructed by sorting n distinct elements obtained from Infinite.natEmbedding.

theorem FirstOrder.Language.Fin.countable_orderEmbedding (n : ℕ) {J : Type u_1} [LinearOrder J] [Countable J] : Countable (Fin n ↪o J)

Fin n ↪o J is countable whenever J is countable. The injection from Fin n ↪o J to Fin n → J via DFunLike.coe is injective (by DFunLike.coe_injective), and Fin n → J is countable when J is countable because Fin n is finite.

Section 2: templateSentence — the L[[J]]-sentence "φ on the constants of t"

def FirstOrder.Language.Lomega1omegaTemplate.templateSentence {L : Language} {J : Type u} [LinearOrder J] {n : ℕ} (φ : L.BoundedFormulaω Empty n) (t : Fin n ↪o J) : (L.withConstants J).Sentenceω

The L[[J]]-sentence expressing "φ holds when its n bound variables are interpreted as the constants c_{t 0}, …, c_{t (n-1)}". Built by lifting φ to L[[J]], opening its bound variables, and substituting them with the closed terms for the constants t 0, …, t (n-1).

Equations

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

Section 3: realize_templateSentence — semantic bridge to φ.Realize

theorem FirstOrder.Language.realize_templateSentence {L : Language} {M : Type u_1} [L.Structure M] {J : Type u} [LinearOrder J] (σ : J → M) {n : ℕ} (φ : L.BoundedFormulaω Empty n) (t : Fin n ↪o J) : (Lomega1omegaTemplate.templateSentence φ t).Realize M ↔ φ.Realize Empty.elim (σ ∘ ⇑t)

Realizing templateSentence φ t in an L[[J]]-expansion of M (built from a function σ : J → M via constantsOn.structure σ) is equivalent to realizing φ itself on the tuple σ ∘ t : Fin n → M. The proof composes realize_subst, realize_openBounds, and realize_mapLanguage.

Section 4: templateTheory — the L[[J]]-theory pinning down the template

def FirstOrder.Language.Lomega1omegaTemplate.templateTheory {L : Language} (T : L.Lomega1omegaTemplate) (J : Type u) [LinearOrder J] : Set (L.withConstants J).Sentenceω

The L[[J]]-theory whose models are exactly the L[[J]]-structures whose constants realize the template T. For each formula φ and each increasing tuple t : Fin n ↪o J, the theory contains either templateSentence φ t (if T.truth φ) or its negation (if ¬ T.truth φ). Both directions are needed: without the negative sentences, a model could realize formulas the template declares false.

Equations

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

def FirstOrder.Language.Lomega1omegaTemplate.templateTheoryOn {L : Language} (T : L.Lomega1omegaTemplate) (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) (J : Type u) [LinearOrder J] : Set (L.withConstants J).Sentenceω

The restricted template theory: like templateTheory, but only includes sentences for formulas whose (arity, φ)-pair lies in the family Γ. When Γ and J are both countable, the resulting theory is countable (see templateTheoryOn_countable), making it a candidate input to model_existence — which the full templateTheory can never be.

Equations

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

theorem FirstOrder.Language.Lomega1omegaTemplate.templateTheoryOn_subset_templateTheory {L : Language} (T : L.Lomega1omegaTemplate) (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) (J : Type u) [LinearOrder J] : T.templateTheoryOn Γ J ⊆ T.templateTheory J

Monotonicity: the restricted template theory is a subset of the full template theory.

theorem FirstOrder.Language.Lomega1omegaTemplate.templateTheoryOn_mono {L : Language} (T : L.Lomega1omegaTemplate) {Γ Γ' : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (hΓ : Γ ⊆ Γ') (J : Type u) [LinearOrder J] : T.templateTheoryOn Γ J ⊆ T.templateTheoryOn Γ' J

Monotonicity of templateTheoryOn in the formula family Γ: enlarging Γ can only enlarge the restricted template theory.

theorem FirstOrder.Language.Lomega1omegaTemplate.templateTheoryOn_countable {L : Language} {T : L.Lomega1omegaTemplate} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (hΓ : Γ.Countable) {J : Type u} [LinearOrder J] [Countable J] : (T.templateTheoryOn Γ J).Countable

When the family Γ and the index type J are both countable, the restricted template theory is countable. This is the point of templateTheoryOn: the full templateTheory T J is always continuum-sized (Lω₁ω formulas form a continuum), but the restricted theory can be countable and thus a candidate input to model_existence.

Section 5: finite satisfiability of templateTheory in the source model

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.templateTheory_finitelySatisfiable {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type u_1} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) {J : Type u} [LinearOrder J] {F : Set (L.withConstants J).Sentenceω} (hFin : F.Finite) (hSub : F ⊆ h.template.templateTheory J) : ∃ (σ : J → M), ∀ τ ∈ F, τ.Realize M

If h : IsLomega1omegaIndiscernible a for a : I → M over an infinite linear order I, then every finite subset of templateTheory h.template J is satisfiable in the source model M, expanded to an L[[J]]-structure via an appropriate interpretation σ : J → M. The interpretation is built by sorting the finitely many J-indices appearing in the finite fragment, embedding them into I via [Infinite I], and pulling them through a.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.templateTheoryOn_finitelySatisfiable {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type u_1} [L.Structure M] {a : I → M} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (h : IsLomega1omegaIndiscernibleOn a Γ) {J : Type u} [LinearOrder J] {F : Set (L.withConstants J).Sentenceω} (hFin : F.Finite) (hSub : F ⊆ (templateOfSeq a).templateTheoryOn Γ J) : ∃ (σ : J → M), ∀ τ ∈ F, τ.Realize M

Restricted-indiscernibility variant of templateTheory_finitelySatisfiable: every finite subset of (templateOfSeq a).templateTheoryOn Γ J is satisfiable in the source model, provided a is restricted-indiscernible on Γ (not on all formulas).

This is a fresh specialized proof, not a delegation through the full-indiscernibility version: the witness extraction explicitly carries ⟨n, φ⟩ ∈ Γ so that the weaker templateOfSeq_truth_iff applies at the final step. The σ/Finset plumbing is identical to the full version at lines 208-295; only the witness-extraction step (Step 2) and the final template_truth_iff calls (Step 5) differ.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.templateTheoryOn_finitelySatisfiable {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type u_1} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) {J : Type u} [LinearOrder J] (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) {F : Set (L.withConstants J).Sentenceω} (hFin : F.Finite) (hSub : F ⊆ h.template.templateTheoryOn Γ J) : ∃ (σ : J → M), ∀ τ ∈ F, τ.Realize M

Restricted version of templateTheory_finitelySatisfiable: every finite subset of h.template.templateTheoryOn Γ J is satisfiable in the source model. This is a direct corollary via templateTheoryOn_subset_templateTheory; the point of stating it separately is that this is the form a downstream model-existence call will actually invoke (since only the restricted theory can ever be countable).

Section 7: sequence-indexed wrappers

Convenience wrappers over templateTheoryOn specialized to a family given as a sequence s : ℕ → Σ n, L.BoundedFormulaω Empty n. The payoff is ergonomic: the countability of Set.range s is automatic, so templateTheoryOfSeq_countable drops the Γ.Countable hypothesis that templateTheoryOn_countable requires.

def FirstOrder.Language.Lomega1omegaTemplate.templateTheoryOfSeq {L : Language} (T : L.Lomega1omegaTemplate) (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (J : Type u) [LinearOrder J] : Set (L.withConstants J).Sentenceω

Sequence-based restricted template theory: same content as templateTheoryOn T (Set.range s) J, with a dedicated name for callers that want to hand a sequence rather than a set.

Equations

• T.templateTheoryOfSeq s J = T.templateTheoryOn (Set.range s) J

theorem FirstOrder.Language.Lomega1omegaTemplate.templateTheoryOfSeq_countable {L : Language} {J : Type u} [LinearOrder J] {T : L.Lomega1omegaTemplate} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) [Countable J] : (T.templateTheoryOfSeq s J).Countable

templateTheoryOfSeq is countable whenever J is countable. Follows from templateTheoryOn_countable via Set.countable_range; the countability of the family comes for free from the sequence structure.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.templateTheoryOfSeq_finitelySatisfiable {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type u_1} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) {J : Type u} [LinearOrder J] (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) {F : Set (L.withConstants J).Sentenceω} (hFin : F.Finite) (hSub : F ⊆ h.template.templateTheoryOfSeq s J) : ∃ (σ : J → M), ∀ τ ∈ F, τ.Realize M

Sequence-indexed finite satisfiability in the source indiscernible model. Direct delegation to templateTheoryOn_finitelySatisfiable.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.templateTheoryOfSeq_finitelySatisfiable {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type u_1} [L.Structure M] {a : I → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (h : IsLomega1omegaIndiscernibleOn a (Set.range s)) {J : Type u} [LinearOrder J] {F : Set (L.withConstants J).Sentenceω} (hFin : F.Finite) (hSub : F ⊆ (templateOfSeq a).templateTheoryOfSeq s J) : ∃ (σ : J → M), ∀ τ ∈ F, τ.Realize M

Sequence-indexed wrapper for templateTheoryOn_finitelySatisfiable under restricted indiscernibility.