“Some copy answers yes” stays in polynomial space

DescriptiveComplexity.ExpExpansion.someCls reads the inner problem inside one of the copies of an order-guessing expansion, and the copy is quantified existentially. This file shows that the quantifier costs nothing at DescriptiveComplexity.PSPACE, which is what makes the order-free reading of DescriptiveComplexity.EXPSPACE possible. The copy is guessed, as a relation, which is what a walk can do and a fixed point cannot; the deterministic class pays for the same existential differently, by naming the copy with one of its points (DescriptiveComplexity.Exponential.FreeTime).

Three closure properties of DescriptiveComplexity.SOTCDefinable do the work:

• guessing a relation: DescriptiveComplexity.SOTCDefinable.exBlock carries a guessed block in the state of the walk and never touches it again. The guessed block here is one unary relation variable (DescriptiveComplexity.markBlock), the copy;
• conjoining a first-order condition (DescriptiveComplexity.SOTCDefinable.and_sentence): the sentence goes into the source condition of the walk. It is what asks the guessed relation to be a copy;
• restricting to a definable part: reading the inner problem inside the guessed copy is a relativized ordered reduction to it, and membership is closed under those (DescriptiveComplexity.PFPDefinable.of_relOrderedReduction).

Conjoining a first-order condition to a walk

theorem DescriptiveComplexity.SOTCDefinable.and_sentence {F : FirstOrder.Language} [F.IsRelational] {P R : DecisionProblem F} (hR : SOTCDefinable R) (γ : (F.sum FirstOrder.Language.order).Sentence) (h : ∀ (M : Type) [inst : F.Structure M] [inst_1 : LinearOrder M] [Finite M] [Nonempty M], P.Holds M ↔ M ⊨ γ ∧ R.Holds M) : SOTCDefinable P

SO(TC) is closed under conjoining a first-order sentence: the sentence goes into the source condition of the walk, which no step and no target can undo.

The block that guesses a copy

def DescriptiveComplexity.markBlock : SOBlock

The block of a single unary relation variable: the guessed copy.

Equations

• DescriptiveComplexity.markBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 1 }

@[reducible, inline]

abbrev DescriptiveComplexity.markBlockSym : markBlock.lang.Relations 1

The guessed copy, as a symbol of the block's vocabulary.

Equations

• DescriptiveComplexity.markBlockSym = ⟨(), DescriptiveComplexity.markBlockSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.markSym (F : FirstOrder.Language) : (F.sum markBlock.lang).Relations 1

The guessed copy, as a symbol of the vocabulary the inner problem is read over.

Equations

• DescriptiveComplexity.markSym F = Sum.inr DescriptiveComplexity.markBlockSym

def DescriptiveComplexity.markSet (F : FirstOrder.Language) (M : Type) [(F.sum markBlock.lang).Structure M] : Set M

The marked part.

Equations

• DescriptiveComplexity.markSet F M = {x : M | FirstOrder.Language.Structure.RelMap (DescriptiveComplexity.markSym F) ![x]}

def DescriptiveComplexity.effSet (F : FirstOrder.Language) (M : Type) [(F.sum markBlock.lang).Structure M] : Set M

The marked part when it is nonempty, and the whole structure when it is not: a definable domain has to be inhabited, and nothing marks the guess as nonempty.

Equations

• DescriptiveComplexity.effSet F M = {x : M | x ∈ DescriptiveComplexity.markSet F M ∨ ∀ (y : M), y ∉ DescriptiveComplexity.markSet F M}

theorem DescriptiveComplexity.effSet_nonempty {F : FirstOrder.Language} {M : Type} [(F.sum markBlock.lang).Structure M] [Nonempty M] : (effSet F M).Nonempty

theorem DescriptiveComplexity.effSet_eq_markSet {F : FirstOrder.Language} {M : Type} [(F.sum markBlock.lang).Structure M] {x : M} (hx : x ∈ markSet F M) : effSet F M = markSet F M

theorem DescriptiveComplexity.mem_markSet_equiv {F : FirstOrder.Language} {M : Type} [(F.sum markBlock.lang).Structure M] {N : Type} [(F.sum markBlock.lang).Structure N] (e : (F.sum markBlock.lang).Equiv M N) (x : M) : x ∈ markSet F M ↔ e x ∈ markSet F N

theorem DescriptiveComplexity.image_markSet {F : FirstOrder.Language} {M : Type} [(F.sum markBlock.lang).Structure M] {N : Type} [(F.sum markBlock.lang).Structure N] (e : (F.sum markBlock.lang).Equiv M N) : ⇑e '' markSet F M = markSet F N

theorem DescriptiveComplexity.image_effSet {F : FirstOrder.Language} {M : Type} [(F.sum markBlock.lang).Structure M] {N : Type} [(F.sum markBlock.lang).Structure N] (e : (F.sum markBlock.lang).Equiv M N) : ⇑e '' effSet F M = effSet F N

The inner problem, read in the marked copy

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.ExpExpansion.markLangOf {L : FirstOrder.Language} (X : ExpExpansion L) : FirstOrder.Language

