Signed occurrences through the relationalization layer (issue #14, Unit 6 — the D6 gate)

The polarity bookkeeping of the graph translation, in three gates.

Gate 1 — the atomic calculus. Term graphs are positive-only: termGraphAux is built from graph atoms by conjunction, einf, and existential blocks — all sign-preserving — so its negative set is empty and its positive set is the whole graphRelSym-image. The graph axioms, by contrast, do use their graph relations in both signs (functionality has one in an antecedent); what matters is that they contribute no base-relation occurrence in either sign (relationsInSigned_graphAxioms_inter_base), which is why the identities below are insensitive to whether the axioms sit in a conjunction or an antecedent.

Gate 2 — base-polarity preservation (the stop/go equation).

relationsInSigned s (relationalizeFormula φ) ∩ Set.range (baseRelSym L)
  = baseRelSym L '' relationsInSigned s φ

Relationalization preserves base-relation polarity on the nose, in the audit's exact image/intersection form, with positiveRelationsIn/negativeRelationsIn corollaries and preimage-shaped consumer lemmas.

Gate 3 — back-translation.

relationsInSigned s (backTranslateFormula θ) = baseRelSym L ⁻¹' relationsInSigned s θ

Here the key acceptance fact lands: a graph atom back-translates to an equality, whose signed sets are empty in both signs. So graph relations may carry arbitrary polarity in the graph world and still disappear harmlessly. Composing the two gates gives the exact base-polarity identities for Craig's graph antecedent (graphAxioms F).and (relationalizeFormula r) and consequent (graphAxioms F).imp (relationalizeFormula r).

Symbol-range disjointness

Gate 1: the atomic calculus — term graphs are positive-only

Gate 2: base-polarity preservation (the stop/go equation)

Gate 3: back-translation

theorem FirstOrder.Language.positiveRelationsIn_backTranslateFormula {L : Language} {α : Type} {n : ℕ} (θ : L.graphLanguage.BoundedFormulaω α n) : (backTranslateFormula θ).positiveRelationsIn = L.baseRelSym ⁻¹' θ.positiveRelationsIn

Gate 3, positive corollary.

theorem FirstOrder.Language.negativeRelationsIn_backTranslateFormula {L : Language} {α : Type} {n : ℕ} (θ : L.graphLanguage.BoundedFormulaω α n) : (backTranslateFormula θ).negativeRelationsIn = L.baseRelSym ⁻¹' θ.negativeRelationsIn

Gate 3, negative corollary.

The base-polarity identities for Craig's graph roots

theorem FirstOrder.Language.preimage_baseRelSym_graphAnd {L : Language} (s : Bool) (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] (φ : L.Sentenceω) : L.baseRelSym ⁻¹' BoundedFormulaω.relationsInSigned s (BoundedFormulaω.and (graphAxioms F) (relationalizeFormula φ)) = BoundedFormulaω.relationsInSigned s φ

Preimage form of the graph-antecedent identity — the shape the endpoint consumes, so that no Sigma/definitional-equality friction leaks into the assembly.

theorem FirstOrder.Language.preimage_baseRelSym_graphImp {L : Language} (s : Bool) (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] (φ : L.Sentenceω) : L.baseRelSym ⁻¹' BoundedFormulaω.relationsInSigned s (BoundedFormulaω.imp (graphAxioms F) (relationalizeFormula φ)) = BoundedFormulaω.relationsInSigned s φ

Preimage form of the graph-consequent identity: the axioms sit in an antecedent, so the implication flips their sign — and they still contribute nothing to the base part.