Vocabulary maps with parameters

An FirstOrder.Language.LHom renames relation symbols and keeps their arity, so it cannot express “read this symbol at a value the formula holds in a variable”. That is exactly what a formula has to do when a second-order variable stands for a family of relations, indexed by the elements of the structure: the family is one relation of arity one more, and the index is a free variable of the formula, not an argument of the symbol.

This file is that map. A DescriptiveComplexity.ParamHom sends each relation symbol of the source vocabulary to a symbol of the target of a possibly different arity, together with a reading of each of its arguments: either one of the source symbol's own arguments, named by its index, or a parameter variable. The induced map on formulas (DescriptiveComplexity.ParamHom.onBoundedFormula) rewrites every atom that way and leaves everything else alone. Its realization (DescriptiveComplexity.ParamHom.realize_onBoundedFormula) is the expected one: reading the image in a target structure is reading the source formula in the source structure whose symbols are the target's, read at the parameters' values.

A symbol whose arguments are its own, in order, is the ordinary renaming, so a ParamHom covers an LHom as the degenerate case and a translation may mix the two – which is what its use needs, the base vocabulary passing through untouched while the block symbols pick up an index. Arguments may also be permuted or repeated; nothing here needs that, but nothing rules it out either.

The source vocabulary must be relational (as all of this library's are): a parameter is a variable, and there is no term to substitute it into.

Reading among the marked elements

The use this was written for reads the source sentence in part of the target structure – the original elements of an extended universe – while the parameters are the invented values, which are outside that part. So DescriptiveComplexity.relativizeTo cannot be applied on its own: its correctness moves the whole formula into a substructure, and an atom holding a parameter has no reading there. The second half of this file is the two steps taken together (DescriptiveComplexity.ParamHom.realize_relOnSentenceF): the quantifiers are guarded by the marker, and the source structure is read on the marked elements, at symbols that still mention the parameters.

The data

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

A map of vocabularies with parameters: each relation symbol of L₁ becomes a symbol of L₂ of a possibly different arity, each of whose arguments is either one of the symbol's own – named by its index – or a parameter variable drawn from α.

• ar {k : ℕ} : L₁.Relations k → ℕ

  The arity of the target symbol.

• sym {k : ℕ} (r : L₁.Relations k) : L₂.Relations (self.ar r)

  The target symbol.

• args {k : ℕ} (r : L₁.Relations k) : Fin (self.ar r) → Fin k ⊕ α

  What each argument of the target symbol is: an argument of the source symbol, by index, or a parameter variable.

The map on formulas

def DescriptiveComplexity.ParamHom.onBoundedFormula {L₁ L₂ : FirstOrder.Language} {α β : Type} [L₁.IsRelational] (F : ParamHom L₁ L₂ α) {n : ℕ} : L₁.BoundedFormula β n → L₂.BoundedFormula (β ⊕ α) n

The induced map on formulas: each atom is rewritten symbol and arguments, and nothing else changes.

Equations

• One or more equations did not get rendered due to their size.
• F.onBoundedFormula FirstOrder.Language.BoundedFormula.falsum = ⊥
• F.onBoundedFormula (φ.imp ψ) = (F.onBoundedFormula φ).imp (F.onBoundedFormula ψ)
• F.onBoundedFormula φ.all = (F.onBoundedFormula φ).all

def DescriptiveComplexity.ParamHom.onSentenceF {L₁ L₂ : FirstOrder.Language} {α : Type} (F : ParamHom L₁ L₂ α) [L₁.IsRelational] (φ : L₁.Sentence) : L₂.Formula α

The image of a sentence: a formula on the parameters.

Equations

• F.onSentenceF φ = FirstOrder.Language.Formula.relabel (Sum.elim (fun (e : Empty) => e.elim) id) (F.onBoundedFormula φ)

The source structure a target structure induces

@[instance_reducible]

def DescriptiveComplexity.ParamHom.struc {L₁ L₂ : FirstOrder.Language} {α : Type} (F : ParamHom L₁ L₂ α) (M : Type) [L₂.Structure M] (w : α → M) [L₁.IsRelational] : L₁.Structure M

The source structure read at the parameters: a symbol of L₁ holds of a tuple exactly when its image holds of that tuple and the parameters' values, each argument taken where the map says.

Equations

• One or more equations did not get rendered due to their size.

Realization

theorem DescriptiveComplexity.ParamHom.realize_onBoundedFormula {L₁ L₂ : FirstOrder.Language} {α β : Type} (F : ParamHom L₁ L₂ α) {M : Type} [L₂.Structure M] {w : α → M} [L₁.IsRelational] {n : ℕ} (φ : L₁.BoundedFormula β n) (v : β → M) (xs : Fin n → M) : (F.onBoundedFormula φ).Realize (Sum.elim v w) xs ↔ φ.Realize v xs

The image says of the target structure what the source said of the induced one.

theorem DescriptiveComplexity.ParamHom.realize_onFormula {L₁ L₂ : FirstOrder.Language} {α β : Type} (F : ParamHom L₁ L₂ α) {M : Type} [L₂.Structure M] {w : α → M} [L₁.IsRelational] (φ : L₁.Formula β) (v : β → M) : FirstOrder.Language.Formula.Realize (F.onBoundedFormula φ) (Sum.elim v w) ↔ φ.Realize v

The formula form of DescriptiveComplexity.ParamHom.realize_onBoundedFormula.

theorem DescriptiveComplexity.ParamHom.realize_onSentenceF {L₁ L₂ : FirstOrder.Language} {α : Type} (F : ParamHom L₁ L₂ α) {M : Type} [L₂.Structure M] {w : α → M} [L₁.IsRelational] (φ : L₁.Sentence) : (F.onSentenceF φ).Realize w ↔ M ⊨ φ

The sentence form of DescriptiveComplexity.ParamHom.realize_onBoundedFormula.

Reading among the marked elements

The parameters are values of the target structure that the marked part need not contain, so the image of a source sentence is read at guarded quantifiers rather than moved into a substructure.

@[instance_reducible]

def DescriptiveComplexity.ParamHom.strucOn {L₁ L₂ : FirstOrder.Language} {α : Type} [L₁.IsRelational] (F : ParamHom L₁ L₂ α) {M : Type} [L₂.Structure M] {A : Type} (e : A → M) (w : α → M) : L₁.Structure A

The source structure on the marked part: a symbol holds of a tuple of marked elements exactly when its image holds of the parameters' values followed by that tuple.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.ParamHom.realize_relOnBoundedFormula {L₁ L₂ : FirstOrder.Language} {α β : Type} [L₁.IsRelational] (F : ParamHom L₁ L₂ α) (R : L₂.Relations 1) {M : Type} [L₂.Structure M] {w : α → M} {A : Type} {e : A → M} (hinj : Function.Injective e) (hR : ∀ (x : M), FirstOrder.Language.Structure.RelMap R ![x] ↔ ∃ (a : A), e a = x) {n : ℕ} (φ : L₁.BoundedFormula β n) (v : β → A) (xs : Fin n → A) : ((relativizeTo R (F.onBoundedFormula φ)).Realize (Sum.elim (fun (b : β) => e (v b)) w) fun (i : Fin n) => e (xs i)) ↔ φ.Realize v xs

The image, relativized, says of the marked part what the source said: every quantifier is guarded by the marker, and every symbol is read through the parameters.

def DescriptiveComplexity.ParamHom.relOnSentenceF {L₁ L₂ : FirstOrder.Language} {α : Type} [L₁.IsRelational] (F : ParamHom L₁ L₂ α) (R : L₂.Relations 1) (φ : L₁.Sentence) : L₂.Formula α

The image of a sentence, read among the marked elements: a formula on the parameters.

Equations

• F.relOnSentenceF R φ = FirstOrder.Language.Formula.relabel (Sum.elim (fun (e : Empty) => e.elim) id) (DescriptiveComplexity.relativizeTo R (F.onBoundedFormula φ))

theorem DescriptiveComplexity.ParamHom.realize_relOnSentenceF {L₁ L₂ : FirstOrder.Language} {α : Type} [L₁.IsRelational] (F : ParamHom L₁ L₂ α) (R : L₂.Relations 1) {M : Type} [L₂.Structure M] {w : α → M} {A : Type} {e : A → M} (hinj : Function.Injective e) (hR : ∀ (x : M), FirstOrder.Language.Structure.RelMap R ![x] ↔ ∃ (a : A), e a = x) (φ : L₁.Sentence) : (F.relOnSentenceF R φ).Realize w ↔ A ⊨ φ

The sentence form of DescriptiveComplexity.ParamHom.realize_relOnBoundedFormula.