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.

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

The family closure lemmas (one per ConsistencyPropertyEqOn field)