Value invention, bounded

DescriptiveComplexity.SigmaSONewDefinable guesses a finite extension A ⊕ Fin m of the instance with m unbounded, and that single freedom is what takes existential second-order logic from NP up to RE: the yes-instances become those found by an unbounded search over finite witnesses.

This file puts the bound back, as a parameter. ∃SO[new, d] guesses an extension with at most Nat.card (Fin d → A) invented values – as many as there are d-tuples of the instance – and the point of the notion is that the bound does exactly what it should: it hands the search space back to the instance, so the class is NP again. Read beside PSPACE = NL.exp, the family reads invent nothing (Σ₁), invent polynomially many (here), invent exponentially many (NEXPTIME) and invent unboundedly many (RE): one definition with one parameter.

What is here

• DescriptiveComplexity.SigmaSONewBddDefinable: the polynomial bound;
• DescriptiveComplexity.SigmaSONewExpDefinable: the exponential one, whose invented values are as many as the instance has tuples of c relations of arity d;
• DescriptiveComplexity.SigmaSODefinable.toNewBdd: Σ₁ ⊆ ∃SO[new, d], by inventing nothing, which is the easy half of ∃SO[new, d] = NP.

The converse half – that a bounded extension is definable inside the instance's own d-tuples, so the guess can be moved back onto A – is the substance, and lives in DescriptiveComplexity.SecondOrderNewBddPull, where the d-dimensional interpreted universe enters; together the two give DescriptiveComplexity.sigmaSONewBddDefinable_iff_sigmaSODefinable.

Note that neither the bound nor its absence is a weakening of the other: a definability statement is an equivalence, so relaxing the bound loses the backward direction and tightening it loses the forward one. Passing between the notions means re-guarding the sentence, not reusing it.

def DescriptiveComplexity.SigmaSONewBddDefinable {L : FirstOrder.Language} [L.IsRelational] (d : ℕ) (P : DecisionProblem L) : Prop

Definability in ∃SO[new, d]: one existential second-order block over a universe extended by at most Nat.card (Fin d → A) invented values, and a first-order kernel. The bound is the only difference from DescriptiveComplexity.SigmaSONewDefinable.

Equations

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

theorem DescriptiveComplexity.sigmaSONewBddDefinable_congr {L : FirstOrder.Language} [L.IsRelational] {d : ℕ} {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : SigmaSONewBddDefinable d P ↔ SigmaSONewBddDefinable d Q

∃SO[new, d]-definability only depends on the finite instances of a problem, as ∃SO[new]-definability does.

theorem DescriptiveComplexity.SigmaSODefinable.toNewBdd {L : FirstOrder.Language} [L.IsRelational] {d : ℕ} {P : DecisionProblem L} (h : SigmaSODefinable 1 P) : SigmaSONewBddDefinable d P

Σ₁ ⊆ ∃SO[new, d]: an ∃SO sentence becomes an ∃SO[new, d] sentence when guarded by “nothing was invented”, the bound being satisfied by inventing nothing at all.

Inventing exponentially many values

def DescriptiveComplexity.SigmaSONewExpDefinable {L : FirstOrder.Language} [L.IsRelational] (c d : ℕ) (P : DecisionProblem L) : Prop

Definability in ∃SO[new, exp c d]: the same logic with the number of invented values held to 2 ^ (c · nᵈ) – as many as the instance has tuples of c relations of arity d, which is the size of an exponential expansion of it. This is the middle rung of the family: invent nothing is Σ₁, invent polynomially many is DescriptiveComplexity.SigmaSONewBddDefinable, invent unboundedly many is DescriptiveComplexity.SigmaSONewDefinable.

Two constants and not one: at a one-element instance nᵈ is 1 whatever d is, so a bound of 2 ^ nᵈ would be the constant 2 there, while an expansion's points at such an instance are |Tag| · 2 ^ |B.ι| – a constant the expansion chooses. The factor c is what lets an arbitrary expansion fit.

Equations

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

theorem DescriptiveComplexity.sigmaSONewExpDefinable_congr {L : FirstOrder.Language} [L.IsRelational] {c d : ℕ} {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : SigmaSONewExpDefinable c d P ↔ SigmaSONewExpDefinable c d Q

∃SO[new, exp d]-definability only depends on the finite instances of a problem.