The signed occurrence calculus (issue #14, Unit 0 layer 2)

The Methods-level half of Unit 0: the bridge from the signed traversal of Lomega1omega/Polarity.lean to the unsigned relationsIn, and the signed twin of every occurrence law the interpolation kernel consumes — language maps, relabelling, casting, substitution, quantifier blocks, the constant-expansion machinery (abstractConst, genEx, instConst, stripConsts), and the baseRelationsIn calculus.

Layering: the Core file knows nothing of relationsIn, baseRelationsIn, or the Henkin machinery; everything that mentions them lives here.

Acceptance gates of Unit 0 (all in this file or its Core companion):

• positiveRelationsIn_not / negativeRelationsIn_not — the negation swaps (Core);
• relationsIn_eq_signed_union — relationsIn = positive ∪ negative, which is what turns Lyndon into Craig at the occurrence level;
• exact constructor equations for imp, all, iInf, iSup (Core);
• the exact image law relationsInSigned_mapLanguage.

No semantics and no inseparability notions appear in Unit 0.

The bridge to the unsigned occurrence set

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_eq_signed_union {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : φ.relationsIn = φ.positiveRelationsIn ∪ φ.negativeRelationsIn

Acceptance gate: the relation symbols of a formula are exactly those occurring with one of the two signs. This is what makes Craig interpolation a corollary of Lyndon interpolation at the occurrence level.

theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_subset_relationsIn {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ : L.BoundedFormulaω α n) : relationsInSigned s φ ⊆ φ.relationsIn

Language maps, relabelling, casting, substitution

theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_mapLanguage {L : Language} {α : Type} {L' : Language} (g : L →ᴸ L') (s : Bool) {n : ℕ} (φ : L.BoundedFormulaω α n) : relationsInSigned s (mapLanguage g φ) = (fun (p : (n : ℕ) × L.Relations n) => ⟨p.fst, g.onRelation p.snd⟩) '' relationsInSigned s φ

Acceptance gate (exact image law): a language map moves the signed occurrence sets by the symbol map, sign by sign.

theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_castLE {L : Language} {α : Type} (s : Bool) {m n : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaω α m) : relationsInSigned s (castLE h φ) = relationsInSigned s φ

theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_relabel {L : Language} {α β : Type} {n : ℕ} (g : α → β ⊕ Fin n) (s : Bool) {k : ℕ} (φ : L.BoundedFormulaω α k) : relationsInSigned s (relabel g φ) = relationsInSigned s φ

theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_subst {L : Language} {α β : Type} (s : Bool) {n : ℕ} (φ : L.BoundedFormulaω α n) (tf : α → L.Term β) : relationsInSigned s (φ.subst tf) = relationsInSigned s φ

theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_openBounds {L : Language} (s : Bool) {n : ℕ} (φ : L.BoundedFormulaω Empty n) : relationsInSigned s φ.openBounds = relationsInSigned s φ

Finite quantifier blocks

theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_existsBlock {L : Language} {α : Type} (s : Bool) {n k : ℕ} (φ : L.BoundedFormulaω α (n + k)) : relationsInSigned s φ.existsBlock = relationsInSigned s φ

theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_forallBlock {L : Language} {α : Type} (s : Bool) {n k : ℕ} (φ : L.BoundedFormulaω α (n + k)) : relationsInSigned s φ.forallBlock = relationsInSigned s φ

The constant-expansion machinery

theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_abstractConst {L : Language} (j : ℕ) (s : Bool) {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω Empty n) : relationsInSigned s (abstractConst j φ) = relationsInSigned s φ

Constant abstraction does not move the signed occurrence sets.

theorem FirstOrder.Language.relationsInSigned_genEx {L : Language} (j : ℕ) (s : Bool) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.relationsInSigned s (genEx j ρ) = BoundedFormulaω.relationsInSigned s ρ

The existential generalization of a constant does not move the signed occurrence sets.

theorem FirstOrder.Language.relationsInSigned_instConst {L : Language} (c : ℕ) (s : Bool) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : BoundedFormulaω.relationsInSigned s (instConst c φ) = BoundedFormulaω.relationsInSigned s φ

Instantiating a universal at a constant does not move the signed occurrence sets.

The base signed occurrence sets

def FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned {L' : Language} {J α : Type} {n : ℕ} (s : Bool) (φ : (L'.withConstants J).BoundedFormulaω α n) : Set ((n : ℕ) × L'.Relations n)

The base signed occurrence sets of a constant-expansion formula (the constant layer contributes no relation symbols).

Equations

• FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned s φ = {p : (n : ℕ) × L'.Relations n | ⟨p.fst, Sum.inl p.snd⟩ ∈ FirstOrder.Language.BoundedFormulaω.relationsInSigned s φ}

@[reducible, inline]

abbrev FirstOrder.Language.BoundedFormulaω.basePositiveRelations {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) : Set ((n : ℕ) × L'.Relations n)

The relation symbols occurring positively in a constant-expansion formula, read in the base language.

Equations

• φ.basePositiveRelations = FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned true φ

@[reducible, inline]

abbrev FirstOrder.Language.BoundedFormulaω.baseNegativeRelations {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) : Set ((n : ℕ) × L'.Relations n)

The relation symbols occurring negatively in a constant-expansion formula, read in the base language.

Equations

• φ.baseNegativeRelations = FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned false φ

theorem FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned_subset {L' : Language} {J α : Type} {n : ℕ} (s : Bool) (φ : (L'.withConstants J).BoundedFormulaω α n) : baseRelationsInSigned s φ ⊆ φ.baseRelationsIn

theorem FirstOrder.Language.BoundedFormulaω.baseRelationsIn_eq_signed_union {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) : φ.baseRelationsIn = φ.basePositiveRelations ∪ φ.baseNegativeRelations

The base occurrence set splits by sign, exactly as the ambient one does.

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned_falsum {L' : Language} {J α : Type} {n : ℕ} (s : Bool) : baseRelationsInSigned s falsum = ∅

theorem FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned_not {L' : Language} {J α : Type} {n : ℕ} (s : Bool) (φ : (L'.withConstants J).BoundedFormulaω α n) : baseRelationsInSigned s φ.not = baseRelationsInSigned (!s) φ

Negation swaps the base signs.

theorem FirstOrder.Language.BoundedFormulaω.basePositiveRelations_not {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) : φ.not.basePositiveRelations = φ.baseNegativeRelations

Alias gate: positive base occurrences of ¬φ are the negative ones of φ.

theorem FirstOrder.Language.BoundedFormulaω.baseNegativeRelations_not {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) : φ.not.baseNegativeRelations = φ.basePositiveRelations

Alias gate: negative base occurrences of ¬φ are the positive ones of φ.

theorem FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned_imp_left {L' : Language} {J α : Type} {n : ℕ} {s : Bool} {φ ψ : (L'.withConstants J).BoundedFormulaω α n} : baseRelationsInSigned (!s) φ ⊆ baseRelationsInSigned s (φ.imp ψ)

theorem FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned_imp_right {L' : Language} {J α : Type} {n : ℕ} {s : Bool} {φ ψ : (L'.withConstants J).BoundedFormulaω α n} : baseRelationsInSigned s ψ ⊆ baseRelationsInSigned s (φ.imp ψ)

theorem FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned_imp_subset {L' : Language} {J α : Type} {n : ℕ} {A : Set ((n : ℕ) × L'.Relations n)} {s : Bool} {φ ψ : (L'.withConstants J).BoundedFormulaω α n} (h₁ : baseRelationsInSigned (!s) φ ⊆ A) (h₂ : baseRelationsInSigned s ψ ⊆ A) : baseRelationsInSigned s (φ.imp ψ) ⊆ A

theorem FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned_component_iInf {L' : Language} {J α : Type} {n : ℕ} {s : Bool} {φs : ℕ → (L'.withConstants J).BoundedFormulaω α n} (k : ℕ) : baseRelationsInSigned s (φs k) ⊆ baseRelationsInSigned s (iInf φs)

theorem FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned_component_iSup {L' : Language} {J α : Type} {n : ℕ} {s : Bool} {φs : ℕ → (L'.withConstants J).BoundedFormulaω α n} (k : ℕ) : baseRelationsInSigned s (φs k) ⊆ baseRelationsInSigned s (iSup φs)

theorem FirstOrder.Language.BoundedFormulaω.baseRelationsInSigned_iSup_subset {L' : Language} {J α : Type} {n : ℕ} {A : Set ((n : ℕ) × L'.Relations n)} {s : Bool} (φs : ℕ → (L'.withConstants J).BoundedFormulaω α n) (h : ∀ (k : ℕ), baseRelationsInSigned s (φs k) ⊆ A) : baseRelationsInSigned s (iSup φs) ⊆ A

Base signed occurrences of the kernel's atomic sentences

@[simp]

theorem FirstOrder.Language.baseRelationsInSigned_constEq {L : Language} (s : Bool) (a b : ℕ) : BoundedFormulaω.baseRelationsInSigned s (constEq a b) = ∅

A constant equality has no signed base occurrences, in either sign — the syntactic form of "equality is logical".

theorem FirstOrder.Language.basePositiveRelations_relInst {L : Language} {l : ℕ} (R : L.Relations l) (g g' : Fin l → ℕ) : BoundedFormulaω.basePositiveRelations (relInst R g) = BoundedFormulaω.basePositiveRelations (relInst R g')

An atomic relation instance occurs positively only, and its base positive set does not depend on the constant tuple.

theorem FirstOrder.Language.basePositiveRelations_relInst_eq {L : Language} {l : ℕ} (R : L.Relations l) (g : Fin l → ℕ) : BoundedFormulaω.basePositiveRelations (relInst R g) = {⟨l, R⟩}

An atomic relation instance's base positive set is exactly its own symbol.

@[simp]

theorem FirstOrder.Language.baseNegativeRelations_relInst {L : Language} {l : ℕ} (R : L.Relations l) (g : Fin l → ℕ) : BoundedFormulaω.baseNegativeRelations (relInst R g) = ∅

theorem FirstOrder.Language.baseRelationsInSigned_instConst {L : Language} (c : ℕ) (s : Bool) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : BoundedFormulaω.baseRelationsInSigned s (instConst c φ) = BoundedFormulaω.baseRelationsInSigned s φ.all

Universal instantiation does not enlarge the base signed sets.

theorem FirstOrder.Language.baseRelationsInSigned_genEx {L : Language} (j : ℕ) (s : Bool) (ρ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaω.baseRelationsInSigned s (genEx j ρ) = BoundedFormulaω.baseRelationsInSigned s ρ

Existential generalization of a constant does not move the base signed sets.

theorem FirstOrder.Language.baseRelationsInSigned_mapLanguage_withConstants {L : Language} (s : Bool) (r : L.Sentenceω) : BoundedFormulaω.baseRelationsInSigned s (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) r) = BoundedFormulaω.relationsInSigned s r

theorem FirstOrder.Language.basePositiveRelations_mapLanguage_withConstants {L : Language} (r : L.Sentenceω) : (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) r).basePositiveRelations = BoundedFormulaω.positiveRelationsIn r

Alias form of the constant-expansion image law, positive sign (matches the abbrev shape, so rw fires on goals stated with basePositiveRelations).

theorem FirstOrder.Language.baseNegativeRelations_mapLanguage_withConstants {L : Language} (r : L.Sentenceω) : (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) r).baseNegativeRelations = BoundedFormulaω.negativeRelationsIn r

Alias form of the constant-expansion image law, negative sign.

theorem FirstOrder.Language.relationsInSigned_stripConsts {L : Language} {α : Type} (s : Bool) {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω α n) (h : sentenceJConsts φ ⊆ ∅) : BoundedFormulaω.relationsInSigned s (φ.stripConsts h) ⊆ BoundedFormulaω.baseRelationsInSigned s φ

Stripping a constant-free formula keeps the signed occurrences inside the base signed set.