Relationalizing an ∃SO[new] definition

Hardness proofs whose target reads the source structure through the defining formulas of an interpretation cope with function symbols for free; one whose target has to name what a function does – as the encoded sentence of DescriptiveComplexity.FINSAT must, since it carries its own quantifiers – does not. This file removes function symbols from the source once and for all:

every ∃SO[new]-definable problem admits a first-order reduction to an ∃SO[new]-definable problem over a relational vocabulary (DescriptiveComplexity.exists_relational_of_sigmaSONewDefinable).

Composed with a hardness result proved for relational sources, it gives the hardness result for all of them, which is what DescriptiveComplexity.CofinalHard asks for.

The two obstacles, and how they are removed

The junk value. An extended universe A ⊕ Fin m interprets a function symbol on a tuple with an invented argument by applying f^A to DescriptiveComplexity.oldPart, which sends every invented value to Classical.arbitrary A. That element depends on the carrier type only, so no formula can name it, and a translation that has to mention it is stuck. The way out is that the definability equivalence quantifies over every L-structure instance on the carrier: transporting the structure along a transposition gives a second instance, isomorphic to the first, whose junk element is whatever we like. Hence DescriptiveComplexity.sigmaSONewDefinable_junk: an ∃SO[new] definition may be read with any junk element.

The terms. The relational vocabulary is the atomic diagram language DescriptiveComplexity.atomLang: one relation symbol of arity n per atomic formula of L in n variables. An L-structure carries one canonically, and the map is a one-dimensional first-order interpretation, since “this atomic formula holds of this tuple” is a first-order property of the tuple. The kernel is then translated atom by atom, in place: an atom at context length n becomes an existential block of n + 1 variables – the coerced arguments, and the junk element the block guesses – followed by the corresponding symbol of the atomic diagram language. Nothing else in the kernel changes, so no de Bruijn index is ever shifted.

An extended universe with a chosen junk value

def DescriptiveComplexity.oldPartAt (A : Type) (m : ℕ) (z : A) : A ⊕ Fin m → A

The original-element part of an extended universe, reading an invented value as a given element rather than Classical.arbitrary.

Equations

• DescriptiveComplexity.oldPartAt A m z = Sum.elim id fun (x : Fin m) => z

@[instance_reducible]

def DescriptiveComplexity.extBaseAt (L : FirstOrder.Language) (A : Type) [L.Structure A] (m : ℕ) (z : A) : L.Structure (A ⊕ Fin m)

The base structure carried by an extended universe with a chosen junk value.

Equations

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

@[instance_reducible]

def DescriptiveComplexity.extStructureAt (L : FirstOrder.Language) (A : Type) [L.Structure A] (m : ℕ) (z : A) : (newLang L).Structure (A ⊕ Fin m)

The extended structure with a chosen junk value.

Equations

• DescriptiveComplexity.extStructureAt L A m z = L.sumStructure FirstOrder.Language.oldMark (A ⊕ Fin m)

theorem DescriptiveComplexity.extStructureAt_arbitrary (L : FirstOrder.Language) (A : Type) [L.Structure A] [Nonempty A] (m : ℕ) : extStructureAt L A m (Classical.arbitrary A) = extStructure L A m

At the arbitrary element it is the extended structure of DescriptiveComplexity.extStructure.

The three defining equations of the extended structure, stated with the instance explicit: two structures on one carrier are in play below, so no occurrence of funMap or RelMap may be left to instance synthesis.

theorem DescriptiveComplexity.funMap_extAt {L : FirstOrder.Language} {A : Type} {m : ℕ} (z : A) (inst : L.Structure A) {n : ℕ} (g : L.Functions n) (x : Fin n → A ⊕ Fin m) : FirstOrder.Language.Structure.funMap (Sum.inl g) x = Sum.inl (FirstOrder.Language.Structure.funMap g fun (i : Fin n) => oldPartAt A m z (x i))

theorem DescriptiveComplexity.relMap_extAt {L : FirstOrder.Language} {A : Type} {m : ℕ} (z : A) (inst : L.Structure A) {n : ℕ} (s : L.Relations n) (x : Fin n → A ⊕ Fin m) : FirstOrder.Language.Structure.RelMap (Sum.inl s) x ↔ ∃ (y : Fin n → A), (∀ (i : Fin n), x i = Sum.inl (y i)) ∧ FirstOrder.Language.Structure.RelMap s y

theorem DescriptiveComplexity.relMap_extAt_old {L : FirstOrder.Language} {A : Type} {m : ℕ} (z : A) (inst : L.Structure A) (x : Fin 1 → A ⊕ Fin m) : FirstOrder.Language.Structure.RelMap (Sum.inr FirstOrder.Language.oldSym) x ↔ IsOld (x 0)

@[instance_reducible]

def DescriptiveComplexity.transportStruct {L : FirstOrder.Language} {A : Type} (π : A ≃ A) (inst : L.Structure A) : L.Structure A

Transporting a structure along a permutation of its carrier: a second structure on the same type, isomorphic to the first.

Equations

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

theorem DescriptiveComplexity.funMap_transport {L : FirstOrder.Language} {A : Type} (π : A ≃ A) (inst : L.Structure A) {n : ℕ} (g : L.Functions n) (x : Fin n → A) : FirstOrder.Language.Structure.funMap g x = π.symm (FirstOrder.Language.Structure.funMap g fun (i : Fin n) => π (x i))

