The copy a point names, and EXPTIME without the order

DescriptiveComplexity.Exponential.FreeSpace reads the inner problem inside one of the copies of an order-guessing expansion and keeps it in PSPACE, the copy being guessed as a relation. A deterministic class cannot guess, so DescriptiveComplexity.PTIME needs the copy to be named by something a fixed point can carry: one element. A copy is the class of any one of its points, so “some copy answers yes” is DescriptiveComplexity.ExpExpansion.somePtCls, an existential over points, and DescriptiveComplexity.mem_PTIME_exElement – every relation variable of the induction carrying the point as a further argument – is what keeps it in PTIME.

Two steps, then:

• the inner problem read in the class of a marked point is a relativized ordered reduction to it (DescriptiveComplexity.ExpExpansion.ptReduction), so membership carries over (DescriptiveComplexity.IFPDefinable.of_relOrderedReduction);
• the mark is then existentially quantified away (DescriptiveComplexity.ExpExpansion.mem_PTIME_somePtCls).

The conclusion is DescriptiveComplexity.mem_EXPTIME_iff_solfpDefinableFree: EXPTIME is SO(LFP) with no order in the statement, as EXPSPACE is SO(PFP).

The copy a point names

def DescriptiveComplexity.ExpExpansion.ptClsSet {L : FirstOrder.Language} (X : ExpExpansion L) {N : Type} [X.orderFree.E.Structure N] (c : N) : Set N

The copy a point names: the points carrying its guessed order – or the whole structure when it carries none, so that the part is never empty.

Equations

• X.ptClsSet c = {y : N | FirstOrder.Language.Structure.RelMap X.sameSym ![c, y] ∨ ∀ (w : N), ¬FirstOrder.Language.Structure.RelMap X.sameSym ![c, w]}

theorem DescriptiveComplexity.ExpExpansion.ptClsSet_eq_of_refl {L : FirstOrder.Language} {X : ExpExpansion L} {N : Type} [X.orderFree.E.Structure N] {c : N} (h : FirstOrder.Language.Structure.RelMap X.sameSym ![c, c]) : X.ptClsSet c = {y : N | FirstOrder.Language.Structure.RelMap X.sameSym ![c, y]}

At a point that carries an order – every point of an order-guessing expansion does – the copy it names is its class.

Some copy answers yes, the copy being named by a point

