Constant instances

This neutral module defines the two closing operations by the auxiliary constants of L[[ℕ]]:

• instConst c ψ — open the single bound variable of ψ : BoundedFormulaω Empty 1 and substitute the constant c_c;
• closeBy φ τ — open all n bound variables of φ : BoundedFormulaω Empty n and substitute the constants c_{τ i}.

def FirstOrder.Language.instConst {L : Language} (c : ℕ) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : (L.withConstants ℕ).Sentenceω

The constant instance ψ(c): open the bound variable of ψ and substitute the constant c_c.

Equations

• FirstOrder.Language.instConst c ψ = FirstOrder.Language.BoundedFormulaω.subst ψ.openBounds fun (x : Fin 1) => FirstOrder.Language.constTerm c

noncomputable def FirstOrder.Language.closeBy {L : Language} {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω Empty n) (τ : Fin n → ℕ) : (L.withConstants ℕ).Sentenceω

The closing substitution of a bounded formula by constants.

Equations

• FirstOrder.Language.closeBy φ τ = FirstOrder.Language.BoundedFormulaω.subst φ.openBounds fun (i : Fin n) => FirstOrder.Language.constTerm (τ i)