theorem DescriptiveComplexity.relMap_transport {L : FirstOrder.Language} {A : Type} (π : A ≃ A) (inst : L.Structure A) {n : ℕ} (s : L.Relations n) (x : Fin n → A) : FirstOrder.Language.Structure.RelMap s x ↔ FirstOrder.Language.Structure.RelMap s fun (i : Fin n) => π (x i)

def DescriptiveComplexity.transportEquiv {L : FirstOrder.Language} {A : Type} (π : A ≃ A) (inst : L.Structure A) : L.Equiv A A

The permutation is that isomorphism.

Equations

• DescriptiveComplexity.transportEquiv π inst = { toEquiv := π, map_fun' := ⋯, map_rel' := ⋯ }

def DescriptiveComplexity.extIsoTransport {L : FirstOrder.Language} {A : Type} (π : A ≃ A) (inst : L.Structure A) (m : ℕ) (z : A) : (newLang L).Equiv (A ⊕ Fin m) (A ⊕ Fin m)

The junk value moves with the permutation: the extended structure of the transported instance, with junk z, is the extended structure of the original instance with junk π z. This is what lets a definition be read at any junk value at all.

Equations

• DescriptiveComplexity.extIsoTransport π inst m z = { toEquiv := π.sumCongr (Equiv.refl (Fin m)), map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.sigmaSONewDefinable_junk {L : FirstOrder.Language} {P : DecisionProblem L} (h : SigmaSONewDefinable P) : ∃ (B : SOBlock) (φ : (soLang (newLang L) [B]).Sentence), ∀ (A : Type) [_inst : L.Structure A] [Finite A] [Nonempty A] (z : A), P.Holds A ↔ ∃ (m : ℕ), SORealize (newLang L) (A ⊕ Fin m) [B] φ true

An ∃SO[new] definition may be read with any junk value: the extended universe interpreting a function symbol on an invented argument through the given element z rather than through Classical.arbitrary.

This is what makes the undefinability of Classical.arbitrary A harmless: the junk element is not a feature of the problem, only of one presentation of the extended universe.

The atomic diagram language

The relational vocabulary the source is moved to: one relation symbol of arity n per atomic formula of L in n variables. Every structure carries one canonically, and “this atomic formula holds of this tuple” is a first-order property of the tuple, so the map is a one-dimensional interpretation.

def DescriptiveComplexity.atomLang (L : FirstOrder.Language) : FirstOrder.Language

The atomic diagram language: a relation symbol of arity n for each atom r(t₁, …, t_l) and each equality t₁ = t₂ of L in n variables.

Equations

• DescriptiveComplexity.atomLang L = { Functions := fun (x : ℕ) => Empty, Relations := fun (n : ℕ) => (l : ℕ) × L.Relations l × (Fin l → L.Term (Fin n)) ⊕ L.Term (Fin n) × L.Term (Fin n) }

instance DescriptiveComplexity.atomLang_isRelational {L : FirstOrder.Language} : (atomLang L).IsRelational

@[instance_reducible]

def DescriptiveComplexity.atomStructure (L : FirstOrder.Language) (A : Type) [L.Structure A] : (atomLang L).Structure A

The atomic diagram of a structure: each symbol holds of the tuples satisfying the atomic formula it names.

Equations

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

theorem DescriptiveComplexity.relMap_atomStructure_rel {L : FirstOrder.Language} {A : Type} [L.Structure A] {n l : ℕ} (r : L.Relations l) (ts : Fin l → L.Term (Fin n)) (x : Fin n → A) : FirstOrder.Language.Structure.RelMap (Sum.inl ⟨l, (r, ts)⟩) x ↔ FirstOrder.Language.Structure.RelMap r fun (j : Fin l) => FirstOrder.Language.Term.realize x (ts j)

theorem DescriptiveComplexity.relMap_atomStructure_eq {L : FirstOrder.Language} {A : Type} [L.Structure A] {n : ℕ} (t₁ t₂ : L.Term (Fin n)) (x : Fin n → A) : FirstOrder.Language.Structure.RelMap (Sum.inr (t₁, t₂)) x ↔ FirstOrder.Language.Term.realize x t₁ = FirstOrder.Language.Term.realize x t₂

def DescriptiveComplexity.atomFml {L : FirstOrder.Language} {n : ℕ} (R : (atomLang L).Relations n) : L.Formula (Fin n × Fin 1)

The defining formula of a symbol of the atomic diagram language: the atomic formula it names, read at the one-dimensional tuple.

Equations

• DescriptiveComplexity.atomFml (Sum.inl ⟨fst, (r, ts)⟩) = r.formula fun (j : Fin fst) => FirstOrder.Language.Term.relabel (fun (i : Fin n) => (i, 0)) (ts j)
• DescriptiveComplexity.atomFml (Sum.inr (t₁, t₂)) = (FirstOrder.Language.Term.relabel (fun (i : Fin n) => (i, 0)) t₁).equal (FirstOrder.Language.Term.relabel (fun (i : Fin n) => (i, 0)) t₂)

def DescriptiveComplexity.atomInterp (L : FirstOrder.Language) : FOInterpretation L (atomLang L) Unit 1

The atomic diagram, as a one-dimensional first-order interpretation.

Equations

• DescriptiveComplexity.atomInterp L = { relFormula := fun {n : ℕ} (R : (DescriptiveComplexity.atomLang L).Relations n) (x : Fin n → Unit) => DescriptiveComplexity.atomFml R }

theorem DescriptiveComplexity.realize_atomFml {L : FirstOrder.Language} {n : ℕ} (R : (atomLang L).Relations n) {A : Type} [L.Structure A] (v : Fin n × Fin 1 → A) : (atomFml R).Realize v ↔ FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => v (i, 0)

What the defining formula of an atomic-diagram symbol says: the symbol holds of the tuple.

def DescriptiveComplexity.atomMapEquiv {L : FirstOrder.Language} (A : Type) [L.Structure A] : (atomLang L).Equiv ((atomInterp L).Map A) A

The interpreted structure is the atomic diagram, through the equivalence of a one-dimensional single-tag universe with its own carrier.

Equations

• DescriptiveComplexity.atomMapEquiv A = { toEquiv := (DescriptiveComplexity.atomInterp L).mapEquivSelf A, map_fun' := ⋯, map_rel' := ⋯ }

def DescriptiveComplexity.atomReduction {L : FirstOrder.Language} (P : DecisionProblem L) (Q : DecisionProblem (atomLang L)) (h : ∀ (A : Type) [inst : L.Structure A] [Finite A] [Nonempty A], P.Holds A ↔ Q.Holds A) : FOReduction P Q

The relationalizing reduction: any problem reduces, first-order, to a problem over the atomic diagram language that agrees with it on the atomic diagrams of finite structures.

Equations

• DescriptiveComplexity.atomReduction P Q h = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.atomInterp L, correct := ⋯ }

