The budgeted labelled pair's countermodel (issue #15) #
Turns the completion of the labelled root pair into an actual model: from budgeted inseparability of
({r₁}, {r₂.not}) — which by budgetedPairInsep_root_of_no_interpolant follows from absence of an
admissible interpolant — a structure satisfying r₁ and refuting r₂.
This is the countermodel that contradicts r₁ ⊨ r₂ in the final interpolation argument.
Boundaries #
[L.IsRelational]enters here, as the quotient term model requires it; the completion step does not.- Relation-symbol countability is inherited from the completion step and is consumed only there.
- Both labelled roots are read off with the positive truth direction, matching how the family was seeded; the negative direction of the truth lemma is discarded, so no polarity argument is needed.
theorem
FirstOrder.Language.exists_budgetedPair_model
{L : Language}
[L.IsRelational]
[Countable ((l : ℕ) × L.Relations l)]
{F₁ F₂ : Set ((n : ℕ) × L.Functions n)}
{R₁ R₂ : Set ((n : ℕ) × L.Relations n)}
{r₁ r₂ : (L.withConstants ℕ).Sentenceω}
(hr₁ : (sentenceJConsts r₁).Finite)
(hr₂ : (sentenceJConsts r₂).Finite)
(hroot : BudgetedPairMem r₁ (BoundedFormulaω.not r₂) F₁ R₁ F₂ R₂ ({r₁} ∪ {BoundedFormulaω.not r₂}))
:
The model endpoint. A labelled root member yields a model of r₁ refuting r₂.