The vocabulary the inner problem is read over: the order-guessing one, plus the guessed copy.

Equations

• X.markLangOf = X.orderFree.E.sum DescriptiveComplexity.markBlock.lang

@[instance_reducible]

noncomputable def DescriptiveComplexity.ExpExpansion.markReduct {L : FirstOrder.Language} (X : ExpExpansion L) (M : Type) [X.markLangOf.Structure M] : X.orderFree.E.Structure M

The order-guessing structure underlying a structure that also carries a guessed copy.

Equations

• X.markReduct M = FirstOrder.Language.LHom.sumInl.reduct M

def DescriptiveComplexity.ExpExpansion.effProblem {L : FirstOrder.Language} (X : ExpExpansion L) (Q : DecisionProblem X.E) : DecisionProblem X.markLangOf

The inner problem read in the marked part – or in the whole structure when nothing is marked, so that the part is never empty.

Equations

• X.effProblem Q = { Holds := fun (M : Type) (x : X.markLangOf.Structure M) => Q.Holds (X.clsPart (DescriptiveComplexity.effSet X.orderFree.E M)), iso_invariant := ⋯ }

def DescriptiveComplexity.ExpExpansion.clsProblem {L : FirstOrder.Language} (X : ExpExpansion L) (Q : DecisionProblem X.E) : DecisionProblem X.markLangOf

The guessed copy is a copy, and the inner problem holds in it.

Equations

• X.clsProblem Q = { Holds := fun (M : Type) (x : X.markLangOf.Structure M) => X.IsCls (DescriptiveComplexity.markSet X.orderFree.E M) ∧ (X.effProblem Q).Holds M, iso_invariant := ⋯ }

Reading the inner problem inside the marked part, as a reduction

The marked part is a definable subset of the structure, so reading the inner problem there is a relativized ordered reduction to it – and PSPACE membership is closed under those. The domain formula is the marked part, widened to the whole structure when nothing is marked, since a definable domain must be inhabited.

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.ExpExpansion.markSymO {L : FirstOrder.Language} (X : ExpExpansion L) : (X.markLangOf.sum FirstOrder.Language.order).Relations 1

The mark, as a symbol of the source vocabulary of the reduction.

Equations

• X.markSymO = Sum.inl (DescriptiveComplexity.markSym X.orderFree.E)

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.ExpExpansion.origSymO {L : FirstOrder.Language} (X : ExpExpansion L) {n : ℕ} (r : X.E.Relations n) : (X.markLangOf.sum FirstOrder.Language.order).Relations n

A relation of the original vocabulary, as a symbol of the source vocabulary of the reduction.

Equations

• X.origSymO r = Sum.inl (Sum.inl (X.origSym r))

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.ExpExpansion.nullSymO {L : FirstOrder.Language} (X : ExpExpansion L) (s : X.E.Relations 0) : (X.markLangOf.sum FirstOrder.Language.order).Relations 1

The unary shift of a nullary symbol, as a symbol of the source vocabulary of the reduction.

Equations

• X.nullSymO s = Sum.inl (Sum.inl (X.nullSym s))

noncomputable def DescriptiveComplexity.ExpExpansion.noMarkF {L : FirstOrder.Language} (X : ExpExpansion L) {α : Type} : (X.markLangOf.sum FirstOrder.Language.order).Formula α

Nothing is marked.

Equations

• X.noMarkF = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.BoundedFormula.not (X.markSymO.formula₁ (FirstOrder.Language.var (Sum.inr 0))))

noncomputable def DescriptiveComplexity.ExpExpansion.effF {L : FirstOrder.Language} (X : ExpExpansion L) {α : Type} (x : α) : (X.markLangOf.sum FirstOrder.Language.order).Formula α

The domain of the reduction: the marked part, or everything when nothing is marked.

Equations

• X.effF x = X.markSymO.formula₁ (FirstOrder.Language.var x) ⊔ X.noMarkF

theorem DescriptiveComplexity.ExpExpansion.realize_noMarkF {L : FirstOrder.Language} {X : ExpExpansion L} {M : Type} [X.markLangOf.Structure M] [LinearOrder M] {α : Type} (v : α → M) : X.noMarkF.Realize v ↔ ∀ (y : M), y ∉ markSet X.orderFree.E M

theorem DescriptiveComplexity.ExpExpansion.realize_effF {L : FirstOrder.Language} {X : ExpExpansion L} {M : Type} [X.markLangOf.Structure M] [LinearOrder M] {α : Type} (v : α → M) (x : α) : (X.effF x).Realize v ↔ v x ∈ effSet X.orderFree.E M

noncomputable def DescriptiveComplexity.ExpExpansion.effInterp {L : FirstOrder.Language} (X : ExpExpansion L) : RelFOInterpretation (X.markLangOf.sum FirstOrder.Language.order) X.E Unit 1