Blocks of existential quantifiers

The translation of an atom introduces a fixed number of fresh variables at the end of the context, which is what makes it a purely local rewriting: nothing already in the kernel is shifted.

def DescriptiveComplexity.exs {L : FirstOrder.Language} {α : Type} {n : ℕ} (k : ℕ) : L.BoundedFormula α (n + k) → L.BoundedFormula α n

A block of k existential quantifiers.

Equations

• DescriptiveComplexity.exs 0 ψ = ψ
• DescriptiveComplexity.exs n.succ ψ = DescriptiveComplexity.exs n ψ.ex

theorem DescriptiveComplexity.realize_exs {L : FirstOrder.Language} {α M : Type} [L.Structure M] {n : ℕ} (k : ℕ) (ψ : L.BoundedFormula α (n + k)) (v : α → M) (xs : Fin n → M) : (exs k ψ).Realize v xs ↔ ∃ (ys : Fin (n + k) → M), (∀ (i : Fin n), ys (Fin.castAdd k i) = xs i) ∧ ψ.Realize v ys

What a block of existential quantifiers says: the context is extended by k values, the ones already there being kept.

The shadow of a term

The translation replaces a term by the value it takes; the point of the construction is that this value is computed in the instance, on the tuple the junk convention leaves behind.

@[reducible, inline]

abbrev DescriptiveComplexity.srcLang (L : FirstOrder.Language) (B : SOBlock) : FirstOrder.Language

The kernel language of an ∃SO[new] definition.

Equations

• DescriptiveComplexity.srcLang L B = (DescriptiveComplexity.newLang L).sum B.lang

def DescriptiveComplexity.jBlock (B : SOBlock) : SOBlock

The block, extended by the unary relation variable naming the junk element.

Equations

• DescriptiveComplexity.jBlock B = { ι := B.ι ⊕ Unit, ιFinite := ⋯, arity := Sum.elim B.arity fun (x : Unit) => 1 }

@[reducible, inline]

abbrev DescriptiveComplexity.tgtLang (L : FirstOrder.Language) (B : SOBlock) : FirstOrder.Language

The kernel language the translation lands in: the atomic diagram language, extended and expanded by the enlarged block.

Equations

• DescriptiveComplexity.tgtLang L B = (DescriptiveComplexity.newLang (DescriptiveComplexity.atomLang L)).sum (DescriptiveComplexity.jBlock B).lang

def DescriptiveComplexity.termDown {L : FirstOrder.Language} {B : SOBlock} {α : Type} : (srcLang L B).Term α → L.Term α

The L-term a term of the kernel language shadows: neither the marker nor the vocabulary of a block has function symbols, so every function application is one of L.

Equations

• DescriptiveComplexity.termDown (FirstOrder.Language.var x_1) = FirstOrder.Language.var x_1
• DescriptiveComplexity.termDown (FirstOrder.Language.func (Sum.inl (Sum.inl g)) ts) = FirstOrder.Language.func g fun (j : Fin l) => DescriptiveComplexity.termDown (ts j)
• DescriptiveComplexity.termDown (FirstOrder.Language.func (Sum.inl (Sum.inr e)) _ts) = Empty.elim e
• DescriptiveComplexity.termDown (FirstOrder.Language.func (Sum.inr e) _ts) = Empty.elim e

def DescriptiveComplexity.termShadow {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} (t : (srcLang L B).Term (Empty ⊕ Fin n)) : L.Term (Fin n)

The shadow of a term of the kernel, as an L-term in the context variables: the index of a symbol of the atomic diagram language.

Equations

• DescriptiveComplexity.termShadow t = FirstOrder.Language.Term.relabel (Sum.elim Empty.elim id) (DescriptiveComplexity.termDown t)

