Constant generalization: the ∀-twin of genEx, and countable-conjunction bounds

Neutral companion to ConstantElimination.lean. Where genEx j ρ existentially generalizes the constant c_j out of a sentence, genAll j ρ generalizes it universally, with the matching realization lemma, occurrence calculus, and the two entailment-acceptance sequents:

• entails_genAll_of_entails (side 1): Γ ⊨ σ(c) ⟹ Γ ⊨ ∀x σ(x), c fresh for Γ. Unlike genEx's side-1 sequent this genuinely needs freshness — ∀-introduction is not weakening;
• entails_not_genAll_of_entails_not (side 2): Δ, δ(c) ⊨ ¬σ(c) ⟹ Δ, ∃x δ(x) ⊨ ¬∀x σ(x), c fresh for Δ.

genAll is class-preserving for the quantifier hierarchy of Lomega1omega/QuantifierClass.lean (isUniversal_genAll), because all is admissible at the universal sign and neither constant abstraction nor relabel moves the class; genEx, dually, is never universal (not_isUniversal_genEx). That pair of facts is what makes an asymmetric separator class possible at all, so both live here rather than inside any one consumer.

The second half collects the class and occurrence bounds for Theoryω.conjunction, the countable conjunction of a theory: existentiality and the three symbol/support bounds descend from the members.

Nothing here is specific to Malitz interpolation (issue #15) or to end extensions (issue #16); both consume it.

genAll: universal generalization of a fresh constant

noncomputable def FirstOrder.Language.genAll {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : (L.withConstants ℕ).Sentenceω

Universally generalize the constant c_j out of a sentence: abstract c_j into the free variable 0, then universally quantify it. The ∀-twin of genEx.

Equations

• FirstOrder.Language.genAll j ρ = (FirstOrder.Language.BoundedFormulaω.relabel Sum.inr (FirstOrder.Language.BoundedFormulaω.abstractConst j ρ)).all

theorem FirstOrder.Language.notMem_sentenceJConsts_genAll {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : j ∉ sentenceJConsts (genAll j ρ)

c_j is not in the constant support of its own universal generalization.

Occurrence facts for genAll

theorem FirstOrder.Language.baseFunctionsIn_genAll_subset {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.baseFunctionsIn (genAll j ρ) ⊆ BoundedFormulaω.baseFunctionsIn ρ

theorem FirstOrder.Language.baseRelationsIn_genAll {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.baseRelationsIn (genAll j ρ) = BoundedFormulaω.baseRelationsIn ρ

theorem FirstOrder.Language.sentenceJConsts_genAll_subset {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : sentenceJConsts (genAll j ρ) ⊆ sentenceJConsts ρ

The quantifier class of genAll (and the genEx non-fact)

theorem FirstOrder.Language.hasQuantSigned_genAll {L : Language} (j : ℕ) (s : Bool) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.hasQuantSigned s (genAll j ρ) ↔ s = true ∨ BoundedFormulaω.hasQuantSigned s ρ

The exact signed-occurrence equation for genAll. Universal generalization adds one positive occurrence and moves nothing else: at sign true the right disjunct is absorbed, and at sign false the occurrences are exactly those of ρ.

This is what lets a labelled budget absorb a generalization whose universal parent already sits on the same side.

theorem FirstOrder.Language.hasQuantSigned_genEx {L : Language} (j : ℕ) (s : Bool) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.hasQuantSigned s (genEx j ρ) ↔ s = false ∨ BoundedFormulaω.hasQuantSigned s ρ

The exact signed-occurrence equation for genEx, the dual of hasQuantSigned_genAll: existential generalization adds one negative occurrence and moves nothing else.

The genAll acceptance sequents

theorem FirstOrder.Language.entails_genAll_of_entails {L : Language} {j : ℕ} {σc : (L.withConstants ℕ).Sentenceω} {Γ : Set (L.withConstants ℕ).Sentenceω} (hfresh : ∀ γ ∈ Γ, j ∉ sentenceJConsts γ) (hyp : Theoryω.Entails Γ σc) : Theoryω.Entails Γ (genAll j σc)

Acceptance, Γ side: Γ ⊨ σ(c) upgrades to Γ ⊨ ∀x σ(x) when c_j is fresh for Γ. Unlike genEx's Γ-side sequent this genuinely needs freshness — ∀-introduction is not weakening.

theorem FirstOrder.Language.entails_not_genAll_of_entails_not_self {L : Language} {j : ℕ} {σc : (L.withConstants ℕ).Sentenceω} {Δ : Set (L.withConstants ℕ).Sentenceω} (hyp : Theoryω.Entails Δ (BoundedFormulaω.not σc)) : Theoryω.Entails Δ (BoundedFormulaω.not (genAll j σc))

Negative acceptance without freshness. If Δ already refutes σ(c), it refutes ∀x σ(x) outright: the universal is instantiated at c's own interpretation, so nothing has to be fresh for Δ and no witness is consumed.

This is the shape a labelled pair needs when the separator is abstracted on the side that does not own c; entails_not_genAll_of_entails_not is the different, witness-passing sequent.