The budgeted labelled pair (issue #15, side-labelled restart)

The certificate selected by docs/malitz-source-reconstruction-2.md: Feferman's Theorem 4.3 keeps the two sides labelled — formulas are retained on their derivational side, never reprojected by vocabulary — and carries three conditions along the derivation beside the two entailments:

• the shared vocabulary condition on the separator;
• the shared constant condition, sentenceJConsts θ ⊆ theoryJConsts Γ ∩ theoryJConsts Δ (Feferman's Free₀(θ) ⊆ Free₀(ϕ) ∩ Free₀(ψ), in the constant presentation);
• the two quantifier permissions, hasQuantSigned true θ → HasQuantSigned true Γ and hasQuantSigned false θ → HasQuantSigned true Δ.

The second permission reads true on the right because Δ holds the negated consequent: at the root Un({r₂.not}) = Ex(r₂).

The shared-constant condition is primary, not derived from the permissions. That is the source's own account: "in building up an interpolant following a cut-free derivation … we are forced to introduce quantifiers into the interpolant only as required to maintain the condition (iii), and that turns out to lead to (iv)" (Feferman, "Ah, Chu!", pp. 2–3). The earlier FefermanAllowed had the dependency backwards, charging constants into the permissions as a standing assumption.

Everything the canonical-projection experiment needed disappears here. A fresh witness constant is added to one labelled side; being absent from the other, the shared-constant condition forbids the separator from mentioning it, so the separator transports unchanged — no genEx, no genAll, no support parameter to strip, no projection coverage, and no root tags. Quantifier non-growth is likewise immediate, because the quantified parent already sits on the same labelled side.

Methods/Interpolation/FefermanProjection.lean is not imported: it is retained as experimental evidence for the canonical-projection route and its C1 failure, not as a dependency.

Provenance

The labelled architecture is source-backed by Feferman's split-sequent proof, which he describes explicitly. The semantic consistency-property implementation below is this repository's adaptation: Stern's model-theoretic forcing proof is identified as the semantic dual, but its exact invariant is unverified — the paper has not been read.

The constant support of a labelled side

def FirstOrder.Language.theoryJConsts {L : Language} (T : Set (L.withConstants ℕ).Sentenceω) : Set ℕ

The Henkin constants occurring anywhere in a set of sentences.

Equations

• FirstOrder.Language.theoryJConsts T = ⋃ σ ∈ T, FirstOrder.Language.sentenceJConsts σ

@[simp]

theorem FirstOrder.Language.theoryJConsts_insert {L : Language} {T : Set (L.withConstants ℕ).Sentenceω} {σ : (L.withConstants ℕ).Sentenceω} : theoryJConsts (insert σ T) = sentenceJConsts σ ∪ theoryJConsts T

The certificate

def FirstOrder.Language.BudgetedPairSeparates {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)) (Γ Δ : Set (L.withConstants ℕ).Sentenceω) (θ : (L.withConstants ℕ).Sentenceω) : Prop

A budgeted separator of the labelled pair (Γ, Δ). Five conditions: the two entailments, the shared vocabulary, the shared constants, and the two quantifier permissions.

Equations

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

def FirstOrder.Language.BudgetedPairInsep {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)) (Γ Δ : Set (L.withConstants ℕ).Sentenceω) : Prop

The invariant: the labelled pair admits no budgeted separator.

Equations

• FirstOrder.Language.BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ = ¬∃ (θ : (L.withConstants ℕ).Sentenceω), FirstOrder.Language.BudgetedPairSeparates F₁ R₁ F₂ R₂ Γ Δ θ

Order behaviour of the invariant

Inseparability is antitone: a separator of a smaller labelled pair is still a separator of any larger one, because all five conditions weaken the right way — entailment survives adding premises, the constant condition survives enlarging the supports, and both permissions survive enlarging the sides. Contrapositively, inseparability of the larger pair gives it for every sub-pair.

This is what lets a discharge transfer a premise onto a side temporarily and then drop it again.

C0 — the mixed contradiction gate

The diagnostic case for the labelled architecture: a sentence on the left with its negation on the right. All five conditions are paid by the two memberships themselves.

C1 — implication branching

The source's rule verbatim: disjunction when the principal formula is on the left, conjunction when on the right. There is no leakage case to consider — the branch sentences join the side their parent is on, and nowhere else.

The fresh-witness rules

The payoff of labelling. A witness constant c fresh for both sides is added to one of them. Freshness on the opposite side is what forbids the separator from mentioning c — via the shared-constant condition — so the separator transports unchanged; freshness on the own side is what moves the entailment. No constant abstraction appears anywhere.

The root collapse and the interpolant equation

