Documentation

TauCeti.ModelTheory.Infinitary.FreeVarSupport

The free-variable support of an infinitary formula #

The free-variable support φ.freeVarSupport of an infinitary formula φ is the set of free variables occurring in one of its atoms. It is a set rather than a Finset: an infinitary conjunction or disjunction may mention infinitely many free variables, one in each branch. For a finitary formula it is the coercion of Mathlib's BoundedFormula.freeVarFinset, and over a countable carrier, in particular in L_{ω₁ω}, it is countable.

The main result realize_congr_freeVarSupport says that the realization of a formula depends only on the values of the free-variable valuation on the support. This is the infinitary analogue of the finitary fact that a formula only sees the variables it mentions.

Main definitions #

Main results #

References #

source
noncomputable def FirstOrder.Language.BoundedFormulaInf.freeVarSupport {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} :
L.BoundedFormulaInf ι α n → Set α

The free-variable support of an infinitary formula: the set of free variables that occur in one of its atoms. Infinitary connectives take the union over all their branches, so the support may be infinite.

Instances For

    Defining equations #

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_falsum {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} :
    falsum.freeVarSupport = ∅

    The false formula has no free variables.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_equal {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} [DecidableEq α] (t₁ t₂ : L.Term (α ⊕ Fin n)) :
    (equal t₁ t₂).freeVarSupport = ↑t₁.varFinsetLeft ∪ ↑t₂.varFinsetLeft

    The free variables of an equation are those of its two terms.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_rel {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} [DecidableEq α] {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) :
    (rel R ts).freeVarSupport = ⋃ (i : Fin l), ↑(ts i).varFinsetLeft

    The free variables of a relational atom are those of its argument terms.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_imp {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) :
    (φ.imp ψ).freeVarSupport = φ.freeVarSupport ∪ ψ.freeVarSupport

    The free variables of an implication are those of either side.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_all {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) :
    φ.all.freeVarSupport = φ.freeVarSupport

    Universal quantification binds a slot, not a free variable, so it keeps the support.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_iSup {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) :
    (iSup φs).freeVarSupport = ⋃ (i : ι), (φs i).freeVarSupport

    The free variables of a disjunction over the carrier are those of its branches.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_iInf {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) :
    (iInf φs).freeVarSupport = ⋃ (i : ι), (φs i).freeVarSupport

    The free variables of a conjunction over the carrier are those of its branches.

    Derived connectives #

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_not {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) :
    φ.not.freeVarSupport = φ.freeVarSupport

    Negation keeps the support.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_bot {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} :
    ⊥.freeVarSupport = ∅

    ⊥ has no free variables.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_top {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} :
    ⊤.freeVarSupport = ∅

    ⊤ has no free variables.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_inf {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) :
    (φ ⊓ ψ).freeVarSupport = φ.freeVarSupport ∪ ψ.freeVarSupport

    The free variables of φ ⊓ ψ are those of φ or ψ.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_sup {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) :
    (φ ⊔ ψ).freeVarSupport = φ.freeVarSupport ∪ ψ.freeVarSupport

    The free variables of φ ⊔ ψ are those of φ or ψ.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_iff {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) :
    (φ.iff ψ).freeVarSupport = φ.freeVarSupport ∪ ψ.freeVarSupport

    The free variables of φ.iff ψ are those of φ or ψ.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_ex {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) :
    φ.ex.freeVarSupport = φ.freeVarSupport

    Existential quantification keeps the support.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_alls {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) :
    freeVarSupport φ.alls = φ.freeVarSupport

    Universally closing the bound-variable slots keeps the support.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_exs {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) :
    freeVarSupport φ.exs = φ.freeVarSupport

    Existentially closing the bound-variable slots keeps the support.

    Bound-variable relabelling, weakening and carrier transport #

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_mapBound {L : Language} {α : Type u'} {ι : Type uι} {n m : ℕ} (f : Fin m → Fin n) (φ : L.BoundedFormulaInf ι α m) :
    (mapBound f φ).freeVarSupport = φ.freeVarSupport

    Relabelling the bound-variable slots keeps the support.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_castLE {L : Language} {α : Type u'} {ι : Type uι} {n m : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaInf ι α m) :
    (castLE h φ).freeVarSupport = φ.freeVarSupport

    Weakening keeps the support.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_iInfAlong {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} {κ : Type uκ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) :
    (iInfAlong c φs).freeVarSupport = ⋃ (i : ι), (φs i).freeVarSupport

    The support of a coded conjunction is the union of the supports of its conjuncts: the padding ⊤ has no free variables.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_iSupAlong {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} {κ : Type uκ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) :
    (iSupAlong c φs).freeVarSupport = ⋃ (i : ι), (φs i).freeVarSupport

    The support of a coded disjunction is the union of the supports of its disjuncts: the padding ⊥ has no free variables.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.freeVarSupport_reindex {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} {κ : Type uκ} (c : TauCeti.IndexCoding ι κ) (φ : L.BoundedFormulaInf ι α n) :
    (reindex c φ).freeVarSupport = φ.freeVarSupport

    Transporting a formula along a coding of its carrier keeps the support.

    Countability #

    source
    theorem FirstOrder.Language.BoundedFormulaInf.countable_freeVarSupport {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} [Countable ι] (φ : L.BoundedFormulaInf ι α n) :
    φ.freeVarSupport.Countable

    Over a countable carrier, in particular in L_{ω₁ω}, an infinitary formula has countably many free variables.

    Realization depends only on the support #

    source
    theorem FirstOrder.Language.BoundedFormulaInf.realize_congr_freeVarSupport {L : Language} {α : Type u'} {ι : Type uι} {n : ℕ} {M : Type w} [L.Structure M] {φ : L.BoundedFormulaInf ι α n} {v v' : α → M} (h : Set.EqOn v v' φ.freeVarSupport) (xs : Fin n → M) :
    φ.Realize v xs ↔ φ.Realize v' xs

    Realization depends only on the free-variable support: two valuations of the free variables that agree on φ.freeVarSupport realize φ at the same bound-variable valuations.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.freeVarSupport_toInf {L : Language} {α : Type u'} [DecidableEq α] {ι : Type uι} {n : ℕ} (φ : L.BoundedFormula α n) :
    φ.toInf.freeVarSupport = ↑φ.freeVarFinset

    On a finitary formula, embedded at any carrier, the free-variable support is the coercion of Mathlib's BoundedFormula.freeVarFinset. In particular it is finite.

    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.freeVarSupport_subst {L : FirstOrder.Language} {ι : Type uι} {α : Type u'} {β : Type uβ} {n : ℕ} [DecidableEq β] (φ : L.BoundedFormulaInf ι α n) (f : α → L.Term β) :
    (subst φ f).freeVarSupport = ⋃ a ∈ φ.freeVarSupport, ↑(f a).varFinset

    The support after substitution is the union of the variables of the terms substituted for the free variables in the support.

    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.freeVarSupport_relabel {L : FirstOrder.Language} {ι : Type uι} {α : Type u'} {β : Type uβ} {n m : ℕ} (g : α → β ⊕ Fin m) (φ : L.BoundedFormulaInf ι α n) :
    (relabel g φ).freeVarSupport = Sum.inl ⁻¹' g '' φ.freeVarSupport

    The support after relabelling consists of the free variables b such that g sends a variable of the original support to Sum.inl b. Variables sent to new bound slots drop out.