The function-generated sublanguage of an L_{ω₁ω} formula

Countability plumbing for the Morley–Hanf chain: the local EM tower requires countably many function symbols, but the honest residual statements assume only countably many relation symbols. This file removes the gap: every L_{ω₁ω} formula mentions only countably many function symbols (functionsIn + functionsIn_countable — formulas are countably-branching well-founded trees), so the construction can run in the generated sublanguage funSublang F (the mentioned functions as a subtype, ALL relations kept — their countability is ambient), and the formula restricts to it (restrictFuns) with mapLanguage (funSublangIncl F) as a left inverse. Downstream (LocalEMOmegaResidual.lean) the sublanguage EM model is expanded back to the full language.

Pure syntax + set-countability; no EM, no local stack, no Conditional/.

Function symbols mentioned by a term / formula

def FirstOrder.Language.Term.functionsIn {L : Language} {α : Type} : L.Term α → Set ((n : ℕ) × L.Functions n)

The function symbols occurring in a term.

Equations

• (FirstOrder.Language.var a).functionsIn = ∅
• (FirstOrder.Language.func f ts).functionsIn = insert ⟨l, f⟩ (⋃ (i : Fin l), (ts i).functionsIn)

theorem FirstOrder.Language.Term.functionsIn_countable {L : Language} {α : Type} (t : L.Term α) : t.functionsIn.Countable

def FirstOrder.Language.BoundedFormulaω.functionsIn {L : Language} {α : Type} {n : ℕ} : L.BoundedFormulaω α n → Set ((n : ℕ) × L.Functions n)

The function symbols occurring in a formula (through all countable connectives).

Equations