theorem FirstOrder.Language.isUniversal_of_budgetedPairSeparates {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {θ : (L.withConstants ℕ).Sentenceω} (h : BudgetedPairSeparates F₁ R₁ F₂ R₂ Γ Δ θ) (hΔ : ¬Theoryω.HasQuantSigned true Δ) : BoundedFormulaω.IsUniversal θ

Root collapse. A budgeted separator against a right side with no universal occurrence is universal; against constant-free sides it is constant-free.

theorem FirstOrder.Language.sentenceJConsts_eq_empty_of_budgetedPairSeparates {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {θ : (L.withConstants ℕ).Sentenceω} (h : BudgetedPairSeparates F₁ R₁ F₂ R₂ Γ Δ θ) (hΓ : theoryJConsts Γ = ∅) : sentenceJConsts θ = ∅

The family shell

BudgetedPairMem is the existential labelled decomposition: the scheduler still completes the single set S, while every membership proof retains the labels the closure argument uses. A shared formula is never automatically duplicated — but, S = Γ ∪ Δ permitting overlap, a discharge may choose a decomposition in which it appears on both sides, which is exactly what the cross-label transfer gates below license.

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

Membership in the labelled family: some finite, GenU-bounded, side-typed decomposition of S whose labelled pair is budget-inseparable.

Equations

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

Fresh constants for a labelled pair

Γ.Finite alone is not enough: a single infinitary sentence can mention infinitely many constants. Finiteness of the support needs the GenU bound as well, via genU_finite_support, together with finite constant support of the two roots.

C0, the remaining label combination

Shared-hypothesis transfer

Duplicating a quantifier-free shared sentence onto the other label. The separator becomes σ.imp θ (resp. σ.and θ), and the price is exactly that σ's constants already occur on the receiving side — the shared-constant condition is what charges it.

Cross-label equality and relation transfer

The mixed rel_congr case, which was load-bearing in Craig's paired construction and is the likeliest hidden obstruction here: the relation atom is on the left, the equality atom on the right. The derived atom mentions a constant b that only the right side carries, so the separator of the extended pair may mention b; substituting the equality's shared partner g i for b removes it, and the shared-constant condition pays for it — g i occurs on both sides. No quantifier is introduced, so both budgets are untouched.

Generic insertion drivers

Every deterministic field is an instance of the same statement: the new sentence is entailed by the side that receives it, and both its constants and its positive quantifier occurrences are already carried there. The three obligations stay separate on purpose — the proof's content is which label received the formula.

The deterministic connective fields

C2 (double negation), C1′ (negated implication, both components), C3 (conjunction component) and C4′ (negated-disjunction component), on each label. Each is three obligations against the parent.

Countable branching — the last isolated gate

The ⋁-style fields, where the consumer must choose a component. Each is proved by contraposition: assume every component extension is separable, choose its separator θₙ, combine with iSup or iInf according to the label, and check the five conditions componentwise.

Three things are worth watching, and all three come out clean:

• the combined separator's constant support is the union of the component supports, and each component support already lies in both theory supports — because inserting a component does not enlarge the receiving side's support, the parent already carrying its constants;
• hasQuantSigned on iSup/iInf exposes one offending component, so the permission flows from that component's separator and then from the parent formula, again by non-growth;
• no label projection and no support enlargement appears anywhere.

The substitution cut, and the mixed equality cases

Mixed eq_trans is the one equality case the shared-hypothesis transfer cannot reach: with a = b on the left and b = d on the right, neither side's support contains both endpoints — the pivot b is the only automatically shared constant. The substitution mechanism that solved mixed rel_congr solves it too, and the two statements genuinely align, so the common core is extracted once.

The remaining equality fields

eq_refl, eq_symm, and same-label eq_trans, on each label. All are entailed-insertion driver applications: the atoms are quantifier-free, so the budget obligations are vacuous, and only the constant obligation carries information.

Same-side relation congruence, and the right eq_refl twin

The two remaining atomic fields. Both are deterministic: the new sentence is entailed by the receiving side, its constants are already carried there, and being atomic it contributes no quantifier occurrence at either sign — so each is an instance of the corresponding driver.

Universal instantiation — the all_inst gate

The first field whose new sentence can carry a constant the side does not yet own. Two facts make it go through without strengthening the invariant:

• the quantifier budget collapses: the inserted instance can only add occurrences that the universal parent φ.all, already on the same side, pays for;
• the constant support grows by at most {c}, so a separator that survives the insertion either never mentioned c (and transports unchanged) or can be universally generalized over it.

The family-level field helpers

One helper per ConsistencyPropertyEqOn field, each stated in the structure's own S ∪ {φ} shape so that the final package is pure eta-application. Every body follows the same four steps: unpack the labelled decomposition, dispatch on the label of the parent, apply one BudgetedPairInsep gate, and repackage with budgetedPairMem_insert_left/_right. The insert-versus-union normalization is hidden here via Set.union_singleton.

No semantic realization proof appears below; if one is ever needed, a gate is missing.

The four countable-connective fields

The two ∀ k fields select the component up front; the two ∃ k fields unpack the gate's witness and return the same k, so the GenU, SentBnd and insertion obligations visibly concern one component. No witness is constructed here.

The equality fields

The initial family member

Two named facts, deliberately separate. The structural one is pure packaging: a labelled pair of singletons, with the generated universe instantiated at those very roots so both GenU obligations are literally root₁_mem/root₂_mem. The logical one supplies its hypothesis, and is where the interpolation assumption enters — note the root pair is inseparable because no admissible interpolant exists, not because of the entailment r₁ ⊨ r₂, which is consumed only at the very end against the extracted model.

theorem FirstOrder.Language.budgetedPairMem_root {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {ρ₁ ρ₂ : (L.withConstants ℕ).Sentenceω} (hb₁ : ρ₁ ∈ SentBnd F₁ R₁) (hb₂ : ρ₂ ∈ SentBnd F₂ R₂) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ {ρ₁} {ρ₂}) : BudgetedPairMem ρ₁ ρ₂ F₁ R₁ F₂ R₂ ({ρ₁} ∪ {ρ₂})

Structural root member. Packaging only; no semantic content.

The consistency property

Pure wiring: every field is its named helper. Nothing below reasons about separators, labels or supports — if a field ever needs more than an application, the corresponding helper is missing.

def FirstOrder.Language.budgetedPairConsistencyProperty {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)) (r₁ r₂ : (L.withConstants ℕ).Sentenceω) (hr₁ : (sentenceJConsts r₁).Finite) (hr₂ : (sentenceJConsts r₂).Finite) : ConsistencyPropertyEqOn (GenU r₁ r₂)

The budgeted labelled-pair consistency property. The finite labelled family over the generated universe GenU r₁ r₂. Root-support finiteness is consumed only by neg_all_witness.

Equations

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