Constant elimination: the C7 acceptance lemmas (issue #8 kernel step 5)

The fresh-constant elimination sequents of the Craig arc (docs/craig-audit.md §6a, correction 3). genEx j ρ existentially generalizes the constant c_j out of a sentence ρ; the two acceptance lemmas transport an entailment from a c_j-mentioning form to its generalization, under freshness of c_j for the fixed side:

• entails_genEx_of_entails (side 1): Γ, φ(c) ⊨ σ(c) ⟹ Γ, ∃x φ(x) ⊨ ∃x σ(x), c fresh for Γ;
• entails_not_genEx_of_entails_not (side 2): Δ ⊨ ¬σ(c) ⟹ Δ ⊨ ¬∃x σ(x), c fresh for Δ.

Both are proved by the reinterpretation engine (realize_abstractConst) plus the invariance-outside-support congruence (realize_congr_const), bridged to arbitrary ambient L[[ℕ]]-structures by ambient_realize_iff_wc. Together they show that abstraction transports a separator from constant support insert c A back to A (the InsepAt C7 step).

noncomputable def FirstOrder.Language.genEx {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : (L.withConstants ℕ).Sentenceω

Existentially generalize the constant c_j out of a sentence: abstract c_j into the free variable 0, then existentially quantify it.

Equations

• FirstOrder.Language.genEx j ρ = (FirstOrder.Language.BoundedFormulaω.relabel Sum.inr (FirstOrder.Language.BoundedFormulaω.abstractConst j ρ)).ex

theorem FirstOrder.Language.realize_genEx {L : Language} {M : Type} (base : L.Structure M) (h : ℕ → M) (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.Realize (genEx j ρ) Empty.elim Fin.elim0 ↔ ∃ (x : M), BoundedFormulaω.Realize ρ Empty.elim Fin.elim0

Realizing the generalization is existentially witnessing the original with c_j reinterpreted to the witness.

theorem FirstOrder.Language.notMem_sentenceJConsts_genEx {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : j ∉ sentenceJConsts (genEx j ρ)

c_j is not in the constant support of its own generalization.

Occurrence facts for genEx

theorem FirstOrder.Language.baseFunctionsIn_genEx_subset {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.baseFunctionsIn (genEx j ρ) ⊆ BoundedFormulaω.baseFunctionsIn ρ

genEx adds no base function symbols.

theorem FirstOrder.Language.baseRelationsIn_genEx {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.baseRelationsIn (genEx j ρ) = BoundedFormulaω.baseRelationsIn ρ

genEx preserves the base relation symbols.

theorem FirstOrder.Language.sentenceJConsts_genEx_subset {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : sentenceJConsts (genEx j ρ) ⊆ sentenceJConsts ρ

genEx adds no constants.

The acceptance lemmas

theorem FirstOrder.Language.entails_genEx_of_entails_plain {L : Language} {Γ : Set (L.withConstants ℕ).Sentenceω} (j : ℕ) (σc : (L.withConstants ℕ).Sentenceω) (hyp : Theoryω.Entails Γ σc) : Theoryω.Entails Γ (genEx j σc)

Plain Γ-side abstraction (freshness-free: ∃-introduction is weakening). Γ ⊨ σ upgrades to Γ ⊨ ∃x σ(x); the witness is the constant's own interpretation.

theorem FirstOrder.Language.entails_genEx_of_entails {L : Language} {j : ℕ} {φc σc : (L.withConstants ℕ).Sentenceω} {Γ : Set (L.withConstants ℕ).Sentenceω} (hfresh : ∀ γ ∈ Γ, j ∉ sentenceJConsts γ) (hyp : (insert φc Γ).Entails σc) : (insert (genEx j φc) Γ).Entails (genEx j σc)

Acceptance, side 1: Γ, φ(c) ⊨ σ(c) upgrades to Γ, ∃x φ(x) ⊨ ∃x σ(x) when c_j is fresh for Γ.

theorem FirstOrder.Language.entails_not_genEx_of_entails_not {L : Language} {j : ℕ} {σc : (L.withConstants ℕ).Sentenceω} {Δ : Set (L.withConstants ℕ).Sentenceω} (hfresh : ∀ δ ∈ Δ, j ∉ sentenceJConsts δ) (hyp : Theoryω.Entails Δ (BoundedFormulaω.not σc)) : Theoryω.Entails Δ (BoundedFormulaω.not (genEx j σc))

Acceptance, side 2: Δ ⊨ ¬σ(c) upgrades to Δ ⊨ ¬∃x σ(x) when c_j is fresh for Δ.