Which invented values are points, and what the expanded relations say of them

An invented value stands for a tagged assignment of the expansion's block: the assignment is what the guessed meaning relations give it (DescriptiveComplexity.SecondOrderNewRead), and the tag is carried the same way, by one nullary variable of the block per tag – so a unary symbol on the extended universe. Neither is a point of the expanded universe on its own: a point carries exactly one tag, and its assignment satisfies that tag's domain sentence. Both are first-order statements about the value, and this file writes them.

• DescriptiveComplexity.isPointF – “this value is a point”: exactly one tag symbol holds of it, and the domain sentence of that tag, read through the meanings among the original elements, holds.
• DescriptiveComplexity.pointRelF – “this relation of the expanded vocabulary holds of these values”: one disjunct per tuple of tags, guarded by the tag symbols of the values, whose body is the defining sentence at that tuple, read the same way. The tags are guessed here, where everywhere else in the library they are chosen when the formula is built, so a static tuple will not do; there are finitely many, so the disjunction is finite.

Both are written over an abstract target vocabulary (DescriptiveComplexity.PointSyms names the symbols and nothing else), and both are formulas with free variables of an arbitrary type, so that the assembly can plug them under whatever quantifiers it needs.

The symbols

structure DescriptiveComplexity.PointSyms (L : FirstOrder.Language) (X : ExpExpansion L) (Lt : FirstOrder.Language) : Type

The symbols the point formulas use in the target vocabulary: those the translation through the meanings needs, one unary symbol per tag, and the marker of the original elements.

• read : ReadSyms L X.B Lt

  The symbols the defining sentences are read at.

• tag : X.Tag → Lt.Relations 1

  “this value carries the tag t”.

• old : Lt.Relations 1

  The marker of the original elements.

The formulas

def DescriptiveComplexity.tagF {L Lt : FirstOrder.Language} {X : ExpExpansion L} (P : PointSyms L X Lt) {α : Type} (t : X.Tag) (v : α) : Lt.Formula α

The atom “the value held by v carries the tag t”.

Equations

• DescriptiveComplexity.tagF P t v = (P.tag t).formula fun (x : Fin 1) => FirstOrder.Language.var v

noncomputable def DescriptiveComplexity.isPointF {L Lt : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} (P : PointSyms L X Lt) {α : Type} (v : α) : Lt.Formula α

“The value held by v is a point of the expanded universe”: it carries exactly one tag, and the domain sentence of that tag holds of the assignment it means.

Equations

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

noncomputable def DescriptiveComplexity.pointRelF {L Lt : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} (P : PointSyms L X Lt) {α : Type} {k : ℕ} (r : X.E.Relations k) (vs : Fin k → α) : Lt.Formula α

“The relation r of the expanded vocabulary holds of the values held by vs”: one disjunct per tuple of tags, guarded by the tag atoms of those values, whose body is the defining sentence at that tuple, read through the meanings among the original elements.

Equations

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

What they say

structure DescriptiveComplexity.PointOn {L Lt : FirstOrder.Language} {X : ExpExpansion L} {M A : Type} [Lt.Structure M] [L.Structure A] [LinearOrder A] (P : PointSyms L X Lt) (e : A → M) (means : M → X.B.Assignment A) (tags : M → X.Tag → Prop) : Prop

The readings the point formulas promise, beyond those of DescriptiveComplexity.ReadOn: the tag symbols are the tags a value carries, and the marker marks the original elements.

• read : ReadOn P.read e means

  The translation reads what it should.

• old (x : M) : FirstOrder.Language.Structure.RelMap P.old ![x] ↔ ∃ (a : A), e a = x

  The original elements are exactly the marked ones.

• tag (v : M) (t : X.Tag) : (FirstOrder.Language.Structure.RelMap (P.tag t) fun (x : Fin 1) => v) ↔ tags v t

  The tag symbols are the tags a value carries.

theorem DescriptiveComplexity.realize_tagF {L Lt : FirstOrder.Language} {X : ExpExpansion L} {P : PointSyms L X Lt} {α M A : Type} [Lt.Structure M] [L.Structure A] [LinearOrder A] {e : A → M} {means : M → X.B.Assignment A} {tags : M → X.Tag → Prop} (h : PointOn P e means tags) (t : X.Tag) (v : α) (w : α → M) : (tagF P t v).Realize w ↔ tags (w v) t

theorem DescriptiveComplexity.realize_isPointF {L Lt : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {P : PointSyms L X Lt} {α M A : Type} [Lt.Structure M] [L.Structure A] [LinearOrder A] {e : A → M} {means : M → X.B.Assignment A} {tags : M → X.Tag → Prop} (hinj : Function.Injective e) (h : PointOn P e means tags) (v : α) (w : α → M) : (isPointF P v).Realize w ↔ ∃ (t : X.Tag), tags (w v) t ∧ (∀ (t' : X.Tag), tags (w v) t' → t' = t) ∧ ExpExpansion.DomHolds (t, means (w v))

DescriptiveComplexity.isPointF says that the value is a point: it carries one tag and no other, and its assignment satisfies that tag's domain sentence.

theorem DescriptiveComplexity.realize_pointRelF {L Lt : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {P : PointSyms L X Lt} {α M A : Type} [Lt.Structure M] [L.Structure A] [LinearOrder A] {e : A → M} {means : M → X.B.Assignment A} {tags : M → X.Tag → Prop} (hinj : Function.Injective e) (h : PointOn P e means tags) {k : ℕ} (r : X.E.Relations k) (vs : Fin k → α) (w : α → M) : (pointRelF P r vs).Realize w ↔ ∃ (τ : Fin k → X.Tag), (∀ (j : Fin k), tags (w (vs j)) (τ j)) ∧ A ⊨ X.relSentence r τ

DescriptiveComplexity.pointRelF says that the relation holds, provided the values carry the tags: some tuple of tags is the one the values carry, and the defining sentence at that tuple holds of the assignments they mean.