The finite inseparable-pair consistency family and its structural lemmas (issue #8, commit 4a)

This file assembles the consistency family whose members will be packaged, in commit 4b, into a ConsistencyPropertyEqOn instance driving the fair Henkin enumeration of the Craig interpolation argument (docs/craig-audit.md §7–§8).

A family member over a fixed shared vocabulary (F, R), right-hand side Δ, and enumeration roots r₁, r₂ is a finite set Γ of L[[ℕ]]-sentences drawn from the generated universe GenU r₁ r₂ that is inseparable from Δ at some finite allowed support A (InsepAt F R A Γ Δ).

The bulk of the file proves the structural closure lemmas — one per ConsistencyPropertyEqOn field — showing that each syntactic decomposition step (the propositional C0–C4 rules, the L_{ω₁ω} conjunction/disjunction component rules, the atomic equality/congruence rules, universal instantiation, and the fresh-witness rule for negated universals) preserves family membership. These are the exact obligations the consistency-property packaging will discharge.

The two moving parts are:

• the underlying InsepAt-level closures (insepAt_*), which certify that inseparability survives each decomposition — built on the consequence-preservation workhorse insepAt_insert_of_entails and a handful of propositional/atomic validities; and
• the family-level closures (insepFamily_*), which additionally track GenU-membership (via the GeneratedUniverse reachability lemmas) and finiteness (via Set.Finite.insert).

Base-symbol / constant-support union bounds

The separators built in the InsepAt closures are combinations (iSup, imp, falsum) of the component separators; these lemmas bound their base symbols and constant support by the components'.

theorem FirstOrder.Language.baseFunctionsIn_iSup_subset {L : Language} {A : Set ((n : ℕ) × L.Functions n)} (σ : ℕ → (L.withConstants ℕ).Sentenceω) (h : ∀ (k : ℕ), BoundedFormulaω.baseFunctionsIn (σ k) ⊆ A) : (BoundedFormulaω.iSup σ).baseFunctionsIn ⊆ A

theorem FirstOrder.Language.baseRelationsIn_iSup_subset {L : Language} {A : Set ((n : ℕ) × L.Relations n)} (σ : ℕ → (L.withConstants ℕ).Sentenceω) (h : ∀ (k : ℕ), BoundedFormulaω.baseRelationsIn (σ k) ⊆ A) : (BoundedFormulaω.iSup σ).baseRelationsIn ⊆ A

theorem FirstOrder.Language.sentenceJConsts_iSup_subset {L : Language} {A : Set ℕ} (σ : ℕ → (L.withConstants ℕ).Sentenceω) (h : ∀ (k : ℕ), sentenceJConsts (σ k) ⊆ A) : sentenceJConsts (BoundedFormulaω.iSup σ) ⊆ A

theorem FirstOrder.Language.baseFunctionsIn_imp_subset {L : Language} {A : Set ((n : ℕ) × L.Functions n)} {σ₁ σ₂ : (L.withConstants ℕ).Sentenceω} (h₁ : BoundedFormulaω.baseFunctionsIn σ₁ ⊆ A) (h₂ : BoundedFormulaω.baseFunctionsIn σ₂ ⊆ A) : (BoundedFormulaω.imp σ₁ σ₂).baseFunctionsIn ⊆ A

theorem FirstOrder.Language.baseRelationsIn_imp_subset {L : Language} {A : Set ((n : ℕ) × L.Relations n)} {σ₁ σ₂ : (L.withConstants ℕ).Sentenceω} (h₁ : BoundedFormulaω.baseRelationsIn σ₁ ⊆ A) (h₂ : BoundedFormulaω.baseRelationsIn σ₂ ⊆ A) : (BoundedFormulaω.imp σ₁ σ₂).baseRelationsIn ⊆ A

theorem FirstOrder.Language.sentenceJConsts_imp_subset {L : Language} {A : Set ℕ} {σ₁ σ₂ : (L.withConstants ℕ).Sentenceω} (h₁ : sentenceJConsts σ₁ ⊆ A) (h₂ : sentenceJConsts σ₂ ⊆ A) : sentenceJConsts (BoundedFormulaω.imp σ₁ σ₂) ⊆ A

theorem FirstOrder.Language.baseFunctionsIn_not {L : Language} (φ : (L.withConstants ℕ).Sentenceω) : (BoundedFormulaω.not φ).baseFunctionsIn = BoundedFormulaω.baseFunctionsIn φ

theorem FirstOrder.Language.baseRelationsIn_not {L : Language} (φ : (L.withConstants ℕ).Sentenceω) : (BoundedFormulaω.not φ).baseRelationsIn = BoundedFormulaω.baseRelationsIn φ

theorem FirstOrder.Language.baseFunctionsIn_falsum {L : Language} : BoundedFormulaω.falsum.baseFunctionsIn = ∅

theorem FirstOrder.Language.baseRelationsIn_falsum {L : Language} : BoundedFormulaω.falsum.baseRelationsIn = ∅

theorem FirstOrder.Language.sentenceJConsts_falsum {L : Language} : sentenceJConsts BoundedFormulaω.falsum = ∅

The consequence-preservation workhorse and semantic validities

theorem FirstOrder.Language.insepAt_insert_of_entails {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).Sentenceω} (hcons : Theoryω.Entails Γ φ) (h : InsepAt F R A Γ Δ) : InsepAt F R A (insert φ Γ) Δ

