Symbols occurring in infinitary formulas

BoundedFormulaInf.functionsIn and BoundedFormulaInf.relationsIn record the symbols occurring in a formula, tagged by arity. Equality contributes only the function symbols of its terms: it is a logical symbol. At a countable branching carrier both sets are countable, with no restriction on the size of the language. This is the input for restricting a sentence to a countable sublanguage.

BoundedFormulaInf.realize_congr_of_agreeOn is symbol locality: two interpretations on one carrier which agree on the occurring symbols give the formula the same truth value. Language maps take occurrence sets to their exact images; bound-variable and free-variable relabelling and carrier coding preserve them, and free-variable substitution preserves relation symbols and adds at most the function symbols of the substituted terms.

def FirstOrder.Language.BoundedFormulaInf.functionsIn {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} : L.BoundedFormulaInf ι α n → Set ((k : ℕ) × L.Functions k)

The function symbols occurring in an infinitary formula, tagged by arity.

def FirstOrder.Language.BoundedFormulaInf.relationsIn {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} : L.BoundedFormulaInf ι α n → Set ((k : ℕ) × L.Relations k)

The relation symbols occurring in an infinitary formula, tagged by arity. Logical equality does not contribute a relation symbol.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_falsum {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} : falsum.functionsIn = ∅

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_equal {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : (equal t₁ t₂).functionsIn = t₁.functionsIn ∪ t₂.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_rel {L : Language} {ι : Type uι} {α : Type uα} {n k : ℕ} (R : L.Relations k) (ts : Fin k → L.Term (α ⊕ Fin n)) : (rel R ts).functionsIn = ⋃ (i : Fin k), (ts i).functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_imp {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : (φ.imp ψ).functionsIn = φ.functionsIn ∪ ψ.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_all {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) : φ.all.functionsIn = φ.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_iSup {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) : (iSup φs).functionsIn = ⋃ (i : ι), (φs i).functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_iInf {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) : (iInf φs).functionsIn = ⋃ (i : ι), (φs i).functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_not {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : φ.not.functionsIn = φ.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_bot {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} : ⊥.functionsIn = ∅

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_top {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} : ⊤.functionsIn = ∅

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_inf {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : (φ ⊓ ψ).functionsIn = φ.functionsIn ∪ ψ.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_sup {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : (φ ⊔ ψ).functionsIn = φ.functionsIn ∪ ψ.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_iff {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : (φ.iff ψ).functionsIn = φ.functionsIn ∪ ψ.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_ex {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) : φ.ex.functionsIn = φ.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_alls {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : functionsIn φ.alls = φ.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_exs {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : functionsIn φ.exs = φ.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_exsLast {L : Language} {ι : Type uι} {α : Type uα} {n k : ℕ} (φ : L.BoundedFormulaInf ι α (n + k)) : φ.exsLast.functionsIn = φ.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_falsum {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} : falsum.relationsIn = ∅

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_equal {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : (equal t₁ t₂).relationsIn = ∅

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_rel {L : Language} {ι : Type uι} {α : Type uα} {n k : ℕ} (R : L.Relations k) (ts : Fin k → L.Term (α ⊕ Fin n)) : (rel R ts).relationsIn = {⟨k, R⟩}

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_imp {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : (φ.imp ψ).relationsIn = φ.relationsIn ∪ ψ.relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_all {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) : φ.all.relationsIn = φ.relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_iSup {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) : (iSup φs).relationsIn = ⋃ (i : ι), (φs i).relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_iInf {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) : (iInf φs).relationsIn = ⋃ (i : ι), (φs i).relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_not {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : φ.not.relationsIn = φ.relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_bot {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} : ⊥.relationsIn = ∅

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_top {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} : ⊤.relationsIn = ∅

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_inf {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : (φ ⊓ ψ).relationsIn = φ.relationsIn ∪ ψ.relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_sup {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : (φ ⊔ ψ).relationsIn = φ.relationsIn ∪ ψ.relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_iff {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : (φ.iff ψ).relationsIn = φ.relationsIn ∪ ψ.relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_ex {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) : φ.ex.relationsIn = φ.relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_alls {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : relationsIn φ.alls = φ.relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_exs {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) : relationsIn φ.exs = φ.relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_exsLast {L : Language} {ι : Type uι} {α : Type uα} {n k : ℕ} (φ : L.BoundedFormulaInf ι α (n + k)) : φ.exsLast.relationsIn = φ.relationsIn

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_countable {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} [Countable ι] (φ : L.BoundedFormulaInf ι α n) : φ.functionsIn.Countable

At a countable branching carrier the set of occurring function symbols is countable.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_mapBound {L : Language} {ι : Type uι} {α : Type uα} {n m : ℕ} (f : Fin m → Fin n) (φ : L.BoundedFormulaInf ι α m) : (mapBound f φ).functionsIn = φ.functionsIn

Relabelling bound positions preserves the occurring function symbols.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_castLE {L : Language} {ι : Type uι} {α : Type uα} {n m : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaInf ι α m) : (castLE h φ).functionsIn = φ.functionsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_iInfAlong {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} {κ : Type uκ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) : (iInfAlong c φs).functionsIn = ⋃ (i : ι), (φs i).functionsIn

Coded conjunction adds no symbols through its padding.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_iSupAlong {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} {κ : Type uκ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) : (iSupAlong c φs).functionsIn = ⋃ (i : ι), (φs i).functionsIn

Coded disjunction adds no symbols through its padding.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_reindex {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} {κ : Type uκ} (c : TauCeti.IndexCoding ι κ) (φ : L.BoundedFormulaInf ι α n) : (reindex c φ).functionsIn = φ.functionsIn

Changing the branching carrier by a coding preserves occurrence sets.

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_countable {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} [Countable ι] (φ : L.BoundedFormulaInf ι α n) : φ.relationsIn.Countable

At a countable branching carrier the set of occurring relation symbols is countable.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_mapBound {L : Language} {ι : Type uι} {α : Type uα} {n m : ℕ} (f : Fin m → Fin n) (φ : L.BoundedFormulaInf ι α m) : (mapBound f φ).relationsIn = φ.relationsIn

Relabelling bound positions preserves the occurring relation symbols.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_castLE {L : Language} {ι : Type uι} {α : Type uα} {n m : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaInf ι α m) : (castLE h φ).relationsIn = φ.relationsIn

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_iInfAlong {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} {κ : Type uκ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) : (iInfAlong c φs).relationsIn = ⋃ (i : ι), (φs i).relationsIn

Coded conjunction adds no symbols through its padding.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_iSupAlong {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} {κ : Type uκ} (c : TauCeti.IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) : (iSupAlong c φs).relationsIn = ⋃ (i : ι), (φs i).relationsIn

Coded disjunction adds no symbols through its padding.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_reindex {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} {κ : Type uκ} (c : TauCeti.IndexCoding ι κ) (φ : L.BoundedFormulaInf ι α n) : (reindex c φ).relationsIn = φ.relationsIn

Changing the branching carrier by a coding preserves occurrence sets.

theorem FirstOrder.Language.BoundedFormulaInf.realize_congr_of_agreeOn {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} {M : Type w} (φ : L.BoundedFormulaInf ι α n) (S S' : L.Structure M) (hF : ∀ {k : ℕ} (f : L.Functions k), ⟨k, f⟩ ∈ φ.functionsIn → ∀ (xs : Fin k → M), Structure.funMap f xs = Structure.funMap f xs) (hR : ∀ {k : ℕ} (R : L.Relations k), ⟨k, R⟩ ∈ φ.relationsIn → ∀ (xs : Fin k → M), Structure.RelMap R xs ↔ Structure.RelMap R xs) (v : α → M) (xs : Fin n → M) : φ.Realize v xs ↔ φ.Realize v xs

Symbol locality. Structures on the same carrier which agree on every symbol occurring in a formula give it the same realization. No agreement on other symbols is required.

@[simp]

theorem FirstOrder.Language.LHom.functionsIn_onBoundedFormulaInf {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (g : L →ᴸ L') (φ : L.BoundedFormulaInf ι α n) : (g.onBoundedFormulaInf φ).functionsIn = (fun (s : (k : ℕ) × L.Functions k) => ⟨s.fst, g.onFunction s.snd⟩) '' φ.functionsIn

Language translation takes the occurring function symbols to their exact image.

@[simp]

theorem FirstOrder.Language.LHom.relationsIn_onBoundedFormulaInf {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (g : L →ᴸ L') (φ : L.BoundedFormulaInf ι α n) : (g.onBoundedFormulaInf φ).relationsIn = (fun (s : (k : ℕ) × L.Relations k) => ⟨s.fst, g.onRelation s.snd⟩) '' φ.relationsIn

Language translation takes the occurring relation symbols to their exact image.

@[simp]

theorem TauCeti.BoundedFormulaInf.functionsIn_relabel {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φ : L.BoundedFormulaInf ι α n) : (relabel g φ).functionsIn = φ.functionsIn

Free-variable relabelling preserves the occurring function symbols.

@[simp]

theorem TauCeti.BoundedFormulaInf.relationsIn_relabel {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φ : L.BoundedFormulaInf ι α n) : (relabel g φ).relationsIn = φ.relationsIn

Free-variable relabelling preserves the occurring relation symbols.

theorem TauCeti.BoundedFormulaInf.functionsIn_subset_functionsIn_subst {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (f : α → L.Term β) : φ.functionsIn ⊆ (subst φ f).functionsIn

Free-variable substitution keeps every function symbol of the formula.

theorem TauCeti.BoundedFormulaInf.functionsIn_subst_subset {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (f : α → L.Term β) : (subst φ f).functionsIn ⊆ φ.functionsIn ∪ ⋃ (a : α), (f a).functionsIn

Free-variable substitution adds at most the function symbols of the substituted terms.

@[simp]

theorem TauCeti.BoundedFormulaInf.relationsIn_subst {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (f : α → L.Term β) : (subst φ f).relationsIn = φ.relationsIn

Free-variable substitution preserves the occurring relation symbols.