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.realize_genAll {L : Language} {M : Type} (base : L.Structure M) (h : ℕ → M) (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.Realize (genAll j ρ) Empty.elim Fin.elim0 ↔ ∀ (x : M), BoundedFormulaω.Realize ρ Empty.elim Fin.elim0

Realizing the universal generalization is realizing the original at every reinterpretation of c_j.

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.functionsIn_genAll_subset {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.functionsIn (genAll j ρ) ⊆ BoundedFormulaω.functionsIn ρ

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

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

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.BoundedFormulaω.universalSigned_abstractConst {L : Language} (j : ℕ) (s : Bool) {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω Empty n) : universalSigned s (abstractConst j φ) ↔ universalSigned s φ

Constant abstraction does not move the quantifier class.

theorem FirstOrder.Language.isUniversal_genAll {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.IsUniversal (genAll j ρ) ↔ BoundedFormulaω.IsUniversal ρ

genAll is class-preserving: universally generalizing a fresh constant out of a universal sentence leaves it universal. This is the whole point of the right-hand C7 trigger.

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.

theorem FirstOrder.Language.not_isUniversal_genEx {L : Language} (j : ℕ) (ρ : (L.withConstants ℕ).Sentenceω) : ¬BoundedFormulaω.IsUniversal (genEx j ρ)

genEx is not class-preserving, recorded separately: genEx j ρ is never universal, since it is a negatively-occurring all. This is a fact about the construction, and is not by itself a failure of the left closure (see malitzInsepAt_witness_of_existentialDelta).

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 {L : Language} {j : ℕ} {φc σc : (L.withConstants ℕ).Sentenceω} {Δ : Set (L.withConstants ℕ).Sentenceω} (hfresh : ∀ δ ∈ Δ, j ∉ sentenceJConsts δ) (hyp : (insert φc Δ).Entails (BoundedFormulaω.not σc)) : (insert (genEx j φc) Δ).Entails (BoundedFormulaω.not (genAll j σc))

Acceptance, Δ side: Δ, δ(c) ⊨ ¬σ(c) upgrades to Δ, ∃x δ(x) ⊨ ¬∀x σ(x) when c_j is fresh for Δ. The witness for ∃x δ(x) is exactly the reinterpretation that refutes ∀x σ(x).

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.

Bounds for the countable conjunction of a theory

theorem FirstOrder.Language.isExistential_conjunction {L : Language} (T : (L.withConstants ℕ).Theoryω) (hT : Set.Countable T) (h : ∀ σ ∈ T, BoundedFormulaω.IsExistential σ) : BoundedFormulaω.IsExistential (T.conjunction hT)

A countable conjunction of existential sentences is existential.

theorem FirstOrder.Language.baseFunctionsIn_conjunction_subset {L : Language} {F : Set ((n : ℕ) × L.Functions n)} (T : (L.withConstants ℕ).Theoryω) (hT : Set.Countable T) (h : ∀ σ ∈ T, BoundedFormulaω.baseFunctionsIn σ ⊆ F) : BoundedFormulaω.baseFunctionsIn (T.conjunction hT) ⊆ F

theorem FirstOrder.Language.baseRelationsIn_conjunction_subset {L : Language} {R : Set ((n : ℕ) × L.Relations n)} (T : (L.withConstants ℕ).Theoryω) (hT : Set.Countable T) (h : ∀ σ ∈ T, BoundedFormulaω.baseRelationsIn σ ⊆ R) : BoundedFormulaω.baseRelationsIn (T.conjunction hT) ⊆ R

theorem FirstOrder.Language.sentenceJConsts_conjunction_subset {L : Language} (T : (L.withConstants ℕ).Theoryω) (hT : Set.Countable T) {A : Set ℕ} (h : ∀ σ ∈ T, sentenceJConsts σ ⊆ A) : sentenceJConsts (T.conjunction hT) ⊆ A