Constant instances: instConst, closeBy, and their substitution algebra

The two closing operations by the auxiliary constants of L[[ℕ]], in a neutral module below both the interpolation layer and the countable-completion kernel:

• 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}.

Their semantic consumer lemmas (realize_instConst, realize_closeBy, …) stay in the modules that own the structures they realize in. This module holds only syntax: the connective/universal algebra of closeBy — how it commutes with the connectives, what the arity-one remainder of a closed universal is, and that the constant instance of that remainder is closeBy at the extended tuple. Atomic template lemmas (closing an equality or relation template gives constEq / relInst) belong with those atoms, above this module.

The public surface is deliberately small: instConst, closeBy, the closeBy_* commutations, closeBy_zero, instConst_eq_closeBy, instConst_closeBy_all_remainder, and the generic substitution laws Term.subst_subst / Term.subst_relabel / Term.relabel_subst / BoundedFormulaω.subst_subst. Everything else is proof scaffolding and is private.

The all case

closeBy φ.all τ is (remainder).all, where the remainder is φ opened, relabeled so that the last bound variable stays bound, and closed by τ. The instance of that remainder at a constant c must be closeBy φ (Fin.snoc τ c) — this is what makes universal-instance closure of a constants-expanded universe follow from a fragment's all_mem. Proving it directly fights castLE inside BoundedFormulaω.relabel, so instead:

• a private closeWith ρ φ closes bound variables by a term assignment ρ, by structural recursion with no relabel of formulas; it depends on ρ only pointwise and composes;
• one private bridge lemma identifies ((openBounds φ).relabel g).subst τ' with a closeWith for the standard splitting g, using the two relabel-composition lemmas of Operations.lean;
• closeBy, its remainder, and instConst are then all closeWiths, and instConst_closeBy_all_remainder is the composition law plus a pointwise check.

Term-level substitution algebra

theorem FirstOrder.Language.Term.subst_subst {L : Language} {α β γ : Type u'} (t : L.Term α) (f : α → L.Term β) (g : β → L.Term γ) : (t.subst f).subst g = t.subst fun (a : α) => (f a).subst g

Substituting after substituting is substituting the composite.

theorem FirstOrder.Language.Term.subst_relabel {L : Language} {α β γ : Type u'} (t : L.Term α) (f : α → β) (g : β → L.Term γ) : (relabel f t).subst g = t.subst (g ∘ f)

Substituting after relabeling is substituting along the relabeling.

theorem FirstOrder.Language.Term.relabel_subst {L : Language} {α β γ : Type u'} (t : L.Term α) (f : α → L.Term β) (g : β → γ) : relabel g (t.subst f) = t.subst fun (a : α) => relabel g (f a)

Relabeling after substituting is substituting the relabeled terms.

theorem FirstOrder.Language.Term.subst_var_eq {L : Language} {α : Type u'} (t : L.Term α) : t.subst var = t

Substituting variables for themselves does nothing.

Formula-level substitution composition

theorem FirstOrder.Language.BoundedFormulaω.subst_subst {L : Language} {α β γ : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) (f : α → L.Term β) (g : β → L.Term γ) : (φ.subst f).subst g = φ.subst fun (a : α) => (f a).subst g

Composition of substitutions: substituting f and then g is substituting a ↦ (f a).subst g. No side condition: subst never touches bound variables.

The closing operations

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)

Definitional commutations of closeBy

Each holds by unfolding openBounds and subst on the constructor. The all case exhibits the arity-one remainder explicitly; relating its instConst to closeBy at the extended parameter tuple is a separate lemma about openBounds, proved where it is consumed.

@[simp]

theorem FirstOrder.Language.closeBy_falsum {L : Language} {n : ℕ} (τ : Fin n → ℕ) : closeBy BoundedFormulaω.falsum τ = BoundedFormulaω.falsum

@[simp]

theorem FirstOrder.Language.closeBy_imp {L : Language} {n : ℕ} (φ ψ : (L.withConstants ℕ).BoundedFormulaω Empty n) (τ : Fin n → ℕ) : closeBy (φ.imp ψ) τ = BoundedFormulaω.imp (closeBy φ τ) (closeBy ψ τ)

@[simp]

theorem FirstOrder.Language.closeBy_not {L : Language} {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω Empty n) (τ : Fin n → ℕ) : closeBy φ.not τ = BoundedFormulaω.not (closeBy φ τ)

@[simp]

theorem FirstOrder.Language.closeBy_iInf {L : Language} {n : ℕ} (φs : ℕ → (L.withConstants ℕ).BoundedFormulaω Empty n) (τ : Fin n → ℕ) : closeBy (BoundedFormulaω.iInf φs) τ = BoundedFormulaω.iInf fun (k : ℕ) => closeBy (φs k) τ

@[simp]

theorem FirstOrder.Language.closeBy_iSup {L : Language} {n : ℕ} (φs : ℕ → (L.withConstants ℕ).BoundedFormulaω Empty n) (τ : Fin n → ℕ) : closeBy (BoundedFormulaω.iSup φs) τ = BoundedFormulaω.iSup fun (k : ℕ) => closeBy (φs k) τ

theorem FirstOrder.Language.closeBy_all {L : Language} {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω Empty (n + 1)) (τ : Fin n → ℕ) : closeBy φ.all τ = ((BoundedFormulaω.relabel insertLastBound φ.openBounds).subst fun (i : Fin n) => constTerm (τ i)).all

The arity-one remainder of closing a universal: closeBy φ.all τ is the universal closure of φ opened, relabeled so that the last bound variable stays bound, and closed by τ.

theorem FirstOrder.Language.instConst_eq_closeBy {L : Language} (c : ℕ) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : instConst c ψ = closeBy ψ fun (x : Fin 1) => c

instConst is closeBy at arity one.

closeWith: closing bound variables by a term assignment, without relabeling formulas

Composition

The bridge to openBounds

closeBy, instConst, and the arity-one remainder of closeBy_all are all ((openBounds φ).relabel g).subst τ' for a splitting g. This is the one place where relabel of a formula — and hence castLE — is met; it is discharged by the two composition lemmas of Operations.lean, exactly as in openBounds_relabel_sumInr.

closeBy, its arity-one remainder, and instConst, as closeWith

theorem FirstOrder.Language.openBounds_subst_elim0 {L : Language} (φ : L.Sentenceω) (τ : Fin 0 → L.Term Empty) : BoundedFormulaω.subst (BoundedFormulaω.openBounds φ) τ = φ

Opening a sentence and substituting the empty tuple of closed terms does nothing.

theorem FirstOrder.Language.closeBy_zero {L : Language} (φ : (L.withConstants ℕ).Sentenceω) (τ : Fin 0 → ℕ) : closeBy φ τ = φ

Closing a sentence by the empty tuple does nothing.

theorem FirstOrder.Language.instConst_closeBy_all_remainder {L : Language} {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω Empty (n + 1)) (τ : Fin n → ℕ) (c : ℕ) : instConst c ((BoundedFormulaω.relabel insertLastBound φ.openBounds).subst fun (i : Fin n) => constTerm (τ i)) = closeBy φ (Fin.snoc τ c)

The instance of the remainder is the closure at the extended tuple.