theorem DescriptiveComplexity.realize_termShadow {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] {n : ℕ} (t : (srcLang L B).Term (Empty ⊕ Fin n)) (v : Fin n → A) : FirstOrder.Language.Term.realize v (termShadow t) = FirstOrder.Language.Term.realize (Sum.elim (fun (a : Empty) => isEmptyElim a) v) (termDown t)

@[instance_reducible]

noncomputable def DescriptiveComplexity.srcStruct {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) : (srcLang L B).Structure (A ⊕ Fin m)

The structure a certificate puts on an extended universe: the instance with its junk convention, expanded by the assignment of the block.

Equations

• DescriptiveComplexity.srcStruct z μ = (DescriptiveComplexity.newLang L).sumStructure B.lang (A ⊕ Fin m)

theorem DescriptiveComplexity.oldPartAt_realize {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {α : Type} (t : (srcLang L B).Term α) (w : α → A ⊕ Fin m) : oldPartAt A m z (FirstOrder.Language.Term.realize w t) = FirstOrder.Language.Term.realize (fun (i : α) => oldPartAt A m z (w i)) (termDown t)

The value of a term, up to the junk convention: forgetting which invented values a term's value came from is computing its shadow in the instance, on the context with the same forgetting applied.

theorem DescriptiveComplexity.realize_func_eq_inl {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {α : Type} {l : ℕ} (g : L.Functions l) (ts : Fin l → (srcLang L B).Term α) (w : α → A ⊕ Fin m) : FirstOrder.Language.Term.realize w (FirstOrder.Language.func (Sum.inl (Sum.inl g)) ts) = Sum.inl (FirstOrder.Language.Term.realize (fun (i : α) => oldPartAt A m z (w i)) (termDown (FirstOrder.Language.func (Sum.inl (Sum.inl g)) ts)))

The value of a term that is a function application is an original element: only a variable can take an invented value.

Finite conjunctions

def DescriptiveComplexity.finConj {L : FirstOrder.Language} {α : Type} {N p : ℕ} : (Fin p → L.BoundedFormula α N) → L.BoundedFormula α N

The conjunction of finitely many bounded formulas.

Equations

• DescriptiveComplexity.finConj x_2 = ⊤
• DescriptiveComplexity.finConj f = f 0 ⊓ DescriptiveComplexity.finConj fun (j : Fin n) => f j.succ

theorem DescriptiveComplexity.realize_finConj {L : FirstOrder.Language} {α M : Type} [L.Structure M] {N p : ℕ} (f : Fin p → L.BoundedFormula α N) (v : α → M) (xs : Fin N → M) : (finConj f).Realize v xs ↔ ∀ (j : Fin p), (f j).Realize v xs

The translation

Each atom is rewritten in place: a block of n + 1 + l existentials at the end of the context holds the coerced context, the guessed junk element and the values of the l arguments, and the atom itself is then a symbol of the atomic diagram language – or of the marker, or of the block – applied to those values. ⊥, → and ∀ are structural, so no de Bruijn index of the kernel moves.

def DescriptiveComplexity.vr {L : FirstOrder.Language} {B : SOBlock} {N : ℕ} (i : Fin N) : (tgtLang L B).Term (Empty ⊕ Fin N)

A variable of the body of a translated atom.

Equations

• DescriptiveComplexity.vr i = FirstOrder.Language.var (Sum.inr i)

def DescriptiveComplexity.xIdx (n l : ℕ) (i : Fin n) : Fin (n + (n + 1 + l))

The i-th variable of the original context.

Equations

• DescriptiveComplexity.xIdx n l i = Fin.castAdd (n + 1 + l) i

def DescriptiveComplexity.uIdx (n l : ℕ) (i : Fin n) : Fin (n + (n + 1 + l))

The i-th variable of the context, coerced to an original element.

Equations

• DescriptiveComplexity.uIdx n l i = ⟨n + ↑i, ⋯⟩

def DescriptiveComplexity.zIdx (n l : ℕ) : Fin (n + (n + 1 + l))

The guessed junk element.

Equations

• DescriptiveComplexity.zIdx n l = ⟨n + n, ⋯⟩

def DescriptiveComplexity.yIdx (n l : ℕ) (j : Fin l) : Fin (n + (n + 1 + l))

The value of the j-th argument of the atom.

Equations

• DescriptiveComplexity.yIdx n l j = ⟨n + n + 1 + ↑j, ⋯⟩

def DescriptiveComplexity.oldOf {L : FirstOrder.Language} {B : SOBlock} {N : ℕ} (i : Fin N) : (tgtLang L B).BoundedFormula Empty N

old x, in the target kernel language.

Equations

• DescriptiveComplexity.oldOf i = FirstOrder.Language.BoundedFormula.rel (Sum.inl (Sum.inr FirstOrder.Language.oldSym)) ![DescriptiveComplexity.vr i]

def DescriptiveComplexity.zOf {L : FirstOrder.Language} {B : SOBlock} {N : ℕ} (i : Fin N) : (tgtLang L B).BoundedFormula Empty N

The relation variable naming the junk element, applied to one variable.

Equations

• DescriptiveComplexity.zOf i = FirstOrder.Language.BoundedFormula.rel (Sum.inr ⟨Sum.inr (), ⋯⟩) fun (x : Fin ((DescriptiveComplexity.jBlock B).arity (Sum.inr ()))) => DescriptiveComplexity.vr i

def DescriptiveComplexity.eqOf {L : FirstOrder.Language} {B : SOBlock} {N : ℕ} (a b : Fin N) : (tgtLang L B).BoundedFormula Empty N

An equality of two variables.

Equations

• DescriptiveComplexity.eqOf a b = FirstOrder.Language.BoundedFormula.equal (DescriptiveComplexity.vr a) (DescriptiveComplexity.vr b)

def DescriptiveComplexity.graphSym {L : FirstOrder.Language} {B : SOBlock} (n : ℕ) (t : (srcLang L B).Term (Empty ⊕ Fin n)) : (atomLang L).Relations (n + 1)

The graph of a term, as a symbol of the atomic diagram language: the equality t(x̄) = xₙ in n + 1 variables.

Equations

• DescriptiveComplexity.graphSym n t = Sum.inr (FirstOrder.Language.Term.relabel Fin.castSucc (DescriptiveComplexity.termShadow t), FirstOrder.Language.var (Fin.last n))

def DescriptiveComplexity.argCl {L : FirstOrder.Language} {B : SOBlock} (n l : ℕ) : (srcLang L B).Term (Empty ⊕ Fin n) → Fin l → (tgtLang L B).BoundedFormula Empty (n + (n + 1 + l))

What pins the value of one argument: a variable takes the value the context gives it – which may be an invented one – and a function application the value its graph gives on the coerced context.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.argCl n l (FirstOrder.Language.var (Sum.inl e)) x✝ = e.elim
• DescriptiveComplexity.argCl n l (FirstOrder.Language.var (Sum.inr i)) x✝ = DescriptiveComplexity.eqOf (DescriptiveComplexity.yIdx n l x✝) (DescriptiveComplexity.xIdx n l i)

def DescriptiveComplexity.atomBody {L : FirstOrder.Language} {B : SOBlock} (n l : ℕ) (ts : Fin l → (srcLang L B).Term (Empty ⊕ Fin n)) (core : (tgtLang L B).BoundedFormula Empty (n + (n + 1 + l))) : (tgtLang L B).BoundedFormula Empty (n + (n + 1 + l))

The body of a translated atom.

Equations

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

def DescriptiveComplexity.flatAtom {L : FirstOrder.Language} {B : SOBlock} (n l : ℕ) (ts : Fin l → (srcLang L B).Term (Empty ⊕ Fin n)) (core : (tgtLang L B).BoundedFormula Empty (n + (n + 1 + l))) : (tgtLang L B).BoundedFormula Empty n

A translated atom.

Equations

• DescriptiveComplexity.flatAtom n l ts core = DescriptiveComplexity.exs (n + 1 + l) (DescriptiveComplexity.atomBody n l ts core)

def DescriptiveComplexity.flat {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} : (srcLang L B).BoundedFormula Empty n → (tgtLang L B).BoundedFormula Empty n

The translation of the kernel: atom by atom, in place.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.flat FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
• DescriptiveComplexity.flat (f₁.imp f₂) = (DescriptiveComplexity.flat f₁).imp (DescriptiveComplexity.flat f₂)
• DescriptiveComplexity.flat f.all = (DescriptiveComplexity.flat f).all

The intended values of the fresh variables

@[instance_reducible]

noncomputable def DescriptiveComplexity.tgtStruct {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m : ℕ} (μ' : (jBlock B).Assignment (A ⊕ Fin m)) : (tgtLang L B).Structure (A ⊕ Fin m)

The structure the translated kernel is read in: the atomic diagram, extended, and expanded by the enlarged block.

Equations

• DescriptiveComplexity.tgtStruct μ' = (DescriptiveComplexity.newLang (DescriptiveComplexity.atomLang L)).sumStructure (DescriptiveComplexity.jBlock B).lang (A ⊕ Fin m)

def DescriptiveComplexity.jAssign {B : SOBlock} {A : Type} {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) : (jBlock B).Assignment (A ⊕ Fin m)

The enlarged assignment: the given one, plus the singleton naming the junk element.

Equations

• DescriptiveComplexity.jAssign z μ (Sum.inl b) = μ b
• DescriptiveComplexity.jAssign z μ (Sum.inr val) = fun (u : Fin ((DescriptiveComplexity.jBlock B).arity (Sum.inr val)) → A ⊕ Fin m) => u ⟨0, Nat.zero_lt_one⟩ = Sum.inl z

noncomputable def DescriptiveComplexity.canonYs {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l : ℕ} (ts : Fin l → (srcLang L B).Term (Empty ⊕ Fin n)) (w : Fin n → A ⊕ Fin m) : Fin (n + (n + 1 + l)) → A ⊕ Fin m

The values the body of a translated atom forces on its fresh variables: the context is kept, the coerced context is the context with the invented values replaced by the junk, and each argument variable holds the value of its term.

Equations

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

theorem DescriptiveComplexity.canonYs_x {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l : ℕ} (ts : Fin l → (srcLang L B).Term (Empty ⊕ Fin n)) (w : Fin n → A ⊕ Fin m) (i : Fin n) : canonYs z μ ts w (xIdx n l i) = w i

theorem DescriptiveComplexity.canonYs_u {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l : ℕ} (ts : Fin l → (srcLang L B).Term (Empty ⊕ Fin n)) (w : Fin n → A ⊕ Fin m) (i : Fin n) : canonYs z μ ts w (uIdx n l i) = Sum.inl (oldPartAt A m z (w i))

theorem DescriptiveComplexity.canonYs_z {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l : ℕ} (ts : Fin l → (srcLang L B).Term (Empty ⊕ Fin n)) (w : Fin n → A ⊕ Fin m) : canonYs z μ ts w (zIdx n l) = Sum.inl z

theorem DescriptiveComplexity.canonYs_y {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l : ℕ} (ts : Fin l → (srcLang L B).Term (Empty ⊕ Fin n)) (w : Fin n → A ⊕ Fin m) (j : Fin l) : canonYs z μ ts w (yIdx n l j) = FirstOrder.Language.Term.realize (Sum.elim (fun (a : Empty) => isEmptyElim a) w) (ts j)

theorem DescriptiveComplexity.idx_cases {n l : ℕ} (p : Fin (n + (n + 1 + l))) : (∃ (i : Fin n), p = xIdx n l i) ∨ (∃ (i : Fin n), p = uIdx n l i) ∨ p = zIdx n l ∨ ∃ (j : Fin l), p = yIdx n l j

The four families of indices exhaust the body's context.

What the body of a translated atom says

theorem DescriptiveComplexity.realize_zOf' {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m N : ℕ} (i : Fin N) (ys : Fin N → A ⊕ Fin m) (μ' : (jBlock B).Assignment (A ⊕ Fin m)) : (zOf i).Realize (fun (a : Empty) => isEmptyElim a) ys ↔ μ' (Sum.inr ()) fun (x : Fin ((jBlock B).arity (Sum.inr ()))) => ys i

theorem DescriptiveComplexity.realize_zOf {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {N : ℕ} (i : Fin N) (ys : Fin N → A ⊕ Fin m) : (zOf i).Realize (fun (a : Empty) => isEmptyElim a) ys ↔ ys i = Sum.inl z

theorem DescriptiveComplexity.realize_oldOf {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m N : ℕ} (i : Fin N) (ys : Fin N → A ⊕ Fin m) (μ' : (jBlock B).Assignment (A ⊕ Fin m)) : (oldOf i).Realize (fun (a : Empty) => isEmptyElim a) ys ↔ IsOld (ys i)

theorem DescriptiveComplexity.realize_eqOf {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m N : ℕ} (a b : Fin N) (ys : Fin N → A ⊕ Fin m) (μ' : (jBlock B).Assignment (A ⊕ Fin m)) : (eqOf a b).Realize (fun (a : Empty) => isEmptyElim a) ys ↔ ys a = ys b

theorem DescriptiveComplexity.realize_argCl_var {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l : ℕ} (i : Fin n) (j : Fin l) (ys : Fin (n + (n + 1 + l)) → A ⊕ Fin m) : (argCl n l (FirstOrder.Language.var (Sum.inr i)) j).Realize (fun (a : Empty) => isEmptyElim a) ys ↔ ys (yIdx n l j) = ys (xIdx n l i)

theorem DescriptiveComplexity.realize_argCl_func {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l k : ℕ} (g : L.Functions k) (ts' : Fin k → (srcLang L B).Term (Empty ⊕ Fin n)) (j : Fin l) (ys : Fin (n + (n + 1 + l)) → A ⊕ Fin m) : (argCl n l (FirstOrder.Language.func (Sum.inl (Sum.inl g)) ts') j).Realize (fun (a : Empty) => isEmptyElim a) ys ↔ ∃ (y : Fin (n + 1) → A), (∀ (i : Fin n), ys (uIdx n l i) = Sum.inl (y i.castSucc)) ∧ ys (yIdx n l j) = Sum.inl (y (Fin.last n)) ∧ FirstOrder.Language.Term.realize (fun (i : Fin n) => y i.castSucc) (termShadow (FirstOrder.Language.func (Sum.inl (Sum.inl g)) ts')) = y (Fin.last n)

def DescriptiveComplexity.ubar {A : Type} {m : ℕ} (z : A) {n : ℕ} (w : Fin n → A ⊕ Fin m) : Fin n → A

The coerced context, as a tuple of the instance.

Equations

• DescriptiveComplexity.ubar z w i = DescriptiveComplexity.oldPartAt A m z (w i)

theorem DescriptiveComplexity.elim_ubar {A : Type} {m : ℕ} (z : A) {n : ℕ} (w : Fin n → A ⊕ Fin m) : (fun (x : Empty ⊕ Fin n) => oldPartAt A m z (Sum.elim (fun (a : Empty) => isEmptyElim a) w x)) = Sum.elim (fun (a : Empty) => isEmptyElim a) (ubar z w)

theorem DescriptiveComplexity.realize_termShadow_ubar {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n : ℕ} (w : Fin n → A ⊕ Fin m) (t : (srcLang L B).Term (Empty ⊕ Fin n)) : FirstOrder.Language.Term.realize (ubar z w) (termShadow t) = oldPartAt A m z (FirstOrder.Language.Term.realize (Sum.elim (fun (a : Empty) => isEmptyElim a) w) t)

The value of a term is its shadow's, on the coerced context.

theorem DescriptiveComplexity.realize_eq_inl_shadow {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n : ℕ} (w : Fin n → A ⊕ Fin m) {k : ℕ} (g : L.Functions k) (ts' : Fin k → (srcLang L B).Term (Empty ⊕ Fin n)) : FirstOrder.Language.Term.realize (Sum.elim (fun (a : Empty) => isEmptyElim a) w) (FirstOrder.Language.func (Sum.inl (Sum.inl g)) ts') = Sum.inl (FirstOrder.Language.Term.realize (ubar z w) (termShadow (FirstOrder.Language.func (Sum.inl (Sum.inl g)) ts')))

A term that is a function application takes the value its shadow names.

theorem DescriptiveComplexity.realize_argCl_iff {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l : ℕ} (w : Fin n → A ⊕ Fin m) (t : (srcLang L B).Term (Empty ⊕ Fin n)) (j : Fin l) (ys : Fin (n + (n + 1 + l)) → A ⊕ Fin m) (hys : ∀ (i : Fin n), ys (xIdx n l i) = w i) (hu : ∀ (i : Fin n), ys (uIdx n l i) = Sum.inl (ubar z w i)) : (argCl n l t j).Realize (fun (a : Empty) => isEmptyElim a) ys ↔ ys (yIdx n l j) = FirstOrder.Language.Term.realize (Sum.elim (fun (a : Empty) => isEmptyElim a) w) t

What an argument clause says, once the coerced context is known: the argument variable holds the value of its term.

theorem DescriptiveComplexity.inl_oldPartAt_of_isOld {A : Type} {m : ℕ} (z : A) {x : A ⊕ Fin m} (h : IsOld x) : Sum.inl (oldPartAt A m z x) = x

theorem DescriptiveComplexity.inl_oldPartAt_of_not {A : Type} {m : ℕ} (z : A) {x : A ⊕ Fin m} (h : ¬IsOld x) : Sum.inl (oldPartAt A m z x) = Sum.inl z

theorem DescriptiveComplexity.realize_atomBody {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l : ℕ} (ts : Fin l → (srcLang L B).Term (Empty ⊕ Fin n)) (core : (tgtLang L B).BoundedFormula Empty (n + (n + 1 + l))) (ys : Fin (n + (n + 1 + l)) → A ⊕ Fin m) : (atomBody n l ts core).Realize (fun (a : Empty) => isEmptyElim a) ys ↔ ys (zIdx n l) = Sum.inl z ∧ (∀ (i : Fin n), (IsOld (ys (xIdx n l i)) → ys (uIdx n l i) = ys (xIdx n l i)) ∧ (¬IsOld (ys (xIdx n l i)) → ys (uIdx n l i) = ys (zIdx n l))) ∧ (∀ (j : Fin l), (argCl n l (ts j) j).Realize (fun (a : Empty) => isEmptyElim a) ys) ∧ core.Realize (fun (a : Empty) => isEmptyElim a) ys

What the body of a translated atom says, conjunct by conjunct.

theorem DescriptiveComplexity.realize_flatAtom {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l : ℕ} (ts : Fin l → (srcLang L B).Term (Empty ⊕ Fin n)) (w : Fin n → A ⊕ Fin m) (core : (tgtLang L B).BoundedFormula Empty (n + (n + 1 + l))) : (flatAtom n l ts core).Realize (fun (a : Empty) => isEmptyElim a) w ↔ core.Realize (fun (a : Empty) => isEmptyElim a) (canonYs z μ ts w)

A translated atom is its core, read at the values the body forces: the existential block is determined, so nothing is really guessed.

The translation is correct

theorem DescriptiveComplexity.realize_core_input {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l : ℕ} (ts : Fin l → (srcLang L B).Term (Empty ⊕ Fin n)) (w : Fin n → A ⊕ Fin m) (r : L.Relations l) : (FirstOrder.Language.BoundedFormula.rel (Sum.inl (Sum.inl (Sum.inl ⟨l, (r, fun (j : Fin l) => FirstOrder.Language.var j)⟩))) fun (j : Fin l) => vr (yIdx n l j)).Realize (fun (a : Empty) => isEmptyElim a) (canonYs z μ ts w) ↔ (FirstOrder.Language.BoundedFormula.rel (Sum.inl (Sum.inl r)) ts).Realize (fun (a : Empty) => isEmptyElim a) w

The core of a translated atom of the instance's vocabulary: the symbol of the atomic diagram language naming that atom, at the values of the arguments.

theorem DescriptiveComplexity.realize_core_block {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m : ℕ} (z : A) (μ : B.Assignment (A ⊕ Fin m)) {n l : ℕ} (ts : Fin l → (srcLang L B).Term (Empty ⊕ Fin n)) (w : Fin n → A ⊕ Fin m) (b : B.lang.Relations l) : (FirstOrder.Language.BoundedFormula.rel (Sum.inr ⟨Sum.inl ↑b, ⋯⟩) fun (j : Fin l) => vr (yIdx n l j)).Realize (fun (a : Empty) => isEmptyElim a) (canonYs z μ ts w) ↔ (FirstOrder.Language.BoundedFormula.rel (Sum.inr b) ts).Realize (fun (a : Empty) => isEmptyElim a) w

The core of a translated atom of a relation variable: the same variable of the enlarged block, at the values of the arguments.

theorem DescriptiveComplexity.realize_flat {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m : ℕ} {z : A} {μ : B.Assignment (A ⊕ Fin m)} {n : ℕ} (f : (srcLang L B).BoundedFormula Empty n) (w : Fin n → A ⊕ Fin m) : (flat f).Realize (fun (a : Empty) => isEmptyElim a) w ↔ f.Realize (fun (a : Empty) => isEmptyElim a) w

The translated kernel says of the atomic diagram what the kernel says of the instance: the two structures share a carrier, and the translation only replaces each atom by the symbol of the atomic diagram language that names it.

The relational problem, and the reduction to it

def DescriptiveComplexity.zSingle {L : FirstOrder.Language} (B : SOBlock) : (tgtLang L B).Sentence

The junk element is a single original element: what makes the guesses of the individual atoms agree.

Equations

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

def DescriptiveComplexity.relKernel {L : FirstOrder.Language} (B : SOBlock) (φ : (srcLang L B).Sentence) : (tgtLang L B).Sentence

The translated kernel: the junk element, and the translation of the original kernel.

Equations

• DescriptiveComplexity.relKernel B φ = DescriptiveComplexity.zSingle B ⊓ DescriptiveComplexity.flat φ

theorem DescriptiveComplexity.realize_zSingle {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {m : ℕ} (μ' : (jBlock B).Assignment (A ⊕ Fin m)) (xs : Fin 0 → A ⊕ Fin m) : FirstOrder.Language.BoundedFormula.Realize (zSingle B) (fun (a : Empty) => isEmptyElim a) xs ↔ ∃ (z : A), ∀ (u : A ⊕ Fin m), (μ' (Sum.inr ()) fun (x : Fin ((jBlock B).arity (Sum.inr ()))) => u) ↔ u = Sum.inl z

The relational problem, and the reduction to it

theorem DescriptiveComplexity.funs_one {B : SOBlock} {M : Type} (u : Fin ((jBlock B).arity (Sum.inr ())) → M) : u = fun (x : Fin ((jBlock B).arity (Sum.inr ()))) => u ⟨0, Nat.zero_lt_one⟩

theorem DescriptiveComplexity.sorealize_src_iff {L : FirstOrder.Language} (B : SOBlock) {A : Type} [instA : L.Structure A] (φ : (srcLang L B).Sentence) (z : A) (m : ℕ) : SORealize (newLang L) (A ⊕ Fin m) [B] φ true ↔ ∃ (μ : B.Assignment (A ⊕ Fin m)), FirstOrder.Language.BoundedFormula.Realize φ (fun (a : Empty) => isEmptyElim a) finZeroElim

theorem DescriptiveComplexity.sorealize_tgt_iff {L : FirstOrder.Language} (B : SOBlock) {A : Type} [instA : L.Structure A] [Nonempty A] (ψ : (tgtLang L B).Sentence) (m : ℕ) : SORealize (newLang (atomLang L)) (A ⊕ Fin m) [jBlock B] ψ true ↔ ∃ (μ' : (jBlock B).Assignment (A ⊕ Fin m)), FirstOrder.Language.BoundedFormula.Realize ψ (fun (a : Empty) => isEmptyElim a) finZeroElim

def DescriptiveComplexity.relHolds {L : FirstOrder.Language} (B : SOBlock) (φ : (srcLang L B).Sentence) (A' : Type) [(atomLang L).Structure A'] : Prop

The relational reading of an ∃SO[new] definition: the same definition over the atomic diagram language, with the junk element guessed by one more relation variable.

Equations

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

def DescriptiveComplexity.relProblem {L : FirstOrder.Language} (B : SOBlock) (φ : (srcLang L B).Sentence) : DecisionProblem (atomLang L)

It is a decision problem: ∃SO[new] sentences are isomorphism-invariant.

Equations

• DescriptiveComplexity.relProblem B φ = { Holds := fun (A' : Type) (x : (DescriptiveComplexity.atomLang L).Structure A') => DescriptiveComplexity.relHolds B φ A', iso_invariant := ⋯ }

theorem DescriptiveComplexity.sigmaSONewDefinable_relProblem {L : FirstOrder.Language} (B : SOBlock) (φ : (srcLang L B).Sentence) : SigmaSONewDefinable (relProblem B φ)

theorem DescriptiveComplexity.relProblem_iff {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instA : L.Structure A] [Nonempty A] {P : DecisionProblem L} (φ : (srcLang L B).Sentence) (hφ : ∀ (A : Type) [inst : L.Structure A] [Finite A] [Nonempty A] (z : A), P.Holds A ↔ ∃ (m : ℕ), SORealize (newLang L) (A ⊕ Fin m) [B] φ true) [Finite A] : P.Holds A ↔ (relProblem B φ).Holds A

The relational reading agrees with the original on atomic diagrams.

The theorem

theorem DescriptiveComplexity.exists_relational_of_sigmaSONewDefinable {L : FirstOrder.Language} {P : DecisionProblem L} (h : SigmaSONewDefinable P) : ∃ (L' : FirstOrder.Language) (hrel : L'.IsRelational) (Q : DecisionProblem L'), SigmaSONewDefinable Q ∧ Nonempty (FOReduction P Q)

Every ∃SO[new]-definable problem admits a first-order reduction to an ∃SO[new]-definable problem over a relational vocabulary.

The relational vocabulary is the atomic diagram language DescriptiveComplexity.atomLang, and the reduction is the identity on the carrier: only the vocabulary changes, an atomic formula of the source becoming a relation symbol of the target. The kernel of the definition is carried across by DescriptiveComplexity.flat, and what makes that possible is that the junk element of the extended universe may be guessed (DescriptiveComplexity.sigmaSONewDefinable_junk).

Composed with a hardness result proved for relational sources, this gives the hardness result for all of them, which is what DescriptiveComplexity.CofinalHard asks for.