Consequence preservation: adding an entailed sentence to Γ cannot break inseparability, because the separator's Γ-entailment survives a cut.

theorem FirstOrder.Language.entails_of_mem_of_entails {L : Language} {Γ : Set (L.withConstants ℕ).Sentenceω} {σ τ : (L.withConstants ℕ).Sentenceω} (hmem : σ ∈ Γ) (hval : σ.Entails τ) : Theoryω.Entails Γ τ

A membership fact plus a pointwise validity yields a Γ-entailment.

theorem FirstOrder.Language.negimp_entails_left {L : Language} (φ ψ : (L.withConstants ℕ).Sentenceω) : Sentenceω.Entails (BoundedFormulaω.imp φ ψ).not φ

theorem FirstOrder.Language.negimp_entails_right {L : Language} (φ ψ : (L.withConstants ℕ).Sentenceω) : Sentenceω.Entails (BoundedFormulaω.imp φ ψ).not (BoundedFormulaω.not ψ)

theorem FirstOrder.Language.not_not_entails {L : Language} (φ : (L.withConstants ℕ).Sentenceω) : Sentenceω.Entails (BoundedFormulaω.not φ).not φ

theorem FirstOrder.Language.iInf_entails_component {L : Language} (φs : ℕ → (L.withConstants ℕ).Sentenceω) (k : ℕ) : Sentenceω.Entails (BoundedFormulaω.iInf φs) (φs k)

theorem FirstOrder.Language.neg_iSup_entails_neg_component {L : Language} (φs : ℕ → (L.withConstants ℕ).Sentenceω) (k : ℕ) : Sentenceω.Entails (BoundedFormulaω.iSup φs).not (BoundedFormulaω.not (φs k))

Atomic equality and relation-congruence validities

cval M c is the ambient interpretation of the constant c_c; a constant equality realizes iff the interpretations coincide.

noncomputable def FirstOrder.Language.cval {L : Language} (M : Type) [S : (L.withConstants ℕ).Structure M] (c : ℕ) : M

The ambient interpretation of the constant c_c (as the realization of constTermS c).

Equations

• FirstOrder.Language.cval M c = FirstOrder.Language.Term.realize (Sum.elim Empty.elim Fin.elim0) (FirstOrder.Language.constTermS c)

theorem FirstOrder.Language.realize_constEq {L : Language} (M : Type) [S : (L.withConstants ℕ).Structure M] (a b : ℕ) : (constEq a b).Realize M ↔ cval M a = cval M b

theorem FirstOrder.Language.entails_constEq_refl {L : Language} {Γ : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) : Theoryω.Entails Γ (constEq c c)

theorem FirstOrder.Language.entails_constEq_symm {L : Language} {Γ : Set (L.withConstants ℕ).Sentenceω} {a b : ℕ} (hmem : constEq a b ∈ Γ) : Theoryω.Entails Γ (constEq b a)

theorem FirstOrder.Language.entails_constEq_trans {L : Language} {Γ : Set (L.withConstants ℕ).Sentenceω} {a b d : ℕ} (h1 : constEq a b ∈ Γ) (h2 : constEq b d ∈ Γ) : Theoryω.Entails Γ (constEq a d)

theorem FirstOrder.Language.entails_rel_congr {L : Language} {Γ : Set (L.withConstants ℕ).Sentenceω} {l : ℕ} (Rr : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ) (h1 : relInst Rr g ∈ Γ) (h2 : constEq (g i) b ∈ Γ) : Theoryω.Entails Γ (relInst Rr (Function.update g i b))

Ambient universal instantiation

theorem FirstOrder.Language.realize_instConst_ambient_iff {L : Language} (c : ℕ) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (M : Type) [S : (L.withConstants ℕ).Structure M] : (instConst c φ).Realize M ↔ φ.Realize Empty.elim fun (x : Fin 1) => ambientConstMap M c

