Substitution for bound positions of infinitary formulas

BoundedFormulaInf.substBounds σ φ replaces the bound position i of an infinitary formula φ with m bound positions by the term σ i, whose variables are the free variables α and k bound positions. Free variables are left in place. Past a quantifier the substitution is lifted by BoundedFormulaInf.liftSubst: the old positions of the substituted terms shift by Fin.castSucc, and the newly quantified position goes to the new last position, so no substituted term is captured by a binder.

Bound substitution generalizes the relabelling BoundedFormulaInf.mapBound, which substitutes bound positions for bound positions. It instantiates a formula with a bound position at a closed term (BoundedFormulaInf.inst), as the quantifier clauses of a consistency property require, and more generally instantiates the n bound positions of a formula at a tuple of terms.

Main definitions

• FirstOrder.Language.BoundedFormulaInf.liftSubst: a bound substitution lifted past a quantifier.
• FirstOrder.Language.BoundedFormulaInf.substBounds: substitution of terms for bound positions.
• FirstOrder.Language.BoundedFormulaInf.inst: instantiation of the single bound position of a formula at a term.

Main results

• FirstOrder.Language.BoundedFormulaInf.realize_substBounds: the substituted formula is realized at xs exactly when the original is realized at the values of the substituted terms.
• FirstOrder.Language.BoundedFormulaInf.substBounds_var and FirstOrder.Language.BoundedFormulaInf.substBounds_substBounds: identity and composition.
• FirstOrder.Language.BoundedFormulaInf.mapBound_eq_substBounds: relabelling is substitution of bound positions for bound positions.
• FirstOrder.Language.BoundedFormulaInf.inst_substBounds_liftSubst: instantiating the body of a quantified formula after substituting closed terms extends the tuple of substituted terms.
• FirstOrder.Language.BoundedFormulaInf.IsAtomic.substBounds: bound substitution keeps atomic formulas atomic.
• FirstOrder.Language.SentenceInf.realize_inst_of_realize_all and FirstOrder.Language.SentenceInf.realize_inst_of_realize_equal: a universal sentence implies its instances, and equal closed terms can be exchanged in an instance.
• FirstOrder.Language.LHom.onBoundedFormulaInf_substBounds: language maps commute with bound substitution.
• FirstOrder.Language.BoundedFormulaInf.relationsIn_substBounds, FirstOrder.Language.BoundedFormulaInf.functionsIn_subset_functionsIn_substBounds and FirstOrder.Language.BoundedFormulaInf.functionsIn_substBounds_subset: bound substitution keeps the relation symbols, keeps the function symbols, and adds at most the function symbols of the substituted terms.

References

• The construction follows Mathlib's finitary BoundedFormula.subst, which substitutes terms for free variables through Term.subst, with binders handled as in BoundedFormulaInf.mapBound.

def FirstOrder.Language.BoundedFormulaInf.liftSubst {L : Language} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) : Fin (m + 1) → L.Term (α ⊕ Fin (k + 1))

Lift a substitution for bound positions past a quantifier: each substituted term has its bound positions shifted by Fin.castSucc, and the newly quantified position goes to the new last position.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.liftSubst_castSucc {L : Language} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (i : Fin m) : liftSubst σ i.castSucc = Term.relabel (Sum.map id Fin.castSucc) (σ i)

A lifted substitution shifts the bound positions of each old substituted term.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.liftSubst_last {L : Language} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) : liftSubst σ (Fin.last m) = var (Sum.inr (Fin.last k))

A lifted substitution sends the newly quantified position to the new last position.

def FirstOrder.Language.BoundedFormulaInf.substBounds {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} : (Fin m → L.Term (α ⊕ Fin k)) → L.BoundedFormulaInf ι α m → L.BoundedFormulaInf ι α k

