What a NEXPTIME source problem looks like

DescriptiveComplexity.ExpDefinable DescriptiveComplexity.NP is the class the hardness proof for DescriptiveComplexity.WideAccept starts from, and it is stated as an existential over an expansion and a problem of NP. A machine cannot be programmed against that. This file puts it in the normal form a program is written against:

an expansion, one block of guessed relation variables, and a first-order kernel – DescriptiveComplexity.NexKernel – the problem holding at a structure exactly when some assignment of the block satisfies the kernel over its expansion.

That is the same shape as the data of the EXPSPACE program – an expansion, a block, a first-order body – with the block's relation variables guessed once rather than iterated to a fixed point, which is the whole difference between the two programs.

The order

The kernel is stated over L.sum FirstOrder.Language.order, one language wider than DescriptiveComplexity.SigmaSODefinable supplies. Nothing is added by that: a machine has an order on its universe whatever the source says, the atoms of an ordered kernel are what the program's atom machinery is written for, and a sentence that mentions no order symbol is a sentence that may. The transport is DescriptiveComplexity.orderAddLHom, the dual of DescriptiveComplexity.orderElimLHom – which eliminates an order symbol by re-quantifying it inside a block, and is the direction that costs something.

Which linear order is on the expanded universe is left to the consumer: the normal form holds at every one, so a reduction may choose the order its encoding induces and pay nothing for the choice.

Adding an order symbol to a kernel

def DescriptiveComplexity.orderAddLHom (L : FirstOrder.Language) (B : SOBlock) : L.sum B.lang →ᴸ (L.sum FirstOrder.Language.order).sum B.lang

The language morphism adding an order symbol to a first-order kernel over a block: every symbol goes to itself, and the order symbol of the target is simply not in the image. The dual of DescriptiveComplexity.orderElimLHom.

Equations

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

theorem DescriptiveComplexity.orderAddLHom_isExpansionOn (L : FirstOrder.Language) (B : SOBlock) (A : Type) (instA : L.Structure A) (lo : LinearOrder A) (ρ : B.Assignment A) : (orderAddLHom L B).IsExpansionOn A

The ordered structure is an expansion along the morphism, whatever the order: the order symbol is the only new one and no formula in the image mentions it.

theorem DescriptiveComplexity.realize_orderAdd {L : FirstOrder.Language} (B : SOBlock) (A : Type) [instA : L.Structure A] [lo : LinearOrder A] (ρ : B.Assignment A) (φ : (L.sum B.lang).Sentence) : A ⊨ (orderAddLHom L B).onSentence φ ↔ A ⊨ φ

Adding the order symbol changes no meaning.

theorem DescriptiveComplexity.exists_orderedKernel {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : SigmaSODefinable 1 P) : ∃ (B : SOBlock) (φ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence), ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ ∃ (ρ : B.Assignment A), A ⊨ φ

A Σ₁ definition, with its kernel read over the ordered expansion. The one block is the certificate the machine guesses; the kernel is what it checks; and the statement holds at every linear order, so a consumer may impose its own.

The normal form of a NEXPTIME source

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

The data a NEXPTIME hardness program is written against: an exponential expansion, one block of guessed relation variables, and a first-order kernel over the expanded vocabulary, its order, and the block.

• X : ExpExpansion L

  The exponential expansion whose points the machine's tape addresses.

• B : SOBlock

  The relation variables the machine guesses.

• ker : ((self.X.E.sum FirstOrder.Language.order).sum self.B.lang).Sentence

  The first-order sentence the machine checks.

def DescriptiveComplexity.NexKernel.Holds {L : FirstOrder.Language} (K : NexKernel L) (M : Type) [instM : K.X.E.Structure M] [LinearOrder M] : Prop

What the kernel says: some assignment of the guessed block satisfies it. This is the predicate the machine's run has to be equivalent to – guess, then check – and it is stated at an arbitrary linear order on the universe, the reduction's own being one.

Equations

• K.Holds M = ∃ (ρ : K.B.Assignment M), M ⊨ K.ker

theorem DescriptiveComplexity.exists_nexKernel {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : ExpDefinable NP P) : ∃ (K : NexKernel L), ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] [inst_4 : LinearOrder (K.X.Map A)], P.Holds A ↔ K.Holds (K.X.Map A)

Every NEXPTIME source problem has a kernel. Unfold DescriptiveComplexity.ExpDefinable DescriptiveComplexity.NP into an expansion and a Σ₁ problem over it, then the Σ₁ problem into a block and a kernel: what is left is guess an assignment over the expanded universe and check a first-order sentence, which is what a program can be written for.

The equivalence is stated at every linear order on the expanded universe, so the reduction that consumes it is free to impose the order its encoding induces (compare DescriptiveComplexity.Draw.encOrder).