Realizing the constant instance φ(c) in an ambient structure is realizing φ at the constant's ambient interpretation.

theorem FirstOrder.Language.all_entails_instConst {L : Language} (c : ℕ) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : Sentenceω.Entails φ.all (instConst c φ)

InsepAt-level closures under the decomposition rules

theorem FirstOrder.Language.insepAt_iSup_component {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hmem : BoundedFormulaω.iSup φs ∈ Γ) (h : InsepAt F R A Γ Δ) : ∃ (k : ℕ), InsepAt F R A (insert (φs k) Γ) Δ

C4 (disjunction): a disjunction in Γ splits off a component preserving inseparability.

theorem FirstOrder.Language.insepAt_neg_iInf_component {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hmem : (BoundedFormulaω.iInf φs).not ∈ Γ) (h : InsepAt F R A Γ Δ) : ∃ (k : ℕ), InsepAt F R A (insert (BoundedFormulaω.not (φs k)) Γ) Δ

C3' (negated conjunction): a negated conjunction in Γ splits off a negated component.

theorem FirstOrder.Language.insepAt_imp_dichotomy {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ ψ : (L.withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.imp φ ψ ∈ Γ) (h : InsepAt F R A Γ Δ) : InsepAt F R A (insert (BoundedFormulaω.not φ) Γ) Δ ∨ InsepAt F R A (insert ψ Γ) Δ

C1 (implication): an implication in Γ yields one of the two possible refinements.

theorem FirstOrder.Language.insepAt_falsum_absurd {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.falsum ∈ Γ) (h : InsepAt F R A Γ Δ) : False

C0 (falsum): ⊥ ∈ Γ is incompatible with inseparability (⊥ separates from anything).

theorem FirstOrder.Language.insepAt_contradiction_absurd {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).Sentenceω} (h1 : φ ∈ Γ) (h2 : BoundedFormulaω.not φ ∈ Γ) (h : InsepAt F R A Γ Δ) : False

A sentence and its negation both in Γ is incompatible with inseparability.

The constant-instance negation identity

The fresh-witness rule produces instConst c φ.not; the family field wants (instConst c φ).not. These are literally the same formula (openBounds and subst distribute over · .imp ⊥).

theorem FirstOrder.Language.instConst_not {L : Language} (c : ℕ) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : instConst c φ.not = BoundedFormulaω.not (instConst c φ)

The finite inseparable-pair consistency family

def FirstOrder.Language.InsepFamilyMem {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) (Δ : Set (L.withConstants ℕ).Sentenceω) (r₁ r₂ : (L.withConstants ℕ).Sentenceω) (Γ : Set (L.withConstants ℕ).Sentenceω) : Prop

A family member: a finite subset of the generated universe GenU r₁ r₂ inseparable from Δ at some finite allowed support. This is the underlying condition set of the interpolation consistency property.

Equations

• FirstOrder.Language.InsepFamilyMem F R Δ r₁ r₂ Γ = (Γ.Finite ∧ Γ ⊆ FirstOrder.Language.GenU r₁ r₂ ∧ ∃ (A : Finset ℕ), FirstOrder.Language.InsepAt F R A Γ Δ)

theorem FirstOrder.Language.InsepFamilyMem.finite {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (h : InsepFamilyMem F R Δ r₁ r₂ Γ) : Γ.Finite

theorem FirstOrder.Language.InsepFamilyMem.subset_genU {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (h : InsepFamilyMem F R Δ r₁ r₂ Γ) : Γ ⊆ GenU r₁ r₂

theorem FirstOrder.Language.InsepFamilyMem.support_finite {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (hr₁ : (sentenceJConsts r₁).Finite) (hr₂ : (sentenceJConsts r₂).Finite) (h : InsepFamilyMem F R Δ r₁ r₂ Γ) : (⋃ γ ∈ Γ, sentenceJConsts γ).Finite

The total constant support of a family member is finite (each member has finite support by genU_finite_support, and a family member is a finite union of members).

The family closure lemmas (one per ConsistencyPropertyEqOn field)

theorem FirstOrder.Language.insepFamily_no_falsum {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) : BoundedFormulaω.falsum ∉ Γ

C0 field: ⊥ ∉ Γ for a family member.

theorem FirstOrder.Language.insepFamily_no_contradiction {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) (φ : (L.withConstants ℕ).Sentenceω) : ¬(φ ∈ Γ ∧ BoundedFormulaω.not φ ∈ Γ)

Contradiction field: no sentence and its negation both lie in a family member.

theorem FirstOrder.Language.insepFamily_imp {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ φ ψ : (L.withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.imp φ ψ ∈ Γ) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) : InsepFamilyMem F R Δ r₁ r₂ (insert (BoundedFormulaω.not φ) Γ) ∨ InsepFamilyMem F R Δ r₁ r₂ (insert ψ Γ)

C1 field: an implication yields one of the two refined family members.

theorem FirstOrder.Language.insepFamily_neg_imp {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ φ ψ : (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.imp φ ψ).not ∈ Γ) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) : InsepFamilyMem F R Δ r₁ r₂ (insert φ Γ) ∧ InsepFamilyMem F R Δ r₁ r₂ (insert (BoundedFormulaω.not ψ) Γ)

C2 field (negated implication): ¬(φ → ψ) yields both refined family members.

theorem FirstOrder.Language.insepFamily_not_not {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ φ : (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.not φ).not ∈ Γ) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) : InsepFamilyMem F R Δ r₁ r₂ (insert φ Γ)

Double-negation field: ¬¬φ refines to φ.

theorem FirstOrder.Language.insepFamily_iInf {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.iInf φs ∈ Γ) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) (k : ℕ) : InsepFamilyMem F R Δ r₁ r₂ (insert (φs k) Γ)

