Exponential expansions: reading a structure over its second-order objects

The one construction the exponential classes are built from. An exponential expansion of L-structures maps a finite ordered L-structure A to a structure over another vocabulary E whose universe is a definable set of tagged assignments of a second-order block. A block with a variable of arity a has 2^(n^a) assignments on a universe of size n, so the expanded universe is exponentially larger than A, and a resource bound read there is one exponential higher than the same bound read on A.

The data (DescriptiveComplexity.ExpExpansion) mirrors DescriptiveComplexity.RelFOInterpretation one level up:

• a finite Tag type and a block B, whose pairs (t, ρ) are the candidate points – the analogue of the tagged tuples Tag × A^dim;
• a domain sentence dom t per tag, over the ordered base vocabulary expanded by one copy of the block, cutting the universe down to a definable set (DescriptiveComplexity.ExpExpansion.Map, a subtype);
• a defining sentence relSentence r τ per relation symbol of E and per tuple of tags, over the ordered base vocabulary expanded by as many copies of the block as the symbol has arguments (DescriptiveComplexity.SOBlock.replicate).

Three design points, each paying for itself downstream.

The tags are part of the data, not a separate dimension. A d-tuple of points is a tag tuple together with an assignment of the replicated block, so composing an expansion with a first-order interpretation gives an expansion again, exactly rather than up to an embedding (DescriptiveComplexity.Exponential.Pull). Without the tag factor every hardness discharge would owe a relativization argument.

There is a domain sentence. Hardness in this library is cofinal hardness and DescriptiveComplexity.cofinalHard_iff hands out relativized reductions ≤ʳᶠᵒ[≤], whose target universe is already a subtype; an expansion composed with one is again an expansion only if expansions may carve out their universe too. dom_nonempty is then the same obligation, for the same reason, as in DescriptiveComplexity.RelOrderedFOReduction.

The sentences see the order, the problem does not. This is the discipline of DescriptiveComplexity.SOTCSpec: the capture theorems this development builds on are the ordered ones, while order-invariance is what makes the notion a DescriptiveComplexity.DecisionProblem.

The data

structure DescriptiveComplexity.ExpExpansion (L : FirstOrder.Language) : Type 1

An exponential expansion of L-structures into E-structures: the universe is a definable set of tagged assignments of the block B, and each relation symbol of E is defined, at each tuple of tags, by a first-order sentence over the ordered base vocabulary expanded by one copy of the block per argument.

• Tag : Type

  The tags: finitely many copies of the space of block assignments.

• tagFinite : Finite self.Tag

  Tags are finite, so that finite structures expand to finite structures.

• B : SOBlock

  The block whose assignments are the points of the expanded universe.

• E : FirstOrder.Language

  The vocabulary of the expanded structure.

• eRelational : self.E.IsRelational

  The expanded vocabulary is relational, as every vocabulary of this library.

• dom : self.Tag → ((L.sum FirstOrder.Language.order).sum self.B.lang).Sentence

  The domain sentence of each tag: a tagged assignment (t, ρ) is a point of the expanded universe iff dom t holds of ρ.

• relSentence {n : ℕ} : self.E.Relations n → (Fin n → self.Tag) → ((L.sum FirstOrder.Language.order).sum (self.B.replicate n).lang).Sentence

  The defining sentence of each relation symbol at each tuple of tags, over as many copies of the block as the symbol has arguments.

• dom_nonempty (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : ∃ (t : self.Tag) (ρ : self.B.Assignment A), A ⊨ self.dom t

  The definable domain is inhabited, so that nonempty structures expand to nonempty structures.

The expanded universe

@[reducible, inline]

abbrev DescriptiveComplexity.ExpExpansion.Point {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) : Type

A candidate point of the expanded universe: a tagged assignment of the block. An abbrev, so that the pair structure stays visible to rw and to instance search – only DescriptiveComplexity.ExpExpansion.Map needs to be opaque, to carry the expanded structure.

Equations

• X.Point A = (X.Tag × X.B.Assignment A)

def DescriptiveComplexity.ExpExpansion.DomHolds {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (p : X.Point A) : Prop

The domain condition on a candidate point: its tag's domain sentence holds of its assignment.

Equations

• DescriptiveComplexity.ExpExpansion.DomHolds p = A ⊨ X.dom p.1

def DescriptiveComplexity.ExpExpansion.Map {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [L.Structure A] [LinearOrder A] : Type

The expanded universe: the tagged block assignments satisfying their tag's domain sentence.

Equations

• X.Map A = { p : X.Point A // DescriptiveComplexity.ExpExpansion.DomHolds p }

def DescriptiveComplexity.ExpExpansion.pt {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (t : X.Tag) (ρ : X.B.Assignment A) (h : DomHolds (t, ρ)) : X.Map A

The point of the expanded universe carried by a tag and an assignment satisfying the domain sentence.

Equations

• DescriptiveComplexity.ExpExpansion.pt t ρ h = ⟨(t, ρ), h⟩

@[simp]

theorem DescriptiveComplexity.ExpExpansion.pt_tag {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (t : X.Tag) (ρ : X.B.Assignment A) (h : DomHolds (t, ρ)) : (↑(pt t ρ h)).1 = t

@[simp]

theorem DescriptiveComplexity.ExpExpansion.pt_assign {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (t : X.Tag) (ρ : X.B.Assignment A) (h : DomHolds (t, ρ)) : (↑(pt t ρ h)).2 = ρ

theorem DescriptiveComplexity.ExpExpansion.map_ext {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {x y : X.Map A} (h₁ : (↑x).1 = (↑y).1) (h₂ : (↑x).2 = (↑y).2) : x = y

Two points of the expanded universe are equal as soon as their tags and their assignments are: the domain condition is a proof.

@[instance_reducible]

instance DescriptiveComplexity.ExpExpansion.mapStructure {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [L.Structure A] [LinearOrder A] : X.E.Structure (X.Map A)

The expanded structure: an n-ary symbol holds of n points iff its defining sentence, at their tags, holds in the base structure with the n copies of the block interpreted by their assignments.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.relMap_map {L : FirstOrder.Language} (X : ExpExpansion L) {A : Type} [L.Structure A] [LinearOrder A] {n : ℕ} (r : X.E.Relations n) (xs : Fin n → X.Map A) : FirstOrder.Language.Structure.RelMap r xs ↔ A ⊨ X.relSentence r fun (i : Fin n) => (↑(xs i)).1

Finiteness and nonemptiness

instance DescriptiveComplexity.ExpExpansion.mapFinite {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] : Finite (X.Map A)

instance DescriptiveComplexity.ExpExpansion.mapNonempty {L : FirstOrder.Language} (X : ExpExpansion L) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Nonempty (X.Map A)