The quantifier round-trip and the arbitrary-syntax C7 consumers (issue #8 tranche 1.5)

The Henkin truth lemma will meet an arbitrary existential ψ.ex (or negated universal (ψ.all).not) and construct its constant instance, not a sentence literally of the form genEx c φ. This file bridges the gap:

• instConst c ψ := (ψ.openBounds).subst (fun _ => constTerm c) — the constant instance ψ(c);
• realize_genEx_instConst — the substitution round-trip: genEx c (instConst c ψ) is realization-equivalent to ψ.ex under freshness of c for ψ;
• insepAt_instConst_of_insepAt_ex / insepAt_not_instConst_of_insepAt_not_all — the actual C7 consumers for arbitrary existential / negated-universal parents.

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

theorem FirstOrder.Language.realize_constTerm {L : Language} {M : Type} (base : L.Structure M) (h : ℕ → M) (c : ℕ) (v : Empty → M) : Term.realize v (constTerm c) = h c

The constant c_c realizes to its interpretation h c.

theorem FirstOrder.Language.realize_instConst {L : Language} {M : Type} (base : L.Structure M) (h : ℕ → M) (c : ℕ) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : BoundedFormulaω.Realize (instConst c ψ) Empty.elim Fin.elim0 ↔ ψ.Realize Empty.elim fun (x : Fin 1) => h c

Realizing the constant instance ψ(c) is realizing ψ at the constant's interpretation.

theorem FirstOrder.Language.realize_genEx_instConst {L : Language} {M : Type} (base : L.Structure M) (h : ℕ → M) (c : ℕ) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hfresh : c ∉ sentenceJConsts ψ) : BoundedFormulaω.Realize (genEx c (instConst c ψ)) Empty.elim Fin.elim0 ↔ ψ.ex.Realize Empty.elim Fin.elim0

The substitution round-trip: for c fresh for ψ, genEx c (instConst c ψ) realizes exactly as ψ.ex.

Ambient semantic equivalence and premise congruence

theorem FirstOrder.Language.realize_genEx_instConst_iff_ex {L : Language} (c : ℕ) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hfresh : c ∉ sentenceJConsts ψ) (M : Type) [S : (L.withConstants ℕ).Structure M] : (genEx c (instConst c ψ)).Realize M ↔ Sentenceω.Realize ψ.ex M

The round-trip as a semantic equivalence over arbitrary ambient structures.

theorem FirstOrder.Language.entails_insert_congr {L : Language} {Γ : Set (L.withConstants ℕ).Sentenceω} {σ₁ σ₂ τ : (L.withConstants ℕ).Sentenceω} (hequiv : ∀ (M : Type) [inst : (L.withConstants ℕ).Structure M] [Nonempty M], σ₁.Realize M ↔ σ₂.Realize M) : (insert σ₁ Γ).Entails τ ↔ (insert σ₂ Γ).Entails τ

Entailment is invariant under replacing an inserted premise by a semantically equivalent sentence.

theorem FirstOrder.Language.insepAt_insert_congr {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {σ₁ σ₂ : (L.withConstants ℕ).Sentenceω} (hequiv : ∀ (M : Type) [inst : (L.withConstants ℕ).Structure M] [Nonempty M], σ₁.Realize M ↔ σ₂.Realize M) : InsepAt F R A (insert σ₁ Γ) Δ ↔ InsepAt F R A (insert σ₂ Γ) Δ

InsepAt is invariant under replacing an inserted premise by a semantically equivalent sentence.

The arbitrary-syntax C7 consumers

theorem FirstOrder.Language.insepAt_instConst_of_insepAt_ex {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hcψ : c ∉ sentenceJConsts ψ) (hcΓ : ∀ γ ∈ Γ, c ∉ sentenceJConsts γ) (hcΔ : ∀ δ ∈ Δ, c ∉ sentenceJConsts δ) (h : InsepAt F R A (insert ψ.ex Γ) Δ) : InsepAt F R (insert c A) (insert (instConst c ψ) Γ) Δ

C7 consumer (existential): if the existential pair is inseparable at support A, then the constant-instance pair is inseparable at support insert c A, for c fresh for ψ, Γ, Δ.

theorem FirstOrder.Language.insepAt_not_instConst_of_insepAt_not_all {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hcψ : c ∉ sentenceJConsts ψ.not) (hcΓ : ∀ γ ∈ Γ, c ∉ sentenceJConsts γ) (hcΔ : ∀ δ ∈ Δ, c ∉ sentenceJConsts δ) (h : InsepAt F R A (insert ψ.all.not Γ) Δ) : InsepAt F R (insert c A) (insert (instConst c ψ.not) Γ) Δ

C7 consumer (negated universal): ¬∀x ψ is ∃x ¬ψ; the witness is ¬ψ(c).