Documentation

TauCeti.ModelTheory.Sublanguage

Symbol sublanguages #

For a set F of function symbols and a set R of relation symbols of a language L, each tagged by its arity, symbSublang F R is the sublanguage of L whose symbols are exactly the members of F and R, and symbSublangIncl F R is its inclusion into L. The inclusion is injective, the sublanguage has countably many symbols of each sort when F and R are countable, and it is relational whenever L is relational or F is empty.

A term of L whose function symbols lie in F restricts to the sublanguage (Term.restrictSymbols), and translating the restriction back along the inclusion recovers the term. If every symbol of F and R lies in the range of a language map g : L →ᴸ L', the inclusion factors through g; no injectivity of g is needed, since a preimage is chosen for each symbol. The restriction of infinitary formulas lives in TauCeti.ModelTheory.Infinitary.Sublanguage.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev FirstOrder.Language.symbSublang {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) :
Language

The symbol sublanguage of L whose function and relation symbols of each arity are the members of F and R. The definition is reducible: a symbol of the sublanguage is a symbol of L together with a proof of membership, and is built and taken apart as such.

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 a symbol sublanguage into L.

    Instances For
      source
      @[simp]
      theorem FirstOrder.Language.symbSublangIncl_onFunction {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {n : ℕ} (f : (symbSublang F R).Functions n) :
      (symbSublangIncl F R).onFunction f = ↑f

      The inclusion sends a function symbol of the sublanguage to the underlying symbol of L.

      source
      @[simp]
      theorem FirstOrder.Language.symbSublangIncl_onRelation {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {n : ℕ} (r : (symbSublang F R).Relations n) :
      (symbSublangIncl F R).onRelation r = ↑r

      The inclusion sends a relation symbol of the sublanguage to the underlying symbol of L.

      source
      theorem FirstOrder.Language.symbSublangIncl_injective {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) :
      (symbSublangIncl F R).Injective

      The inclusion of a symbol sublanguage is injective.

      source
      instance FirstOrder.Language.countable_functions_symbSublang {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} [Countable ↑F] :
      Countable ((n : ℕ) × (symbSublang F R).Functions n)

      A symbol sublanguage with countably many function symbols has countably many function symbols, counted over all arities.

      source
      instance FirstOrder.Language.countable_relations_symbSublang {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} [Countable ↑R] :
      Countable ((n : ℕ) × (symbSublang F R).Relations n)

      A symbol sublanguage with countably many relation symbols has countably many relation symbols, counted over all arities.

      source
      instance FirstOrder.Language.isRelational_symbSublang {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} [L.IsRelational] :
      (symbSublang F R).IsRelational

      Any symbol sublanguage of a relational language is relational.

      source
      instance FirstOrder.Language.isRelational_symbSublang_of_isEmpty {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} [IsEmpty ↑F] :
      (symbSublang F R).IsRelational

      A symbol sublanguage with an empty set of function symbols is relational.

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

      The restriction of a term to a symbol sublanguage containing its function symbols.

      Instances For
        source
        @[simp]
        theorem FirstOrder.Language.Term.restrictSymbols_var {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {α : Type uα} (a : α) (h : (var a).functionsIn ⊆ F) :
        (var a).restrictSymbols h = var a

        Restricting a variable gives the same variable.

        source
        @[simp]
        theorem FirstOrder.Language.Term.restrictSymbols_func {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {α : Type uα} {n : ℕ} (f : L.Functions n) (ts : Fin n → L.Term α) (h : (func f ts).functionsIn ⊆ F) :
        (func f ts).restrictSymbols h = func ⟨f, ⋯⟩ fun (i : Fin n) => (ts i).restrictSymbols ⋯

        Restricting an application restricts the function symbol and every argument.

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

        The inclusion sends the restriction of a term back to the term.

        source
        theorem FirstOrder.Language.LHom.exists_comp_eq_symbSublangIncl {L : Language} {L' : Language} (g : L →ᴸ L') {F : Set ((n : ℕ) × L'.Functions n)} {R : Set ((n : ℕ) × L'.Relations n)} (hF : F ⊆ Set.range fun (s : (n : ℕ) × L.Functions n) => ⟨s.fst, g.onFunction s.snd⟩) (hR : R ⊆ Set.range fun (s : (n : ℕ) × L.Relations n) => ⟨s.fst, g.onRelation s.snd⟩) :
        ∃ (h : symbSublang F R →ᴸ L), g.comp h = symbSublangIncl F R

        If every symbol of F and R is the image of a symbol under g, the inclusion of the symbol sublanguage factors through g.