Renaming and weakening free relation variables

Formula.relabelRel renames outer relation variables by an arity-preserving map, leaving every locally bound relation and all first-order variables unchanged. Formula.weakenRel specializes this to adding an unused relation context, so reusable formulas can move beneath new binders without reconstructing their relation atoms.

Main results

• Formula.realize_relabelRel: renaming pulls back the relation valuation.
• Formula.checkPolarity_relabelRel: polarity checks pull back the marking.
• Formula.wellFormed_relabelRel: renaming preserves formation checks, even for noninjective maps.
• Formula.realize_weakenRel: new relation values do not affect a weakened formula.

def Cslib.Logic.FO.Operator.RelVar.mapUnder {Γ Δ : List ℕ} (Λ : List ℕ) (f : {k : ℕ} → RelVar Γ k → RelVar Δ k) {k : ℕ} : RelVar (Λ ++ Γ) k → RelVar (Λ ++ Δ) k

Extend an arity-preserving renaming beneath a fixed prefix of local relation binders.

@[simp]

theorem Cslib.Logic.FO.Operator.RelVar.split_mapUnder {Γ Δ : List ℕ} (Λ : List ℕ) (f : {k : ℕ} → RelVar Γ k → RelVar Δ k) {k : ℕ} (r : RelVar (Λ ++ Γ) k) : split Λ (mapUnder Λ (fun {k : ℕ} => f) r) = Sum.map id f (split Λ r)

Renaming beneath a binder leaves local variables fixed and maps only outer variables.

def Cslib.Logic.FO.Operator.Formula.relabelRel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ Δ : List ℕ} {α : Type w} : ({k : ℕ} → RelVar Γ k → RelVar Δ k) → Formula L shape Γ α → Formula L shape Δ α

Rename only free relation variables, fixing local binders and all first-order variables.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.realize_relabelRel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ Δ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] (I : Interpretation shape M) (φ : Formula L shape Γ α) (f : {k : ℕ} → RelVar Γ k → RelVar Δ k) (ρ : RelEnv Δ M) (v : α → M) : Realize I (relabelRel (fun {k : ℕ} => f) φ) (fun {k : ℕ} => ρ) v ↔ Realize I φ (fun {x : ℕ} (r : RelVar Γ x) => ρ (f r)) v

Relabeling relations is interpreted by pulling back their valuation.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.checkPolarity_relabelRel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ Δ : List ℕ} {α : Type w} (variance : Variances shape) (φ : Formula L shape Γ α) (f : {k : ℕ} → RelVar Γ k → RelVar Δ k) (sign : Bool) (mark : Marking Δ) : (checkPolarity variance (relabelRel (fun {k : ℕ} => f) φ) sign fun {k : ℕ} => mark) = checkPolarity variance φ sign fun {x : ℕ} (r : RelVar Γ x) => mark (f r)

The polarity of renamed relations is checked using the pulled-back marking.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.wellFormed_relabelRel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ Δ : List ℕ} {α : Type w} (policy : Policy shape) (φ : Formula L shape Γ α) (f : {k : ℕ} → RelVar Γ k → RelVar Δ k) : wellFormed policy (relabelRel (fun {k : ℕ} => f) φ) = wellFormed policy φ

Relation renaming leaves all locally checked formation conditions unchanged.

def Cslib.Logic.FO.Operator.Formula.weakenRel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} (Λ : List ℕ) (φ : Formula L shape Γ α) : Formula L shape (Λ ++ Γ) α

Add unused relation binders to the outer context of a reusable formula.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.realize_weakenRel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] (I : Interpretation shape M) (Λ : List ℕ) (φ : Formula L shape Γ α) (δ : RelEnv Λ M) (ρ : RelEnv Γ M) (v : α → M) : Realize I (weakenRel Λ φ) (fun {k : ℕ} => δ.append fun {k : ℕ} => ρ) v ↔ Realize I φ (fun {k : ℕ} => ρ) v

New relation values do not affect a weakened formula.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.wellFormed_weakenRel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} (policy : Policy shape) (Λ : List ℕ) (φ : Formula L shape Γ α) : wellFormed policy (weakenRel Λ φ) = wellFormed policy φ

Adding unused relation binders preserves well-formedness.