The interpretation reading the original vocabulary inside the marked part: one point per element of the part, the relations read off the ambient structure, a nullary symbol read off the unary shift at a point of the part.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.mem_effInterp_dom {L : FirstOrder.Language} {X : ExpExpansion L} {M : Type} [X.markLangOf.Structure M] [LinearOrder M] (t : Unit) (w : Fin 1 → M) : (X.effInterp.domFormula t).Realize w ↔ w 0 ∈ effSet X.orderFree.E M

noncomputable def DescriptiveComplexity.ExpExpansion.effInterpEquiv {L : FirstOrder.Language} {X : ExpExpansion L} {M : Type} [X.markLangOf.Structure M] [LinearOrder M] : X.E.Equiv (X.clsPart (effSet X.orderFree.E M)) (X.effInterp.MapRel M)

The interpreted universe is the marked part.

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.effReduction {L : FirstOrder.Language} {X : ExpExpansion L} (Q : DecisionProblem X.E) : RelOrderedFOReduction (X.effProblem Q) Q

Reading the inner problem in the marked part is a relativized ordered reduction to it.

Equations

• DescriptiveComplexity.ExpExpansion.effReduction Q = { Tag := Unit, tagFinite := ⋯, dim := 1, toRelInterpretation := X.effInterp, dom_nonempty := ⋯, correct := ⋯ }

theorem DescriptiveComplexity.ExpExpansion.mem_PSPACE_effProblem {L : FirstOrder.Language} {X : ExpExpansion L} {Q : DecisionProblem X.E} (hQ : PSPACE.Mem Q) : PSPACE.Mem (X.effProblem Q)

The inner problem read in the marked part stays in polynomial space.

The guessed copy is a copy: the first-order guard

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.ExpExpansion.sameSymO {L : FirstOrder.Language} {X : ExpExpansion L} : (X.markLangOf.sum FirstOrder.Language.order).Relations 2

The same-order symbol, in the source vocabulary of the reduction.

Equations

• DescriptiveComplexity.ExpExpansion.sameSymO = Sum.inl (Sum.inl X.sameSym)

noncomputable def DescriptiveComplexity.ExpExpansion.isClsS {L : FirstOrder.Language} {X : ExpExpansion L} : (X.markLangOf.sum FirstOrder.Language.order).Sentence

The guard: the marked part is nonempty, and it holds exactly the points carrying the order of any one of its members.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.realize_isClsS {L : FirstOrder.Language} {X : ExpExpansion L} {M : Type} [X.markLangOf.Structure M] [LinearOrder M] : M ⊨ isClsS ↔ X.IsCls (markSet X.orderFree.E M)

theorem DescriptiveComplexity.ExpExpansion.mem_PSPACE_clsProblem {L : FirstOrder.Language} (X : ExpExpansion L) {Q : DecisionProblem X.E} (hQ : PSPACE.Mem Q) : PSPACE.Mem (X.clsProblem Q)

Guessing a copy and checking it stays in polynomial space.

Guessing the copy: “some copy answers yes” is in polynomial space

theorem DescriptiveComplexity.ExpExpansion.someCls_iff_exists_mark {L : FirstOrder.Language} (X : ExpExpansion L) {Q : DecisionProblem X.E} (N : Type) [X.orderFree.E.Structure N] : (X.someCls Q).Holds N ↔ ∃ (ρ : markBlock.Assignment N), (X.clsProblem Q).Holds N

The copy, guessed as a relation variable: a copy of the expansion is exactly a marked part that the guard accepts.

theorem DescriptiveComplexity.ExpExpansion.mem_PSPACE_someCls {L : FirstOrder.Language} (X : ExpExpansion L) {Q : DecisionProblem X.E} (hQ : PSPACE.Mem Q) : PSPACE.Mem (X.someCls Q)

“Some copy answers yes” stays in polynomial space: the copy is guessed into the state of the walk, the guard is a first-order condition on the source state, and the inner problem is read in the copy by a relativized reduction.

EXPSPACE needs no order

theorem DescriptiveComplexity.expDefinable_PSPACE_iff_free {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : ExpDefinable PSPACE P ↔ ExpDefinableFree PSPACE P

PSPACE over an expanded universe needs no order. Left to right the order is guessed into the block of the expansion (DescriptiveComplexity.ExpExpansion.orderFree) and the inner problem is replaced by “some copy answers yes” (DescriptiveComplexity.ExpExpansion.someCls), which is again in PSPACE; right to left an expansion that never mentions the order is one that ignores it.

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

SO(PFP) without the order: a partial fixed point over a second-order universe defined without an order, the equivalence being asked of structures carrying none.

Equations

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

theorem DescriptiveComplexity.sopfpDefinableFree_iff_expDefinableFree {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : SOPFPDefinableFree P ↔ ExpDefinableFree PSPACE P

theorem DescriptiveComplexity.sopfpDefinable_iff_free {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : SOPFPDefinable P ↔ SOPFPDefinableFree P

SO(≤, PFP) = SO(PFP): the order of the expansion can be guessed.

theorem DescriptiveComplexity.mem_EXPSPACE_iff_sopfpDefinableFree {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : EXPSPACE.Mem P ↔ SOPFPDefinableFree P

EXPSPACE is SO(PFP), no order needed.