theorem DescriptiveComplexity.ExpExpansion.image_ptClsSet {L : FirstOrder.Language} (X : ExpExpansion L) {N N' : Type} [X.orderFree.E.Structure N] [X.orderFree.E.Structure N'] (e : X.orderFree.E.Equiv N N') (c : N) : ⇑e '' X.ptClsSet c = X.ptClsSet (e c)

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

Some copy answers yes, the copy being named by one of its points: the problem that replaces the inner one when the inner class cannot guess.

Equations

• X.somePtCls Q = { Holds := fun (N : Type) (x : X.orderFree.E.Structure N) => ∃ (c : N), Q.Holds (X.clsPart (X.ptClsSet c)), iso_invariant := ⋯ }

The copy of a marked point, as a definable part

@[reducible, inline]

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

The vocabulary the inner problem is read over: the order-guessing one, plus a mark for the point that names the copy.

Equations

• X.ptLangOf = DescriptiveComplexity.newLang X.orderFree.E

@[instance_reducible]

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

The order-guessing structure underlying a structure that also carries a marked point.

Equations

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

def DescriptiveComplexity.ExpExpansion.markPtSet {L : FirstOrder.Language} (X : ExpExpansion L) (M : Type) [X.ptLangOf.Structure M] : Set M

The part the reduction reads: the copy the marked point names – or the whole structure when nothing marked names anything, so that the part is never empty.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.markPtSet_nonempty {L : FirstOrder.Language} {X : ExpExpansion L} {M : Type} [X.ptLangOf.Structure M] [Nonempty M] : (X.markPtSet M).Nonempty

theorem DescriptiveComplexity.ExpExpansion.markPtSet_markOne {L : FirstOrder.Language} {X : ExpExpansion L} {N : Type} [inst : X.orderFree.E.Structure N] (c : N) : X.markPtSet N = X.ptClsSet c

The marked point names the copy the point names: at the structure whose mark is a single point, the part the reduction reads is the copy of that point.

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

The inner problem read in the copy the marked point names.

Equations

• X.ptProblem Q = { Holds := fun (M : Type) (x : X.ptLangOf.Structure M) => Q.Holds (X.clsPart (X.markPtSet M)), iso_invariant := ⋯ }

The reduction reading the copy of the marked point

@[reducible, inline]

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

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

Equations

• X.oldSymO = Sum.inl (Sum.inr FirstOrder.Language.oldSym)

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.ExpExpansion.nullSymP {L : FirstOrder.Language} (X : ExpExpansion L) (s : X.E.Relations 0) : (X.ptLangOf.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.nullSymP s = Sum.inl (Sum.inl (X.nullSym s))

@[reducible, inline]

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

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

Equations

• X.sameSymP = Sum.inl (Sum.inl X.sameSym)

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

Nothing marked names anything.

Equations

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

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

The domain of the reduction: the copy the marked point names, or everything when nothing is marked.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.realize_noPtF {L : FirstOrder.Language} {X : ExpExpansion L} {M : Type} [X.ptLangOf.Structure M] [LinearOrder M] {α : Type} (v : α → M) : X.noPtF.Realize v ↔ ∀ (m w : M), ¬(FirstOrder.Language.Structure.RelMap (Sum.inr FirstOrder.Language.oldSym) ![m] ∧ FirstOrder.Language.Structure.RelMap X.sameSym ![m, w])

theorem DescriptiveComplexity.ExpExpansion.realize_ptF {L : FirstOrder.Language} {X : ExpExpansion L} {M : Type} [X.ptLangOf.Structure M] [LinearOrder M] {α : Type} (v : α → M) (x : α) : (X.ptF x).Realize v ↔ v x ∈ X.markPtSet M

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

The interpretation reading the original vocabulary inside the copy the marked point names.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.mem_ptInterp_dom {L : FirstOrder.Language} {X : ExpExpansion L} {M : Type} [X.ptLangOf.Structure M] [LinearOrder M] (t : Unit) (w : Fin 1 → M) : (X.ptInterp.domFormula t).Realize w ↔ w 0 ∈ X.markPtSet M

noncomputable def DescriptiveComplexity.ExpExpansion.ptInterpEquiv {L : FirstOrder.Language} {X : ExpExpansion L} {M : Type} [X.ptLangOf.Structure M] [LinearOrder M] : X.E.Equiv (X.clsPart (X.markPtSet M)) (X.ptInterp.MapRel M)

The interpreted universe is the copy the marked point names.

Equations

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

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

Reading the inner problem in the copy of the marked point is a relativized ordered reduction to it.

Equations

• X.ptReduction Q = { Tag := Unit, tagFinite := ⋯, dim := 1, toRelInterpretation := X.ptInterp, dom_nonempty := ⋯, correct := ⋯ }

theorem DescriptiveComplexity.ExpExpansion.mem_PTIME_ptProblem {L : FirstOrder.Language} (X : ExpExpansion L) {Q : DecisionProblem X.E} (hQ : PTIME.Mem Q) : PTIME.Mem (X.ptProblem Q)

The inner problem read in the copy of the marked point stays in polynomial time.

Quantifying the point away

theorem DescriptiveComplexity.ExpExpansion.mem_PTIME_somePtCls {L : FirstOrder.Language} (X : ExpExpansion L) {Q : DecisionProblem X.E} (hQ : PTIME.Mem Q) : PTIME.Mem (X.somePtCls Q)

“Some copy answers yes” stays in polynomial time: the point naming the copy is carried by every relation variable of the induction.

The correctness of “some copy answers yes”

theorem DescriptiveComplexity.ExpExpansion.isCls_ptClsSet {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] (c : X.orderFree.Map A) : X.IsCls (X.ptClsSet c)

The copy a point of an order-guessing expansion names is a copy: the points carrying its guessed order.

theorem DescriptiveComplexity.ExpExpansion.somePtCls_map_iff {L : FirstOrder.Language} {X : ExpExpansion L} {Q : DecisionProblem X.E} {A : Type} [L.Structure A] [Finite A] [Nonempty A] : (X.somePtCls Q).Holds (X.orderFree.Map A) ↔ ∃ (lo : LinearOrder A), Q.Holds (X.Map A)

Some copy answers yes exactly when the inner problem does, at some linear order of the instance – the same statement as DescriptiveComplexity.ExpExpansion.someCls_map_iff, with the copy named by a point rather than guessed as a set.

EXPTIME needs no order

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

PTIME over an expanded universe needs no order. The order is guessed into the block of the expansion, and the inner problem is replaced by “some copy answers yes” – the copy being named by a point, since a deterministic class cannot guess one.

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

SO(LFP) without the order: a least 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.solfpDefinableFree_iff_expDefinableFree {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : SOLFPDefinableFree P ↔ ExpDefinableFree PTIME P

theorem DescriptiveComplexity.solfpDefinable_iff_free {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : SOLFPDefinable P ↔ SOLFPDefinableFree P

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

theorem DescriptiveComplexity.mem_EXPTIME_iff_solfpDefinableFree {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : EXPTIME.Mem P ↔ SOLFPDefinableFree P

EXPTIME is SO(LFP), no order needed.