Constant surgery: substituting one constant for another

The neutral constant-surgery layer. substConst b a ρ replaces the constant c_b by c_a throughout ρ, built from the existing abstraction/instantiation pair, together with its realization, symbol, constant-support and quantifier-occurrence laws.

Nothing here is specific to interpolation: this is the reusable operation tracked by issue #39 (neutral L_ω₁ω syntax-analysis and constant-surgery API), extracted early because the cross-label equality/relation transfer of the Malitz arc is its first consumer. The decisive law is hasQuantSigned_substConst: substitution moves no quantifier occurrence, which is what lets a consumer replace a constant in a separator without spending a quantifier permission.

The instConst dependency is why this file currently sits under Methods beside the interpolation machinery rather than in the syntax layer; #39's consolidation is where that is resolved.

Constant-for-constant substitution

The machinery the cross-label equality/relation transfers need, and the reason they are the riskiest gate: when the relation atom and the equality atom sit on different labels, the derived atom is entailed by neither side alone, and the separator of the extended pair may legitimately mention a constant that only the other side carries. Feferman's condition (iii) then forces that constant out of the separator — and the operation that does it is substitution of the shared partner, not quantification.

substConst b a ρ replaces the constant c_b by c_a throughout ρ, built from the existing abstraction/instantiation pair.

noncomputable def FirstOrder.Language.substConst {L : Language} (b a : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : (L.withConstants ℕ).Sentenceω

Replace the constant c_b by c_a: abstract b into the free variable, then instantiate at a.

Equations

• FirstOrder.Language.substConst b a ρ = FirstOrder.Language.instConst a (FirstOrder.Language.BoundedFormulaω.relabel Sum.inr (FirstOrder.Language.BoundedFormulaω.abstractConst b ρ))

theorem FirstOrder.Language.realize_substConst {L : Language} {M : Type} (base : L.Structure M) (h : ℕ → M) (b a : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.Realize (substConst b a ρ) Empty.elim Fin.elim0 ↔ BoundedFormulaω.Realize ρ Empty.elim Fin.elim0

Realizing the substitution is realizing the original with b reinterpreted at a's value.

theorem FirstOrder.Language.baseFunctionsIn_substConst_subset {L : Language} (b a : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.baseFunctionsIn (substConst b a ρ) ⊆ BoundedFormulaω.baseFunctionsIn ρ

theorem FirstOrder.Language.baseRelationsIn_substConst {L : Language} (b a : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.baseRelationsIn (substConst b a ρ) ⊆ BoundedFormulaω.baseRelationsIn ρ

theorem FirstOrder.Language.sentenceJConsts_substConst_subset {L : Language} (b a : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : sentenceJConsts (substConst b a ρ) ⊆ sentenceJConsts ρ ∪ {a}

theorem FirstOrder.Language.notMem_sentenceJConsts_substConst {L : Language} (b a : ℕ) (hne : b ≠ a) (ρ : (L.withConstants ℕ).Sentenceω) : b ∉ sentenceJConsts (substConst b a ρ)

The substituted constant is gone, provided it was not the substitute.

theorem FirstOrder.Language.hasQuantSigned_abstractConst {L : Language} (j : ℕ) (s : Bool) {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω Empty n) : BoundedFormulaω.hasQuantSigned s (BoundedFormulaω.abstractConst j φ) ↔ BoundedFormulaω.hasQuantSigned s φ

Constant abstraction does not move the signed quantifier occurrences.

theorem FirstOrder.Language.hasQuantSigned_substConst {L : Language} (b a : ℕ) (s : Bool) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.hasQuantSigned s (substConst b a ρ) ↔ BoundedFormulaω.hasQuantSigned s ρ

Substitution does not move the signed quantifier occurrences: the budgets are untouched.