The Morley–Hanf theorem, discharged

The honest residual MorleySeedTailTemplateRealizable — the sole non-formal input of the realizability-only Morley–Hanf endpoint morley_hanf_of_tail_realizable — is PROVED by the schema route (morleySeed_tailTemplate_model_of_schemaSource): the ω-stage Marker/Henkin completion of the schema sentence universe, its quotient term model with the restricted truth lemma, the fully indiscernible sequence schemaSeq with pinned iSup/negative-iInf witnesses, and the cross-source acceptance through the Skolem-universality mixin. In fact the schema route consumes strictly LESS than the residual offers: the input sequence's tail indiscernibility is not used (seed template values are absolute).

morley_hanf_countable_symbols is the transparent countable-symbol intermediate. The definitive endpoint morley_hanf carries NO symbol-countability hypotheses: the construction runs in the simultaneous symbol-generated sublanguage of φ (symbSublang φ.functionsIn φ.relationsIn, both sorts countable because a formula mentions countably many symbols), and the resulting model is expanded back to L'[[J]] — missing functions act arbitrarily, missing relations as False, constants pass through; the degenerate IsEmpty J case is served by the source model itself. So: ℶ_{ω₁} is a Hanf bound for every L_{ω₁ω} sentence, unconditionally.

theorem FirstOrder.Language.morleySeedTailTemplateRealizable_of_countable_symbols {L' : Language} [Countable ((n : ℕ) × L'.Functions n)] [Countable ((n : ℕ) × L'.Relations n)] : MorleySeedTailTemplateRealizable

The honest Morley–Hanf residual, countable-symbol form: the tail-template theory of the Morley seed is realizable over every target order — by the schema-route construction, which does not even consume the sequence's tail indiscernibility. The transparent intermediate; the sublanguage reduction below removes the countability.

theorem FirstOrder.Language.morley_hanf_countable_symbols {L' : Language} [Countable ((n : ℕ) × L'.Functions n)] [Countable ((n : ℕ) × L'.Relations n)] (φ : L'.Sentenceω) : IsHanfBound φ (Cardinal.beth (Ordinal.omega 1))

The Morley–Hanf theorem for countable-symbol languages: ℶ_{ω₁} is a Hanf bound for every L_{ω₁ω} sentence over a language with countably many function and relation symbols, by seed-template realizability (the schema construction) alone — no extraction is consumed (an injective sequence is already seed-indiscernible, morleySeed_indiscernibleOn). The transparent intermediate to the assumption-free morley_hanf below.

Removing symbol countability: the two-sorted sublanguage reduction

@[reducible]

noncomputable def FirstOrder.Language.expandSymbStructure {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) (J : Type) {N : Type} [Nonempty N] [instN : ((symbSublang F R).withConstants J).Structure N] : (L.withConstants J).Structure N

Expansion of a two-sorted sublanguage [[J]]-structure to the full language: generating function symbols act as before, missing functions act arbitrarily (hence [Nonempty N]); generating relation symbols act as before, missing relations are False; constants pass through.

Equations

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

theorem FirstOrder.Language.realize_templateSentence_expandSymb {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} (J : Type) [LinearOrder J] {N : Type} [Nonempty N] [instN : ((symbSublang F R).withConstants J).Structure N] {n : ℕ} (ψ₀ : (symbSublang F R).BoundedFormulaω Empty n) (t : Fin n ↪o J) : (Lomega1omegaTemplate.templateSentence (BoundedFormulaω.mapLanguage (symbSublangIncl F R) ψ₀) t).Realize N ↔ (Lomega1omegaTemplate.templateSentence ψ₀ t).Realize N

Template sentences transfer along the two-sorted expansion — the symbSublang analogue of realize_templateSentence_expand: skeleton constants agree definitionally, and both symbol sorts peel off through the expansion property (dif_pos on the generating sets).

theorem FirstOrder.Language.morleySeedTailTemplateRealizable_holds {L' : Language} : MorleySeedTailTemplateRealizable

The honest Morley–Hanf residual holds — no symbol-countability assumptions: the schema construction runs in the simultaneous symbol-generated sublanguage of φ (both sorts countable, proved not assumed) at an injective ℕ-sequence of the source, and its model expands back to L'[[J]]; the degenerate IsEmpty J case is served by the source model itself.

theorem FirstOrder.Language.morley_hanf {L' : Language} (φ : L'.Sentenceω) : IsHanfBound φ (Cardinal.beth (Ordinal.omega 1))

The Morley–Hanf theorem: ℶ_{ω₁} is a Hanf bound for every L_{ω₁ω} sentence — over an arbitrary language, with no countability or other side hypotheses. If an L_{ω₁ω} sentence has a model of size at least ℶ_{ω₁}, it has models of arbitrarily large cardinality.