Ehrenfeucht–Mostowski templates for Lω₁ω

Lomega1omegaTemplate L assigns a truth value to every bounded Lω₁ω formula in every arity. The downstream EM modules construct templates from indiscernible sequences and develop their realization 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