The polarity side bound and the one-sided closures (issue #14, Unit 3)

SentBndPol F P N is the polarity refinement of SentBnd F R: a sentence whose base function symbols lie in F, whose base positively occurring relations lie in P, and whose base negatively occurring relations lie in N.

The directional discipline. Negation does not preserve the class — it exchanges the two polarity components:

σ.not ∈ SentBndPol F P N  ↔  σ ∈ SentBndPol F N P

so the unsigned sentBnd_not_iff must not be ported as a same-class equivalence. The subformula rules are correspondingly directional: from φ.imp ψ ∈ SentBndPol F P N one gets φ.not and ψ in the same class (never φ itself), and from (φ.imp ψ).not ∈ SentBndPol F P N one gets φ and ψ.not in the same class. These are exactly the shapes the consistency-property fields consume, and they are what make the side bound stable under the closure rules.

Atoms: a constant equality lies in every class (empty signed sets — equality is logical), while an atomic relation instance is positive-only: relInst R g ∈ SentBndPol F P N ↔ ⟨l, R⟩ ∈ P, never requiring or granting ⟨l, R⟩ ∈ N.

The rest of the file is the one-sided LyndonInsepAt closure suite: entailment insertion and support monotonicity (separator unchanged), the iSup / negated-iInf component selections (separator ⨆ σ), falsum and internal contradiction (separator ⊥), and the fresh-support and quantifier round-trip steps (separator genEx c σ) — every one of them polarity-clean, by the signed calculus.

Not here (Unit 4+): the paired-family predicate, the cross-coordinate C0 and relation-congruence assembly, the ConsistencyPropertyEqOn instance, and any Henkin invocation — and, as of the Unit-3 layering cleanup, not in the dependency cone either: the unsigned base-symbol projections this file consumes now live in the neutral Methods/Interpolation/BaseOccurrenceProjections.lean, whose own cone stops at the generated universe.

The polarity side bound

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

Side vocabulary bound, polarity-refined.

Equations

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

theorem FirstOrder.Language.mem_sentBndPol_iff {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {σ : (L.withConstants ℕ).Sentenceω} : σ ∈ SentBndPol F P N ↔ BoundedFormulaω.baseFunctionsIn σ ⊆ F ∧ BoundedFormulaω.basePositiveRelations σ ⊆ P ∧ BoundedFormulaω.baseNegativeRelations σ ⊆ N

theorem FirstOrder.Language.sentBndPol_not_iff {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {σ : (L.withConstants ℕ).Sentenceω} : BoundedFormulaω.not σ ∈ SentBndPol F P N ↔ σ ∈ SentBndPol F N P

Negation exchanges the polarity components — the directional fact that replaces the unsigned sentBnd_not_iff. It is not a same-class equivalence.

Directional subformula rules

theorem FirstOrder.Language.sentBndPol_imp_neg_left {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {φ ψ : (L.withConstants ℕ).Sentenceω} (h : BoundedFormulaω.imp φ ψ ∈ SentBndPol F P N) : BoundedFormulaω.not φ ∈ SentBndPol F P N

From an implication in the class, the negated antecedent is in the same class (the antecedent itself need not be).

theorem FirstOrder.Language.sentBndPol_imp_right {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {φ ψ : (L.withConstants ℕ).Sentenceω} (h : BoundedFormulaω.imp φ ψ ∈ SentBndPol F P N) : ψ ∈ SentBndPol F P N

From an implication in the class, the consequent is in the same class.

theorem FirstOrder.Language.sentBndPol_neg_imp_left {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {φ ψ : (L.withConstants ℕ).Sentenceω} (h : (BoundedFormulaω.imp φ ψ).not ∈ SentBndPol F P N) : φ ∈ SentBndPol F P N

From a negated implication in the class, the antecedent is in the same class.

theorem FirstOrder.Language.sentBndPol_neg_imp_right {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {φ ψ : (L.withConstants ℕ).Sentenceω} (h : (BoundedFormulaω.imp φ ψ).not ∈ SentBndPol F P N) : BoundedFormulaω.not ψ ∈ SentBndPol F P N

From a negated implication in the class, the negated consequent is in the same class.

theorem FirstOrder.Language.sentBndPol_not_not {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {φ : (L.withConstants ℕ).Sentenceω} (h : (BoundedFormulaω.not φ).not ∈ SentBndPol F P N) : φ ∈ SentBndPol F P N

Double negation stays in the class.

Components of the countable connectives

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

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

theorem FirstOrder.Language.sentBndPol_neg_component_iInf {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) (h : (BoundedFormulaω.iInf φs).not ∈ SentBndPol F P N) : BoundedFormulaω.not (φs k) ∈ SentBndPol F P N

The negated-component rules used by C3' and C4': a negated countable connective in the class yields negated components in the same class.

theorem FirstOrder.Language.sentBndPol_neg_component_iSup {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) (h : (BoundedFormulaω.iSup φs).not ∈ SentBndPol F P N) : BoundedFormulaω.not (φs k) ∈ SentBndPol F P N

Substitution and the atoms

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

Universal instantiation stays in the class.

theorem FirstOrder.Language.sentBndPol_constEq {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} (a b : ℕ) : constEq a b ∈ SentBndPol F P N

A constant equality lies in every side class: its signed base sets are empty in both signs. This is the syntactic form of "equality is logical".

theorem FirstOrder.Language.sentBndPol_relInst_iff {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {l : ℕ} (R : L.Relations l) (g : Fin l → ℕ) : relInst R g ∈ SentBndPol F P N ↔ ⟨l, R⟩ ∈ P

Atomic relation instances are positive-only: membership in the side class is exactly membership of the symbol in the positive component. It never requires — and never grants — membership in N.

theorem FirstOrder.Language.sentBndPol_relInst_congr {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {l : ℕ} (R : L.Relations l) {g : Fin l → ℕ} (g' : Fin l → ℕ) (h : relInst R g ∈ SentBndPol F P N) : relInst R g' ∈ SentBndPol F P N

Congruence: the side class does not see the constant tuple of an atomic instance.

The one-sided closures: separator unchanged

theorem FirstOrder.Language.lyndonInsepAt_insert_of_entails {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).Sentenceω} (hcons : Theoryω.Entails Γ φ) (h : LyndonInsepAt F P N A Γ Δ) : LyndonInsepAt F P N A (insert φ Γ) Δ

Adding a Γ-consequence keeps inseparability (the separator is unchanged).

theorem FirstOrder.Language.lyndonInsepAt_mono_support {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {B : Finset ℕ} (hAB : A ⊆ B) (h : LyndonInsepAt F P N B Γ Δ) : LyndonInsepAt F P N A Γ Δ

Shrinking the allowed-support budget keeps inseparability.

The one-sided closures: component selection (separator ⨆ σ)

theorem FirstOrder.Language.lyndonInsepAt_iSup_component {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hmem : BoundedFormulaω.iSup φs ∈ Γ) (h : LyndonInsepAt F P N A Γ Δ) : ∃ (k : ℕ), LyndonInsepAt F P N A (insert (φs k) Γ) Δ

C4 (countable disjunction): a disjunction in Γ has a component preserving inseparability.

theorem FirstOrder.Language.lyndonInsepAt_neg_iInf_component {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hmem : (BoundedFormulaω.iInf φs).not ∈ Γ) (h : LyndonInsepAt F P N A Γ Δ) : ∃ (k : ℕ), LyndonInsepAt F P N A (insert (BoundedFormulaω.not (φs k)) Γ) Δ

C3' (negated conjunction): a negated conjunction in Γ splits off a negated component.

The one-sided closures: falsum and internal contradiction (separator ⊥)

theorem FirstOrder.Language.lyndonInsepAt_falsum_absurd {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.falsum ∈ Γ) (h : LyndonInsepAt F P N A Γ Δ) : False

theorem FirstOrder.Language.lyndonInsepAt_contradiction_absurd {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).Sentenceω} (h1 : φ ∈ Γ) (h2 : BoundedFormulaω.not φ ∈ Γ) (h : LyndonInsepAt F P N A Γ Δ) : False

The one-sided closures: fresh support and the quantifier round trip (separator genEx)

theorem FirstOrder.Language.lyndonInsepAt_grow_fresh {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (hcΔ : ∀ δ ∈ Δ, c ∉ sentenceJConsts δ) (h : LyndonInsepAt F P N A Γ Δ) : LyndonInsepAt F P N (insert c A) Γ Δ

Fresh-support growth: the budget may be grown by a constant fresh for Δ; the separator is existentially generalized, which is sign-preserving (two flips cancel).

theorem FirstOrder.Language.lyndonInsepAt_witness_of_genEx {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (φc : (L.withConstants ℕ).Sentenceω) (hcΓ : ∀ γ ∈ Γ, c ∉ sentenceJConsts γ) (hcΔ : ∀ δ ∈ Δ, c ∉ sentenceJConsts δ) (h : LyndonInsepAt F P N A (insert (genEx c φc) Γ) Δ) : LyndonInsepAt F P N (insert c A) (insert φc Γ) Δ

The quantifier round trip (C7): a separator of the witness-instantiated pair at support insert c A abstracts to a separator of the existential pair at A, so inseparability descends to the witness instance. The separator is genEx c σ, again sign-preserving.