The paired inseparable-pair consistency family and its model (issue #8, commit 4c part 2)

This file assembles the paired finite inseparable-pair family on top of the validated cross-coordinate gates (PairedInseparability.lean) and the one-sided left closures (InseparablePairFamily.lean). A family member is a U-bounded, symmetrically support-budgeted pair (Γ, Δ) with Γ ⊆ SentBnd F₁ R₁, Δ ⊆ SentBnd F₂ R₂, inseparable at the shared vocabulary (F₁ ∩ F₂, R₁ ∩ R₂).

• SentBnd F R — the side vocabulary predicate (base symbols in (F, R)).
• PairedInsepFamilyMem — the family membership predicate (the ∃ Γ Δ A decomposition).
• pairedInsepConsistencyProperty — the ConsistencyPropertyEqOn (GenU rL rR) bundle. Each field case-splits the trigger between Γ and Δ: the Γ case reuses the one-sided left closure; the Δ case dualizes it through insepAt_swap; the cross cases (C0, shared-equality/relation transfer) use the PairedInseparability gates.
• exists_paired_model — from a root inseparable pair {rL} / {rR}, a single model realizing both roots (over a countable relational vocabulary).
• exists_paired_model_neg — the public wrapper: instantiating rR := r₂.not yields a model with M ⊨ r₁ ∧ ¬ M ⊨ r₂.

The side vocabulary predicate SentBnd

def FirstOrder.Language.SentBnd {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) : Set (L.withConstants ℕ).Sentenceω

Side vocabulary bound. A sentence whose base function/relation symbols lie in (F, R).

Equations

• One or more equations did not get rendered due to their size.

SentBnd closure lemmas

theorem FirstOrder.Language.sentBnd_not_iff {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {σ : (L.withConstants ℕ).Sentenceω} : BoundedFormulaω.not σ ∈ SentBnd F R ↔ σ ∈ SentBnd F R

theorem FirstOrder.Language.sentBnd_imp_left {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {φ ψ : (L.withConstants ℕ).Sentenceω} (h : BoundedFormulaω.imp φ ψ ∈ SentBnd F R) : φ ∈ SentBnd F R

theorem FirstOrder.Language.sentBnd_imp_right {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {φ ψ : (L.withConstants ℕ).Sentenceω} (h : BoundedFormulaω.imp φ ψ ∈ SentBnd F R) : ψ ∈ SentBnd F R

theorem FirstOrder.Language.sentBnd_component_iInf {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) (h : BoundedFormulaω.iInf φs ∈ SentBnd F R) : φs k ∈ SentBnd F R

theorem FirstOrder.Language.sentBnd_component_iSup {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) (h : BoundedFormulaω.iSup φs ∈ SentBnd F R) : φs k ∈ SentBnd F R

theorem FirstOrder.Language.sentBnd_instConst {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (c : ℕ) (h : φ.all ∈ SentBnd F R) : instConst c φ ∈ SentBnd F R

theorem FirstOrder.Language.sentBnd_constEq {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} (a b : ℕ) : constEq a b ∈ SentBnd F R

Constant-expansion roots as side-bounded sentences

The two shapes every countable interpolation core needs of its labelled roots. Each replaces a four-part tuple of base-occurrence and negation rewrites at the call site.

theorem FirstOrder.Language.mapLanguage_withConstants_mem_sentBnd {L : Language} (r : L.Sentenceω) : BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) r ∈ SentBnd (BoundedFormulaω.functionsIn r) (BoundedFormulaω.relationsIn r)

A constant-expansion image is bounded by its own base symbols.

theorem FirstOrder.Language.mapLanguage_withConstants_not_mem_sentBnd {L : Language} (r : L.Sentenceω) : (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) r).not ∈ SentBnd (BoundedFormulaω.functionsIn r) (BoundedFormulaω.relationsIn r)

…and so is its negation, SentBnd being negation-invariant.

theorem FirstOrder.Language.sentBnd_relInst_congr {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {l : ℕ} (Rr : L.Relations l) {g : Fin l → ℕ} (g' : Fin l → ℕ) (h : relInst Rr g ∈ SentBnd F R) : relInst Rr g' ∈ SentBnd F R

Atomic constant-support facts

theorem FirstOrder.Language.mem_constTermS_jConsts {L : Language} (c : ℕ) : c ∈ (constTermS c).jConsts

theorem FirstOrder.Language.mem_sentenceJConsts_constEq_left {L : Language} (a b : ℕ) : a ∈ sentenceJConsts (constEq a b)

theorem FirstOrder.Language.mem_sentenceJConsts_constEq_right {L : Language} (a b : ℕ) : b ∈ sentenceJConsts (constEq a b)

theorem FirstOrder.Language.sentenceJConsts_constEq_subset {L : Language} (a b : ℕ) : sentenceJConsts (constEq a b) ⊆ {a, b}

theorem FirstOrder.Language.sentenceJConsts_constEq_comm {L : Language} (a b : ℕ) : sentenceJConsts (constEq a b) = sentenceJConsts (constEq b a)

theorem FirstOrder.Language.sentenceJConsts_relInst_eq {L : Language} {l : ℕ} (Rr : L.Relations l) (g : Fin l → ℕ) : sentenceJConsts (relInst Rr g) = Set.range g

The paired family

def FirstOrder.Language.PairedInsepFamilyMem {L : Language} (F₁ : Set ((n : ℕ) × L.Functions n)) (R₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (R₂ : Set ((n : ℕ) × L.Relations n)) (rL rR : (L.withConstants ℕ).Sentenceω) (S : Set (L.withConstants ℕ).Sentenceω) : Prop

A paired family member: a symmetrically support-budgeted, U-bounded, side-typed pair (Γ, Δ) inseparable at the shared vocabulary (F₁ ∩ F₂, R₁ ∩ R₂).

Equations

• One or more equations did not get rendered due to their size.

Support and freshness bookkeeping

theorem FirstOrder.Language.support_mem_left {L : Language} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {A : Finset ℕ} {φ : (L.withConstants ℕ).Sentenceω} (hmem : φ ∈ Γ) (hsupp : (⋃ γ ∈ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ Δ, sentenceJConsts δ ⊆ ↑A) : sentenceJConsts φ ⊆ ↑A

theorem FirstOrder.Language.support_mem_right {L : Language} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {A : Finset ℕ} {φ : (L.withConstants ℕ).Sentenceω} (hmem : φ ∈ Δ) (hsupp : (⋃ γ ∈ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ Δ, sentenceJConsts δ ⊆ ↑A) : sentenceJConsts φ ⊆ ↑A

theorem FirstOrder.Language.support_mem {L : Language} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {A : Finset ℕ} {φ : (L.withConstants ℕ).Sentenceω} (hmem : φ ∈ Γ ∪ Δ) (hsupp : (⋃ γ ∈ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ Δ, sentenceJConsts δ ⊆ ↑A) : sentenceJConsts φ ⊆ ↑A

theorem FirstOrder.Language.support_insert_left {L : Language} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).Sentenceω} {A : Finset ℕ} (hφ : sentenceJConsts φ ⊆ ↑A) (h : (⋃ γ ∈ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ Δ, sentenceJConsts δ ⊆ ↑A) : (⋃ γ ∈ insert φ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ Δ, sentenceJConsts δ ⊆ ↑A

theorem FirstOrder.Language.support_insert_right {L : Language} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).Sentenceω} {A : Finset ℕ} (hφ : sentenceJConsts φ ⊆ ↑A) (h : (⋃ γ ∈ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ Δ, sentenceJConsts δ ⊆ ↑A) : (⋃ γ ∈ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ insert φ Δ, sentenceJConsts δ ⊆ ↑A

theorem FirstOrder.Language.fresh_left {L : Language} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {A : Finset ℕ} (c : ℕ) (hc : c ∉ ↑A) (hsupp : (⋃ γ ∈ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ Δ, sentenceJConsts δ ⊆ ↑A) (γ : (L.withConstants ℕ).Sentenceω) : γ ∈ Γ → c ∉ sentenceJConsts γ

theorem FirstOrder.Language.fresh_right {L : Language} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {A : Finset ℕ} (c : ℕ) (hc : c ∉ ↑A) (hsupp : (⋃ γ ∈ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ Δ, sentenceJConsts δ ⊆ ↑A) (δ : (L.withConstants ℕ).Sentenceω) : δ ∈ Δ → c ∉ sentenceJConsts δ

theorem FirstOrder.Language.insepAt_insert_right_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 φ Δ)

Grow the Δ-coordinate by an entailed sentence (the right-coordinate twin of insepAt_insert_of_entails, obtained through insepAt_swap).

The two coordinate-growth constructors

theorem FirstOrder.Language.pairedInsep_insert_left {L : Language} {F₁ : Set ((n : ℕ) × L.Functions n)} {R₁ : Set ((n : ℕ) × L.Relations n)} {F₂ : Set ((n : ℕ) × L.Functions n)} {R₂ : Set ((n : ℕ) × L.Relations n)} {rL rR : (L.withConstants ℕ).Sentenceω} {S Γ Δ : Set (L.withConstants ℕ).Sentenceω} {A : Finset ℕ} {φ : (L.withConstants ℕ).Sentenceω} (hSeq : S = Γ ∪ Δ) (hΓfin : Γ.Finite) (hΔfin : Δ.Finite) (hΓU : Γ ⊆ GenU rL rR) (hΔU : Δ ⊆ GenU rL rR) (hΓS : Γ ⊆ SentBnd F₁ R₁) (hΔS : Δ ⊆ SentBnd F₂ R₂) (hφU : φ ∈ GenU rL rR) (hφS : φ ∈ SentBnd F₁ R₁) (hsupp : (⋃ γ ∈ insert φ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ Δ, sentenceJConsts δ ⊆ ↑A) (hA : InsepAt (F₁ ∩ F₂) (R₁ ∩ R₂) A (insert φ Γ) Δ) : PairedInsepFamilyMem F₁ R₁ F₂ R₂ rL rR (S ∪ {φ})

Add φ to the Γ-coordinate of a paired family member.

theorem FirstOrder.Language.pairedInsep_insert_right {L : Language} {F₁ : Set ((n : ℕ) × L.Functions n)} {R₁ : Set ((n : ℕ) × L.Relations n)} {F₂ : Set ((n : ℕ) × L.Functions n)} {R₂ : Set ((n : ℕ) × L.Relations n)} {rL rR : (L.withConstants ℕ).Sentenceω} {S Γ Δ : Set (L.withConstants ℕ).Sentenceω} {A : Finset ℕ} {φ : (L.withConstants ℕ).Sentenceω} (hSeq : S = Γ ∪ Δ) (hΓfin : Γ.Finite) (hΔfin : Δ.Finite) (hΓU : Γ ⊆ GenU rL rR) (hΔU : Δ ⊆ GenU rL rR) (hΓS : Γ ⊆ SentBnd F₁ R₁) (hΔS : Δ ⊆ SentBnd F₂ R₂) (hφU : φ ∈ GenU rL rR) (hφS : φ ∈ SentBnd F₂ R₂) (hsupp : (⋃ γ ∈ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ insert φ Δ, sentenceJConsts δ ⊆ ↑A) (hA : InsepAt (F₁ ∩ F₂) (R₁ ∩ R₂) A Γ (insert φ Δ)) : PairedInsepFamilyMem F₁ R₁ F₂ R₂ rL rR (S ∪ {φ})

Add φ to the Δ-coordinate of a paired family member.

The paired inseparable-pair consistency property

def FirstOrder.Language.pairedInsepConsistencyProperty {L : Language} (F₁ : Set ((n : ℕ) × L.Functions n)) (R₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (R₂ : Set ((n : ℕ) × L.Relations n)) (rL rR : (L.withConstants ℕ).Sentenceω) (hrL : (sentenceJConsts rL).Finite) (hrR : (sentenceJConsts rR).Finite) : ConsistencyPropertyEqOn (GenU rL rR)

The paired inseparable-pair consistency property. The finite paired family over the generated universe GenU rL rR, with each ConsistencyPropertyEqOn closure field discharged by a Γ/Δ case split: the Γ case reuses the one-sided left closure, the Δ case dualizes it through insepAt_swap, and the cross cases use the PairedInseparability gates. The root finiteness hypotheses enter only in neg_all_witness (to choose a fresh witness).

Equations

• One or more equations did not get rendered due to their size.

The paired model endpoint

theorem FirstOrder.Language.exists_paired_model {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (F₁ : Set ((n : ℕ) × L.Functions n)) (R₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (R₂ : Set ((n : ℕ) × L.Relations n)) (rL rR : (L.withConstants ℕ).Sentenceω) (hrL : (sentenceJConsts rL).Finite) (hrR : (sentenceJConsts rR).Finite) (hrLsent : rL ∈ SentBnd F₁ R₁) (hrRsent : rR ∈ SentBnd F₂ R₂) (A₀ : Finset ℕ) (hsupp : sentenceJConsts rL ∪ sentenceJConsts rR ⊆ ↑A₀) (hroot : InsepAt (F₁ ∩ F₂) (R₁ ∩ R₂) A₀ {rL} {rR}) : ∃ (M : Type) (x : (L.withConstants ℕ).Structure M) (_ : Nonempty M), rL.Realize M ∧ rR.Realize M

Paired model existence. From a root inseparable pair {rL} / {rR} (support-budgeted at A₀, side-typed at (F₁, R₁) / (F₂, R₂), inseparable at the shared vocabulary), over a countable relational vocabulary, there is a single L[[ℕ]]-model realizing both roots. The fair enumeration produces a Henkin-complete S* ⊇ {rL, rR}; its quotient term model realizes every positive member, and both roots enter positively.

theorem FirstOrder.Language.exists_paired_model_neg {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (F₁ : Set ((n : ℕ) × L.Functions n)) (R₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (R₂ : Set ((n : ℕ) × L.Relations n)) (r₁ r₂ : (L.withConstants ℕ).Sentenceω) (hr₁ : (sentenceJConsts r₁).Finite) (hr₂ : (sentenceJConsts r₂).Finite) (hr₁sent : r₁ ∈ SentBnd F₁ R₁) (hr₂sent : BoundedFormulaω.not r₂ ∈ SentBnd F₂ R₂) (A₀ : Finset ℕ) (hsupp : sentenceJConsts r₁ ∪ sentenceJConsts (BoundedFormulaω.not r₂) ⊆ ↑A₀) (hroot : InsepAt (F₁ ∩ F₂) (R₁ ∩ R₂) A₀ {r₁} {BoundedFormulaω.not r₂}) : ∃ (M : Type) (x : (L.withConstants ℕ).Structure M) (_ : Nonempty M), r₁.Realize M ∧ ¬r₂.Realize M

Public wrapper (interpolation polarity). Instantiating rR := r₂.not yields a single model with M ⊨ r₁ and ¬ M ⊨ r₂ — the seed {r₁, r₂.not} (not {r₁, r₂}).