Substitute terms for the bound positions of an infinitary formula: bound position i is replaced by σ i, and free variables are kept. Past a quantifier, σ is lifted by liftSubst, so the substituted terms are not captured.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_falsum {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) : substBounds σ falsum = falsum

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_equal {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (t₁ t₂ : L.Term (α ⊕ Fin m)) : substBounds σ (equal t₁ t₂) = equal (t₁.subst (Sum.elim (var ∘ Sum.inl) σ)) (t₂.subst (Sum.elim (var ∘ Sum.inl) σ))

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_rel {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin m)) : substBounds σ (rel R ts) = rel R fun (i : Fin l) => (ts i).subst (Sum.elim (var ∘ Sum.inl) σ)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_imp {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ ψ : L.BoundedFormulaInf ι α m) : substBounds σ (φ.imp ψ) = (substBounds σ φ).imp (substBounds σ ψ)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_all {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ : L.BoundedFormulaInf ι α (m + 1)) : substBounds σ φ.all = (substBounds (liftSubst σ) φ).all

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_iSup {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φs : ι → L.BoundedFormulaInf ι α m) : substBounds σ (iSup φs) = iSup fun (i : ι) => substBounds σ (φs i)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_iInf {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φs : ι → L.BoundedFormulaInf ι α m) : substBounds σ (iInf φs) = iInf fun (i : ι) => substBounds σ (φs i)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_not {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ : L.BoundedFormulaInf ι α m) : substBounds σ φ.not = (substBounds σ φ).not

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_ex {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ : L.BoundedFormulaInf ι α (m + 1)) : substBounds σ φ.ex = (substBounds (liftSubst σ) φ).ex

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_bot {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) : substBounds σ ⊥ = ⊥

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_top {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) : substBounds σ ⊤ = ⊤

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_inf {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ ψ : L.BoundedFormulaInf ι α m) : substBounds σ (φ ⊓ ψ) = substBounds σ φ ⊓ substBounds σ ψ

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_sup {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ ψ : L.BoundedFormulaInf ι α m) : substBounds σ (φ ⊔ ψ) = substBounds σ φ ⊔ substBounds σ ψ

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_iff {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ ψ : L.BoundedFormulaInf ι α m) : substBounds σ (φ.iff ψ) = (substBounds σ φ).iff (substBounds σ ψ)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_substBounds {L : Language} {ι : Type uι} {α : Type uα} {M : Type w} [L.Structure M] {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ : L.BoundedFormulaInf ι α m) (v : α → M) (xs : Fin k → M) : (substBounds σ φ).Realize v xs ↔ φ.Realize v fun (i : Fin m) => Term.realize (Sum.elim v xs) (σ i)

Bound substitution is realization at the substituted values: the substituted formula is realized at xs exactly when the original is realized at the values of the substituted terms.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_var {L : Language} {ι : Type uι} {α : Type uα} {m : ℕ} (φ : L.BoundedFormulaInf ι α m) : substBounds (fun (i : Fin m) => var (Sum.inr i)) φ = φ