• FirstOrder.Language.BoundedFormulaω.falsum.functionsIn = ∅
• (FirstOrder.Language.BoundedFormulaω.equal t u).functionsIn = t.functionsIn ∪ u.functionsIn
• (FirstOrder.Language.BoundedFormulaω.rel R ts).functionsIn = ⋃ (i : Fin l), (ts i).functionsIn
• (φ.imp ψ).functionsIn = φ.functionsIn ∪ ψ.functionsIn
• φ.all.functionsIn = φ.functionsIn
• (FirstOrder.Language.BoundedFormulaω.iSup φs).functionsIn = ⋃ (i : ℕ), (φs i).functionsIn
• (FirstOrder.Language.BoundedFormulaω.iInf φs).functionsIn = ⋃ (i : ℕ), (φs i).functionsIn

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_countable {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : φ.functionsIn.Countable

The generated sublanguage

def FirstOrder.Language.funSublang {L : Language} (F : Set ((n : ℕ) × L.Functions n)) : Language

The sublanguage of L generated by a set F of function symbols: the functions of F (as a subtype) and all of L's relations. Keeping the relations whole means relation-symbol countability transports from L unchanged, and only the function side — the one the local EM tower needs and the honest residuals do not assume — is cut down to F.

Equations

• FirstOrder.Language.funSublang F = { Functions := fun (n : ℕ) => { f : L.Functions n // ⟨n, f⟩ ∈ F }, Relations := fun (n : ℕ) => L.Relations n }

def FirstOrder.Language.funSublangIncl {L : Language} (F : Set ((n : ℕ) × L.Functions n)) : funSublang F →ᴸ L

The inclusion of the generated sublanguage.

Equations

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

theorem FirstOrder.Language.funSublang_fun_countable {L : Language} {F : Set ((n : ℕ) × L.Functions n)} (hF : F.Countable) : Countable ((n : ℕ) × (funSublang F).Functions n)

The generated sublanguage of a countable symbol set has countably many function symbols — the certificate the local EM tower needs, now provable rather than assumed.

theorem FirstOrder.Language.funSublang_rel_countable {L : Language} (F : Set ((n : ℕ) × L.Functions n)) [h : Countable ((l : ℕ) × L.Relations l)] : Countable ((l : ℕ) × (funSublang F).Relations l)

Relation-symbol countability transports to the generated sublanguage (definitionally the same relation symbols).

Restriction of terms and formulas into the generated sublanguage

def FirstOrder.Language.Term.restrictFuns {L : Language} {α : Type} {F : Set ((n : ℕ) × L.Functions n)} (t : L.Term α) : t.functionsIn ⊆ F → (funSublang F).Term α

Restrict a term whose function symbols lie in F to the generated sublanguage.

Equations

• (FirstOrder.Language.var x_2).restrictFuns x_3 = FirstOrder.Language.var x_2
• (FirstOrder.Language.func f ts).restrictFuns h = FirstOrder.Language.func ⟨f, ⋯⟩ fun (i : Fin l) => (ts i).restrictFuns ⋯

theorem FirstOrder.Language.Term.onTerm_restrictFuns {L : Language} {α : Type} {F : Set ((n : ℕ) × L.Functions n)} (t : L.Term α) (h : t.functionsIn ⊆ F) : (funSublangIncl F).onTerm (t.restrictFuns h) = t

The inclusion is a left inverse of term restriction.

def FirstOrder.Language.BoundedFormulaω.restrictFuns {L : Language} {α : Type} {F : Set ((n : ℕ) × L.Functions n)} {n : ℕ} (φ : L.BoundedFormulaω α n) : φ.functionsIn ⊆ F → (funSublang F).BoundedFormulaω α n

Restrict a formula whose function symbols lie in F to the generated sublanguage (relations pass through unchanged).

Equations

• FirstOrder.Language.BoundedFormulaω.falsum.restrictFuns x_4 = FirstOrder.Language.BoundedFormulaω.falsum
• (FirstOrder.Language.BoundedFormulaω.equal t u).restrictFuns h = FirstOrder.Language.BoundedFormulaω.equal (t.restrictFuns ⋯) (u.restrictFuns ⋯)
• (FirstOrder.Language.BoundedFormulaω.rel R ts).restrictFuns h = FirstOrder.Language.BoundedFormulaω.rel R fun (i : Fin l) => (ts i).restrictFuns ⋯
• (φ.imp ψ).restrictFuns h = (φ.restrictFuns ⋯).imp (ψ.restrictFuns ⋯)
• φ.all.restrictFuns h = (φ.restrictFuns h).all
• (FirstOrder.Language.BoundedFormulaω.iSup φs).restrictFuns h = FirstOrder.Language.BoundedFormulaω.iSup fun (i : ℕ) => (φs i).restrictFuns ⋯
• (FirstOrder.Language.BoundedFormulaω.iInf φs).restrictFuns h = FirstOrder.Language.BoundedFormulaω.iInf fun (i : ℕ) => (φs i).restrictFuns ⋯

theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_restrictFuns {L : Language} {α : Type} {F : Set ((n : ℕ) × L.Functions n)} {n : ℕ} (φ : L.BoundedFormulaω α n) (h : φ.functionsIn ⊆ F) : mapLanguage (funSublangIncl F) (φ.restrictFuns h) = φ

The inclusion is a left inverse of formula restriction: the restricted formula maps back to the original. The bridge that lets the sublanguage EM model realize the original formulas.

The simultaneous symbol-generated sublanguage

The schema route needs BOTH symbol sorts countable (its completion enumerates atoms over the relation symbols too), while the definitive Morley–Hanf endpoint assumes neither. So alongside the function-only sublanguage above, this section cuts BOTH sorts down to the (countable) symbols a formula mentions: relationsIn + countability, the two-sorted symbSublang, its inclusion, restriction restrictSymbols, and the left-inverse law.

def FirstOrder.Language.BoundedFormulaω.relationsIn {L : Language} {α : Type} {n : ℕ} : L.BoundedFormulaω α n → Set ((n : ℕ) × L.Relations n)

The relation symbols occurring in a formula (through all countable connectives).

Equations

• FirstOrder.Language.BoundedFormulaω.falsum.relationsIn = ∅
• (FirstOrder.Language.BoundedFormulaω.equal t u).relationsIn = ∅
• (FirstOrder.Language.BoundedFormulaω.rel R ts).relationsIn = {⟨l, R⟩}
• (φ.imp ψ).relationsIn = φ.relationsIn ∪ ψ.relationsIn
• φ.all.relationsIn = φ.relationsIn
• (FirstOrder.Language.BoundedFormulaω.iSup φs).relationsIn = ⋃ (i : ℕ), (φs i).relationsIn
• (FirstOrder.Language.BoundedFormulaω.iInf φs).relationsIn = ⋃ (i : ℕ), (φs i).relationsIn

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_countable {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : φ.relationsIn.Countable

def FirstOrder.Language.symbSublang {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) : Language

The sublanguage of L generated by a set F of function symbols AND a set R of relation symbols, both as subtypes.

Equations

• FirstOrder.Language.symbSublang F R = { Functions := fun (n : ℕ) => { f : L.Functions n // ⟨n, f⟩ ∈ F }, Relations := fun (n : ℕ) => { r : L.Relations n // ⟨n, r⟩ ∈ R } }

def FirstOrder.Language.symbSublangIncl {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) : symbSublang F R →ᴸ L

The inclusion of the two-sorted generated sublanguage.

Equations

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

theorem FirstOrder.Language.symbSublang_fun_countable {L : Language} {F : Set ((n : ℕ) × L.Functions n)} (hF : F.Countable) (R : Set ((n : ℕ) × L.Relations n)) : Countable ((n : ℕ) × (symbSublang F R).Functions n)

Function-symbol countability of the two-sorted generated sublanguage.

theorem FirstOrder.Language.symbSublang_rel_countable {L : Language} (F : Set ((n : ℕ) × L.Functions n)) {R : Set ((n : ℕ) × L.Relations n)} (hR : R.Countable) : Countable ((n : ℕ) × (symbSublang F R).Relations n)

Relation-symbol countability of the two-sorted generated sublanguage.

def FirstOrder.Language.Term.restrictSymbols {L : Language} {α : Type} {F : Set ((n : ℕ) × L.Functions n)} (R : Set ((n : ℕ) × L.Relations n)) (t : L.Term α) : t.functionsIn ⊆ F → (symbSublang F R).Term α

Restrict a term whose function symbols lie in F to the two-sorted sublanguage.

Equations

• FirstOrder.Language.Term.restrictSymbols R (FirstOrder.Language.var x_2) x_3 = FirstOrder.Language.var x_2
• FirstOrder.Language.Term.restrictSymbols R (FirstOrder.Language.func f ts) h = FirstOrder.Language.func ⟨f, ⋯⟩ fun (i : Fin l) => FirstOrder.Language.Term.restrictSymbols R (ts i) ⋯

theorem FirstOrder.Language.Term.onTerm_restrictSymbols {L : Language} {α : Type} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} (t : L.Term α) (h : t.functionsIn ⊆ F) : (symbSublangIncl F R).onTerm (restrictSymbols R t h) = t

The inclusion is a left inverse of two-sorted term restriction.

def FirstOrder.Language.BoundedFormulaω.restrictSymbols {L : Language} {α : Type} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {n : ℕ} (φ : L.BoundedFormulaω α n) : φ.functionsIn ⊆ F → φ.relationsIn ⊆ R → (symbSublang F R).BoundedFormulaω α n

Restrict a formula whose function AND relation symbols lie in F/R to the two-sorted generated sublanguage.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.BoundedFormulaω.falsum.restrictSymbols x_5 x_6 = FirstOrder.Language.BoundedFormulaω.falsum
• (FirstOrder.Language.BoundedFormulaω.rel Rl ts).restrictSymbols hF hR = FirstOrder.Language.BoundedFormulaω.rel ⟨Rl, ⋯⟩ fun (i : Fin l) => FirstOrder.Language.Term.restrictSymbols R (ts i) ⋯
• (φ.imp ψ).restrictSymbols hF hR = (φ.restrictSymbols ⋯ ⋯).imp (ψ.restrictSymbols ⋯ ⋯)
• φ.all.restrictSymbols hF hR = (φ.restrictSymbols hF hR).all
• (FirstOrder.Language.BoundedFormulaω.iSup φs).restrictSymbols hF hR = FirstOrder.Language.BoundedFormulaω.iSup fun (i : ℕ) => (φs i).restrictSymbols ⋯ ⋯
• (FirstOrder.Language.BoundedFormulaω.iInf φs).restrictSymbols hF hR = FirstOrder.Language.BoundedFormulaω.iInf fun (i : ℕ) => (φs i).restrictSymbols ⋯ ⋯

theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_restrictSymbols {L : Language} {α : Type} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {n : ℕ} (φ : L.BoundedFormulaω α n) (hF : φ.functionsIn ⊆ F) (hR : φ.relationsIn ⊆ R) : mapLanguage (symbSublangIncl F R) (φ.restrictSymbols hF hR) = φ

The inclusion is a left inverse of two-sorted formula restriction.

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_restrictSymbols {L : Language} {α : Type} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} (s : Bool) {n : ℕ} (φ : L.BoundedFormulaω α n) (hF : φ.functionsIn ⊆ F) (hR : φ.relationsIn ⊆ R) : universalSigned s (φ.restrictSymbols hF hR) ↔ universalSigned s φ

Restriction preserves the quantifier class. No new induction: restriction is inverted by the inclusion language map, and language maps transport the signed class exactly.