Interpreting a vocabulary by formulas on a definable part

A first-order interpretation of this library (DescriptiveComplexity.FOInterpretation) builds its universe out of tagged d-tuples, which is what a reduction needs and what makes composition work. A translation that only has to read one element per point pays for that packaging without using it: the tags are a single one, the dimension is one, and every statement carries a Unit × (Fin 1 → A) that has to be unwound again.

This file is that translation, stated directly. A DescriptiveComplexity.FormulaSubst gives one formula per relation symbol of the source vocabulary, on as many free variables as the symbol has arguments; DescriptiveComplexity.FormulaSubst.substTo rewrites a source formula by substituting them and guarding every quantifier by a domain formula, and DescriptiveComplexity.FormulaSubst.realize_substTo says what it is worth: the image, read in the target structure at points of the definable part, says what the source formula says of the structure those formulas define on that part.

The definable part is not given as a subtype but as an arbitrary type with an injection into the target whose range the domain formula defines. That is what lets a caller take the part to be the object it already has – the universe of an expansion, say – instead of a subtype it would then have to transport across.

The data

structure DescriptiveComplexity.FormulaSubst (L₁ L₂ : FirstOrder.Language) : Type

An interpretation of L₁ by L₂-formulas: one formula per relation symbol, on as many free variables as the symbol has arguments.

• rel {n : ℕ} : L₁.Relations n → L₂.Formula (Fin n)

  The formula defining a relation symbol.

def DescriptiveComplexity.FormulaSubst.domGuard {L₂ : FirstOrder.Language} {β : Type} (D : L₂.Formula (Fin 1)) (n : ℕ) : L₂.BoundedFormula β (n + 1)

The guard “the last bound variable is in the definable part”.

Equations

• DescriptiveComplexity.FormulaSubst.domGuard D n = FirstOrder.Language.BoundedFormula.relabel (fun (x : Fin 1) => Sum.inr (Fin.last n)) D

def DescriptiveComplexity.FormulaSubst.substTo {L₁ L₂ : FirstOrder.Language} {β : Type} (F : FormulaSubst L₁ L₂) (D : L₂.Formula (Fin 1)) [L₁.IsRelational] {n : ℕ} : L₁.BoundedFormula β n → L₂.BoundedFormula β n

The translation: every atom is replaced by the formula defining its symbol, and every quantifier is guarded by the domain formula.

Equations

• F.substTo D FirstOrder.Language.BoundedFormula.falsum = ⊥
• F.substTo D (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = (FirstOrder.Language.var t₁.varOf).bdEqual (FirstOrder.Language.var t₂.varOf)
• F.substTo D (FirstOrder.Language.BoundedFormula.rel r ts) = FirstOrder.Language.BoundedFormula.relabel (fun (i : Fin l) => (ts i).varOf) (F.rel r)
• F.substTo D (φ.imp ψ) = (F.substTo D φ).imp (F.substTo D ψ)
• F.substTo D φ.all = ((DescriptiveComplexity.FormulaSubst.domGuard D x✝).imp (F.substTo D φ)).all

def DescriptiveComplexity.FormulaSubst.substSentence {L₁ L₂ : FirstOrder.Language} (F : FormulaSubst L₁ L₂) (D : L₂.Formula (Fin 1)) [L₁.IsRelational] (φ : L₁.Sentence) : L₂.Sentence

The image of a sentence.

Equations

• F.substSentence D φ = F.substTo D φ

The structure the formulas define

@[instance_reducible]

def DescriptiveComplexity.FormulaSubst.strucOn {L₁ L₂ : FirstOrder.Language} (F : FormulaSubst L₁ L₂) {M Pt : Type} [L₂.Structure M] [L₁.IsRelational] (e : Pt → M) : L₁.Structure Pt

The structure the formulas define on the definable part: a symbol holds of a tuple exactly when its formula holds of the elements that tuple names.

Equations

• F.strucOn e = { funMap := fun {n : ℕ} (f : L₁.Functions n) => isEmptyElim f, RelMap := fun {x : ℕ} (r : L₁.Relations x) (ts : Fin x → Pt) => (F.rel r).Realize fun (i : Fin x) => e (ts i) }

Realization

theorem DescriptiveComplexity.FormulaSubst.realize_domGuard {L₂ : FirstOrder.Language} {β : Type} {D : L₂.Formula (Fin 1)} {M : Type} [L₂.Structure M] {n : ℕ} (v : β → M) (xs : Fin (n + 1) → M) : (domGuard D n).Realize v xs ↔ D.Realize ![xs (Fin.last n)]

theorem DescriptiveComplexity.FormulaSubst.realize_substTo {L₁ L₂ : FirstOrder.Language} {β : Type} {F : FormulaSubst L₁ L₂} {D : L₂.Formula (Fin 1)} {M Pt : Type} [L₂.Structure M] {e : Pt → M} [L₁.IsRelational] (hinj : Function.Injective e) (hD : ∀ (x : M), D.Realize ![x] ↔ ∃ (p : Pt), e p = x) {n : ℕ} (φ : L₁.BoundedFormula β n) (v : β → Pt) (xs : Fin n → Pt) : ((F.substTo D φ).Realize (fun (b : β) => e (v b)) fun (i : Fin n) => e (xs i)) ↔ φ.Realize v xs

The image says of the target structure what the source says of the definable part: quantifiers range over the part, and atoms hold as their formulas say.

theorem DescriptiveComplexity.FormulaSubst.realize_substSentence {L₁ L₂ : FirstOrder.Language} {F : FormulaSubst L₁ L₂} {D : L₂.Formula (Fin 1)} {M Pt : Type} [L₂.Structure M] {e : Pt → M} [L₁.IsRelational] (hinj : Function.Injective e) (hD : ∀ (x : M), D.Realize ![x] ↔ ∃ (p : Pt), e p = x) (φ : L₁.Sentence) : M ⊨ F.substSentence D φ ↔ Pt ⊨ φ

The sentence form of DescriptiveComplexity.FormulaSubst.realize_substTo.