Substituting each bound position by itself is the identity.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.substBounds_substBounds {L : Language} {ι : Type uι} {α : Type uα} {m k l : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (τ : Fin k → L.Term (α ⊕ Fin l)) (φ : L.BoundedFormulaInf ι α m) : substBounds τ (substBounds σ φ) = substBounds (fun (i : Fin m) => (σ i).subst (Sum.elim (var ∘ Sum.inl) τ)) φ

Two successive bound substitutions are one: substitute σ, then τ into the terms of σ.

theorem FirstOrder.Language.BoundedFormulaInf.mapBound_eq_substBounds {L : Language} {ι : Type uι} {α : Type uα} {m n : ℕ} (f : Fin m → Fin n) (φ : L.BoundedFormulaInf ι α m) : mapBound f φ = substBounds (fun (i : Fin m) => var (Sum.inr (f i))) φ

Relabelling is bound substitution of bound positions for bound positions.

Instantiation

def FirstOrder.Language.BoundedFormulaInf.inst {L : Language} {ι : Type uι} {α : Type uα} (φ : L.BoundedFormulaInf ι α 1) (t : L.Term (α ⊕ Fin 0)) : L.FormulaInf ι α

Instantiate the single bound position of φ at the term t. For a sentence-level φ : L.BoundedFormulaInf ι Empty 1 and a closed term t, this is the sentence φ[t].

theorem FirstOrder.Language.BoundedFormulaInf.inst_def {L : Language} {ι : Type uι} {α : Type uα} (φ : L.BoundedFormulaInf ι α 1) (t : L.Term (α ⊕ Fin 0)) : φ.inst t = substBounds (fun (x : Fin 1) => t) φ

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_inst {L : Language} {ι : Type uι} {α : Type uα} {M : Type w} [L.Structure M] (φ : L.BoundedFormulaInf ι α 1) (t : L.Term (α ⊕ Fin 0)) (v : α → M) : (φ.inst t).Realize v ↔ φ.Realize v fun (x : Fin 1) => Term.realize (Sum.elim v default) t

An instance φ[t] holds exactly when φ holds at the value of t.

theorem FirstOrder.Language.BoundedFormulaInf.inst_substBounds_liftSubst {L : Language} {ι : Type uι} {α : Type uα} {n : ℕ} (σ : Fin n → L.Term (α ⊕ Fin 0)) (φ : L.BoundedFormulaInf ι α (n + 1)) (t : L.Term (α ⊕ Fin 0)) : (substBounds (liftSubst σ) φ).inst t = substBounds (Fin.snoc σ t) φ

Instantiating at t the body of a quantified formula whose outer bound positions were substituted by the closed terms σ substitutes the extended tuple Fin.snoc σ t.

theorem FirstOrder.Language.BoundedFormulaInf.IsAtomic.substBounds {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} {φ : L.BoundedFormulaInf ι α m} (h : φ.IsAtomic) (σ : Fin m → L.Term (α ⊕ Fin k)) : (BoundedFormulaInf.substBounds σ φ).IsAtomic

Bound substitution sends atomic formulas to atomic formulas.

Occurring symbols

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_substBounds {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ : L.BoundedFormulaInf ι α m) : (substBounds σ φ).relationsIn = φ.relationsIn

Bound substitution keeps exactly the relation symbols of the formula.

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_subset_functionsIn_substBounds {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ : L.BoundedFormulaInf ι α m) : φ.functionsIn ⊆ (substBounds σ φ).functionsIn

Bound substitution keeps every function symbol of the formula.

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_substBounds_subset {L : Language} {ι : Type uι} {α : Type uα} {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ : L.BoundedFormulaInf ι α m) : (substBounds σ φ).functionsIn ⊆ φ.functionsIn ∪ ⋃ (i : Fin m), (σ i).functionsIn

Bound substitution adds at most the function symbols of the substituted terms.

theorem FirstOrder.Language.SentenceInf.realize_inst_of_realize_all {L : Language} {ι : Type uι} {M : Type w} [L.Structure M] {φ : L.BoundedFormulaInf ι Empty 1} (h : Realize φ.all M) (t : L.Term (Empty ⊕ Fin 0)) : Realize (φ.inst t) M

A universal sentence implies its instance at every closed term.

theorem FirstOrder.Language.SentenceInf.realize_inst_of_realize_equal {L : Language} {ι : Type uι} {M : Type w} [L.Structure M] {t t' : L.Term (Empty ⊕ Fin 0)} {φ : L.BoundedFormulaInf ι Empty 1} (ht : Realize (BoundedFormulaInf.equal t t') M) (hφ : Realize (φ.inst t) M) : Realize (φ.inst t') M

Substitution of equals: if the closed terms t and t' are equal in M, the instance of φ at t' holds whenever the instance at t does.

@[simp]

theorem FirstOrder.Language.LHom.onBoundedFormulaInf_substBounds {L : Language} {L' : Language} {ι : Type uι} {α : Type uα} (g : L →ᴸ L') {m k : ℕ} (σ : Fin m → L.Term (α ⊕ Fin k)) (φ : L.BoundedFormulaInf ι α m) : g.onBoundedFormulaInf (BoundedFormulaInf.substBounds σ φ) = BoundedFormulaInf.substBounds (fun (i : Fin m) => g.onTerm (σ i)) (g.onBoundedFormulaInf φ)

Language maps commute with bound substitution, acting on the substituted terms.