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

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.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.

Section 5: finite satisfiability of templateTheory in the source model

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