Documentation

InfinitaryLogic.Methods.Interpolation.ConstantElimination

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:

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).

source
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
Instances For
    source
    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.

    source
    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 #

    source
    theorem FirstOrder.Language.relationsIn_genEx {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) :
    BoundedFormulaω.relationsIn (genEx j ρ) = BoundedFormulaω.relationsIn ρ

    genEx preserves the relation symbols.

    source
    theorem FirstOrder.Language.functionsIn_genEx_subset {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) :
    BoundedFormulaω.functionsIn (genEx j ρ) ⊆ BoundedFormulaω.functionsIn ρ

    genEx adds no function symbols.

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

    genEx adds no base function symbols.

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

    genEx preserves the base relation symbols.

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

    genEx adds no constants.

    The acceptance lemmas #

    source
    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.

    source
    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 Γ.

    source
    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 Δ.