Capture-avoiding relation renaming

Arity-preserving relation renaming preserves satisfaction under the pulled-back environment, exact syntactic size, FO matrices, and existential SO prefixes. Identity and composition hold as equalities of formulas. Weakening inserts an unused relation binder, which is the basic operation for merging SO witnesses.

theorem Complexity.DescriptiveComplexity.RelRenaming.ext {rctx sctx : List Nat} (f g : RelRenaming rctx sctx) (h : f.index = g.index) : f = g

A relation renaming is determined by its map on indices.

theorem Complexity.DescriptiveComplexity.RelRenaming.ext_iff {rctx sctx : List Nat} {f g : RelRenaming rctx sctx} : f = g ↔ f.index = g.index

@[simp]

theorem Complexity.DescriptiveComplexity.RelRenaming.lift_id (rctx : List Nat) (k : Nat) : (id rctx).lift k = id (k :: rctx)

Lifting fixes the identity renaming.

theorem Complexity.DescriptiveComplexity.RelRenaming.lift_comp {rctx sctx tctx : List Nat} (g : RelRenaming sctx tctx) (f : RelRenaming rctx sctx) (k : Nat) : (g.comp f).lift k = (g.lift k).comp (f.lift k)

Lifting commutes with composition.

@[simp]

theorem Complexity.DescriptiveComplexity.RelRenaming.pull_id {card : Nat} {rctx : List Nat} (ρ : REnv card rctx) : (id rctx).pull ρ = ρ

Pulling an environment through the identity does nothing.

theorem Complexity.DescriptiveComplexity.RelRenaming.pull_comp {rctx sctx tctx : List Nat} (g : RelRenaming sctx tctx) (f : RelRenaming rctx sctx) {card : Nat} (ρ : REnv card tctx) : (g.comp f).pull ρ = f.pull (g.pull ρ)

Pullback reverses the order of composition.

@[simp]

theorem Complexity.DescriptiveComplexity.RelRenaming.pull_lift_rCons {rctx sctx : List Nat} (f : RelRenaming rctx sctx) {card k : Nat} (S : (Fin k → Fin card) → Prop) (ρ : REnv card sctx) : (f.lift k).pull (rCons S ρ) = rCons S (f.pull ρ)

A lifted renaming preserves the freshly bound relation.

@[simp]

theorem Complexity.DescriptiveComplexity.RelRenaming.pull_weaken_rCons {rctx : List Nat} {card k : Nat} (S : (Fin k → Fin card) → Prop) (ρ : REnv card rctx) : (weaken rctx k).pull (rCons S ρ) = ρ

Weakening ignores the freshly bound relation.

theorem Complexity.DescriptiveComplexity.SOFormula.renameRel_sat {V : Vocabulary} {rctx sctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (f : RelRenaming rctx sctx) (A : FinStruct V) (σ : Env A.card n) (ρ : REnv A.card sctx) : Sat A σ ρ (renameRel f φ) ↔ Sat A σ (f.pull ρ) φ

Satisfaction after relation renaming is satisfaction in the pulled-back environment.

theorem Complexity.DescriptiveComplexity.SOFormula.renameRel_weaken_sat {V : Vocabulary} {rctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (A : FinStruct V) (σ : Env A.card n) (ρ : REnv A.card rctx) {k : Nat} (S : (Fin k → Fin A.card) → Prop) : Sat A σ (rCons S ρ) (renameRel (RelRenaming.weaken rctx k) φ) ↔ Sat A σ ρ φ

Inserting an unused relation variable leaves satisfaction unchanged.

@[simp]

theorem Complexity.DescriptiveComplexity.SOFormula.size_renameRel {V : Vocabulary} {rctx sctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (f : RelRenaming rctx sctx) : (renameRel f φ).size = φ.size

Relation renaming leaves the number of syntax nodes unchanged.

@[simp]

theorem Complexity.DescriptiveComplexity.SOFormula.isFOMatrix_renameRel {V : Vocabulary} {rctx sctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (f : RelRenaming rctx sctx) : (renameRel f φ).IsFOMatrix ↔ φ.IsFOMatrix

Relation renaming preserves and reflects being an FO matrix.

@[simp]

theorem Complexity.DescriptiveComplexity.SOFormula.isExistSO_renameRel {V : Vocabulary} {rctx sctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (f : RelRenaming rctx sctx) : (renameRel f φ).IsExistSO ↔ φ.IsExistSO

Relation renaming preserves and reflects existential SO prefix form.

@[simp]

theorem Complexity.DescriptiveComplexity.SOFormula.renameRel_id {V : Vocabulary} {rctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) : renameRel (RelRenaming.id rctx) φ = φ

Identity renaming fixes the formula exactly.

theorem Complexity.DescriptiveComplexity.SOFormula.renameRel_comp {V : Vocabulary} {rctx sctx tctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (f : RelRenaming rctx sctx) (g : RelRenaming sctx tctx) : renameRel g (renameRel f φ) = renameRel (g.comp f) φ

Successive relation renamings equal their composite.