Documentation

LeanPool.InfinitaryLogic.Methods.GeneratedSublanguage

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 #

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

The function symbols occurring in a term.

Equations
Instances For
    source
    theorem FirstOrder.Language.Term.functionsIn_countable {L : Language} {α : Type} (t : L.Term α) :
    t.functionsIn.Countable
    source
    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
    Instances For
      source
      theorem FirstOrder.Language.BoundedFormulaω.functionsIn_countable {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) :
      φ.functionsIn.Countable

      The generated sublanguage #

      Restriction of terms and formulas into the generated sublanguage #

      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.

      source
      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
      Instances For
        source
        theorem FirstOrder.Language.BoundedFormulaω.relationsIn_countable {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) :
        φ.relationsIn.Countable
        source
        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
        Instances For
          source
          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.
          Instances For
            source
            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.

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

            source
            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
            Instances For
              source
              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
              Instances For
                source
                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.

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