Documentation

TauCeti.ModelTheory.Infinitary.Sublanguage

Restricting infinitary formulas to symbol sublanguages #

A formula of L whose occurring symbols lie in F and R restricts to the symbol sublanguage symbSublang F R (BoundedFormulaInf.restrictSymbols), and translating the restriction back along the inclusion symbSublangIncl F R recovers the formula. At a countable carrier a formula mentions only countably many symbols (BoundedFormulaInf.functionsIn_countable), so the sublanguage of its own symbols has countably many symbols of each sort, whatever the size of L. Truth is unaffected: the restriction is realized in any structure on which the inclusion is an expansion, for instance in the reduct of an L-structure, or in an L-structure expanding a structure of the sublanguage (Mathlib's LHom.defaultExpansion with symbSublangIncl_injective), exactly when the formula is. This is how statements proved for countable languages reach sentences of arbitrary languages.

The restriction also pulls formulas back along an arbitrary language map g : L →ᴸ L': a formula of L' whose occurring symbols all lie in the range of g is the image under g of a formula of L. No injectivity of g is needed, since the inclusion of the sublanguage factors through g (LHom.exists_comp_eq_symbSublangIncl).

Main definitions #

Main results #

References #

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

The restriction of an infinitary formula to a symbol sublanguage containing its function and relation symbols.

Instances For
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.restrictSymbols_falsum {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {ι : Type uι} {α : Type uα} {n : ℕ} (hF : falsum.functionsIn ⊆ F) (hR : falsum.relationsIn ⊆ R) :
    falsum.restrictSymbols hF hR = falsum

    Restricting the false formula gives the false formula.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.restrictSymbols_equal {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {ι : Type uι} {α : Type uα} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) (hF : (equal t₁ t₂).functionsIn ⊆ F) (hR : (equal t₁ t₂).relationsIn ⊆ R) :
    (equal t₁ t₂).restrictSymbols hF hR = equal (t₁.restrictSymbols ⋯) (t₂.restrictSymbols ⋯)

    Restricting an equation restricts both sides.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.restrictSymbols_rel {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {ι : Type uι} {α : Type uα} {n l : ℕ} (r : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) (hF : (rel r ts).functionsIn ⊆ F) (hR : (rel r ts).relationsIn ⊆ R) :
    (rel r ts).restrictSymbols hF hR = rel ⟨r, ⋯⟩ fun (i : Fin l) => (ts i).restrictSymbols ⋯

    Restricting a relational atom restricts the relation symbol and every argument.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.restrictSymbols_imp {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {ι : Type uι} {α : Type uα} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) (hF : (φ.imp ψ).functionsIn ⊆ F) (hR : (φ.imp ψ).relationsIn ⊆ R) :
    (φ.imp ψ).restrictSymbols hF hR = (φ.restrictSymbols ⋯ ⋯).imp (ψ.restrictSymbols ⋯ ⋯)

    Restriction commutes with implication.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.restrictSymbols_all {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) (hF : φ.all.functionsIn ⊆ F) (hR : φ.all.relationsIn ⊆ R) :
    φ.all.restrictSymbols hF hR = (φ.restrictSymbols ⋯ ⋯).all

    Restriction commutes with universal quantification.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.restrictSymbols_iSup {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {ι : Type uι} {α : Type uα} {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) (hF : (iSup φs).functionsIn ⊆ F) (hR : (iSup φs).relationsIn ⊆ R) :
    (iSup φs).restrictSymbols hF hR = iSup fun (i : ι) => (φs i).restrictSymbols ⋯ ⋯

    Restriction commutes with disjunctions over the carrier.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.restrictSymbols_iInf {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {ι : Type uι} {α : Type uα} {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) (hF : (iInf φs).functionsIn ⊆ F) (hR : (iInf φs).relationsIn ⊆ R) :
    (iInf φs).restrictSymbols hF hR = iInf fun (i : ι) => (φs i).restrictSymbols ⋯ ⋯

    Restriction commutes with conjunctions over the carrier.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.onBoundedFormulaInf_restrictSymbols {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (hF : φ.functionsIn ⊆ F) (hR : φ.relationsIn ⊆ R) :
    (symbSublangIncl F R).onBoundedFormulaInf (φ.restrictSymbols hF hR) = φ

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

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_restrictSymbols {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {ι : Type uι} {α : Type uα} {M : Type w} [L.Structure M] [(symbSublang F R).Structure M] [(symbSublangIncl F R).IsExpansionOn M] {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (hF : φ.functionsIn ⊆ F) (hR : φ.relationsIn ⊆ R) (v : α → M) (xs : Fin n → M) :
    (φ.restrictSymbols hF hR).Realize v xs ↔ φ.Realize v xs

    Realization of a restriction. On a carrier where the L-structure expands the structure of the sublanguage along the inclusion, the restriction of a formula is realized exactly when the formula is. This applies to the reduct of an L-structure, through Mathlib's LHom.isExpansionOn_reduct.

    source
    theorem FirstOrder.Language.LHom.exists_eq_onBoundedFormulaInf_of_subset_range {L : Language} {L' : Language} (g : L →ᴸ L') {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L'.BoundedFormulaInf ι α n) (hF : φ.functionsIn ⊆ Set.range fun (s : (n : ℕ) × L.Functions n) => ⟨s.fst, g.onFunction s.snd⟩) (hR : φ.relationsIn ⊆ Set.range fun (s : (n : ℕ) × L.Relations n) => ⟨s.fst, g.onRelation s.snd⟩) :
    ∃ (ψ : L.BoundedFormulaInf ι α n), g.onBoundedFormulaInf ψ = φ

    Pulling a formula back along a language map. An infinitary formula of L' whose occurring function and relation symbols all lie in the range of g : L →ᴸ L' is the image under g of a formula of L. No injectivity of g is needed.