Documentation

LeanPool.InfinitaryLogic.Methods.EM.FragmentAdapter

EM Realization: the compactness-oracle layer #

The endpoints that take EM template theories from finite satisfiability to a model, by applying a supplied Theoryω.OrdinaryCompactness oracle.

An EM template theory is built from an arbitrary s : ℕ → Σ n, L.BoundedFormulaω Empty n, so its sentences lie in an arbitrary fragment: there is no fragment-specific fact to appeal to, and no admissible module is imported here.

The oracle is genuinely an assumption — full Lω₁ω compactness for L[[J]] fails in general. Realization.lean's model-input endpoints are the honest residual beneath it: they take the model itself, and the oracle factors through them.

Stretching along an arbitrary target order #

These theorems package the existing templateTheoryOfSeq pipeline into caller-ready form: from an indiscernible template they produce a target L[[J]]-structure N whose constants satisfy the template on formulas in Set.range s (the countable family named by the enumeration s). The target order J is an arbitrary linear order — including uncountable target orders, which is where Morley–Hanf cardinality amplification lives.

Two forms are provided:

Scope: these theorems do NOT claim full IsLomega1omegaIndiscernible for any extracted sequence — that would require enumerating all Lω₁ω formulas, which is not currently formalized. They DO allow uncountable J, which is what cardinality amplification for MorleyHanfTransfer eventually needs; the residual step is extracting an indiscernible source sequence of length I ≥ ℶ_ω₁ from a large model (the Erdős–Rado half, not addressed here).

source
theorem FirstOrder.Language.realize_templateSentence_of_structure {L : Language} {J : Type u} [LinearOrder J] {N : Type u_1} [(L.withConstants J).Structure N] {n : ℕ} (φ : L.BoundedFormulaω Empty n) (t : Fin n ↪o J) :
(Lomega1omegaTemplate.templateSentence φ t).Realize N ↔ φ.Realize Empty.elim fun (i : Fin n) => Term.realize Empty.elim (func (Sum.inr (t i)) Fin.elim0)

Generalized realize_templateSentence.

Like realize_templateSentence (InfinitaryLogic/Methods/EM/Realization.lean:97), but takes an arbitrary [L[[J]].Structure N] instead of requiring the L[[J]]-structure to be built from a specific σ : J → M via constantsOn.structure σ. The L-structure on N is derived from the L[[J]]-structure via the canonical reduct along lhomWithConstants L J.

The right-hand side realizes φ on the sequence fun i => b (t i), where b j is the closed-term realization of the constant symbol Sum.inr j (i.e., the interpretation of the J-indexed constant in the given L[[J]]-structure on N).

Morley–Hanf-oriented corollaries #

source
def FirstOrder.Language.disEqFormula {L : Language} :
L.BoundedFormulaω Empty 2

The 2-ary Lω₁ω disequality formula x₀ ≠ x₁.

Equations
Instances For
    source
    def FirstOrder.Language.morleySeed {L : Language} (φ : L.Sentenceω) :
    ℕ → (n : ℕ) × L.BoundedFormulaω Empty n

    The Morley seed of a sentence φ: the concrete two-formula family the Morley–Hanf tail bridge feeds the EM machinery — φ itself, the disequality x₀ ≠ x₁, and repeated φ-filler. The honest tail-template residual quantifies over exactly this seed (MorleySeedTailTemplateRealizable in Conditional/MorleyHanfTransfer.lean), NOT over arbitrary formula sequences: an arbitrary sequence can enumerate {Pᵢ x}ᵢ ∪ {⋀ᵢ Pᵢ x} against a "height" model, whose tail template is finitely satisfiable but unsatisfiable — a genuine L_{ω₁ω} compactness failure.

    Equations
    Instances For
      source
      theorem FirstOrder.Language.morleySeed_indiscernibleOn {L : Language} {M : Type u_1} [L.Structure M] (φ : L.Sentenceω) {a : ℕ → M} (ha : ∀ (i j : ℕ), i ≠ j → a i ≠ a j) :
      IsLomega1omegaIndiscernibleOn a (Set.range (morleySeed φ))

      The Morley seed needs no extraction: ANY pairwise-distinct sequence is fully Lω₁ω-indiscernible on Set.range (morleySeed φ) — the arity-0 members ignore their tuples, and the disequality is true on every strictly monotone pair of a pairwise-distinct sequence. This is why the definitive Morley–Hanf route consumes no Ramsey/Erdős–Rado extraction at all: Infinite.natEmbedding already supplies a seed-indiscernible sequence.

      Restricted-indiscernibility variants #

      These _on theorems take IsLomega1omegaIndiscernibleOn a (Set.range s) instead of the full IsLomega1omegaIndiscernible a, and state their conclusions against (templateOfSeq a).truth rather than h.template.truth.