Documentation

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 #

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

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

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

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

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

                      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.