C3 field (conjunction): each component of a conjunction refines the member.

theorem FirstOrder.Language.insepFamily_neg_iInf {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.iInf φs).not ∈ Γ) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) : ∃ (k : ℕ), InsepFamilyMem F R Δ r₁ r₂ (insert (BoundedFormulaω.not (φs k)) Γ)

C3' field (negated conjunction): some negated component refines the member.

theorem FirstOrder.Language.insepFamily_iSup {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.iSup φs ∈ Γ) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) : ∃ (k : ℕ), InsepFamilyMem F R Δ r₁ r₂ (insert (φs k) Γ)

C4 field (disjunction): some component refines the member.

theorem FirstOrder.Language.insepFamily_neg_iSup {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.iSup φs).not ∈ Γ) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) (k : ℕ) : InsepFamilyMem F R Δ r₁ r₂ (insert (BoundedFormulaω.not (φs k)) Γ)

C4' field (negated disjunction): each negated component refines the member.

theorem FirstOrder.Language.insepFamily_eq_refl {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) (c : ℕ) : InsepFamilyMem F R Δ r₁ r₂ (insert (constEq c c) Γ)

Equality reflexivity field: c = c can always be added.

theorem FirstOrder.Language.insepFamily_eq_symm {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {a b : ℕ} (hmem : constEq a b ∈ Γ) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) : InsepFamilyMem F R Δ r₁ r₂ (insert (constEq b a) Γ)

Equality symmetry field: a = b ∈ Γ lets b = a be added.

theorem FirstOrder.Language.insepFamily_eq_trans {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {a b d : ℕ} (h1 : constEq a b ∈ Γ) (h2 : constEq b d ∈ Γ) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) : InsepFamilyMem F R Δ r₁ r₂ (insert (constEq a d) Γ)

Equality transitivity field: a = b, b = d ∈ Γ let a = d be added.

theorem FirstOrder.Language.insepFamily_rel_congr {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {l : ℕ} (Rr : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ) (h1 : relInst Rr g ∈ Γ) (h2 : constEq (g i) b ∈ Γ) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) : InsepFamilyMem F R Δ r₁ r₂ (insert (relInst Rr (Function.update g i b)) Γ)

Relation-congruence field: replacing one argument of an atomic relation instance by an equal constant can be added.

theorem FirstOrder.Language.insepFamily_all_inst {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (hmem : φ.all ∈ Γ) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) (c : ℕ) : InsepFamilyMem F R Δ r₁ r₂ (insert (instConst c φ) Γ)

Universal instantiation field: ∀x φ ∈ Γ lets every constant instance φ(c) be added.

theorem FirstOrder.Language.insepFamily_neg_all_witness {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {Δ Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (hr₁ : (sentenceJConsts r₁).Finite) (hr₂ : (sentenceJConsts r₂).Finite) (hΔfin : (⋃ δ ∈ Δ, sentenceJConsts δ).Finite) (hfam : InsepFamilyMem F R Δ r₁ r₂ Γ) (hmem : φ.all.not ∈ Γ) : ∃ (c : ℕ), InsepFamilyMem F R Δ r₁ r₂ (insert (BoundedFormulaω.not (instConst c φ)) Γ)

The fresh-witness field (negated universal): ¬∀x φ ∈ Γ produces a fresh constant c and the refined family member insert ¬φ(c) Γ. Freshness of c (for Γ, Δ, and φ) is what makes the abstracted separator strip cleanly; it exists because the total constant support in play is finite.