SO(TC) needs no order: the order is a guessed state component

DescriptiveComplexity.SOTCDefinable, like the clausal fragments and the reachability logics, reads its three sentences over the ordered expansion of the vocabulary and asks for the equivalence at every linear order on the universe. For SO(TC) that hypothesis is removable, and this file removes it.

The reason it is removable here and not for SO-Horn, SO-Krom, FO(TC) or FO(DTC) is the reason Fagin's theorem needs no order either: a walk over assignments of a block can guess the order and carry it along. A state of the walk is an assignment of relation variables, so one more binary variable holds a candidate order; the source condition checks that it is a linear one (DescriptiveComplexity.linearGuard), the transition condition says it does not change, and every sentence of the original specification reads it in place of the order symbol (DescriptiveComplexity.orderElimLHom and its two-copy analogue below). The order is then a component of the certificate, exactly as it is in the first block of a Σₖ₊₁ sentence (DescriptiveComplexity.SecondOrderOrdered), and nothing outside the specification sees it.

A deterministic fragment cannot do this – guessing is what the Horn and Krom kernels do not have, and their capture theorems are genuinely statements about ordered structures – so DescriptiveComplexity.PTIME, DescriptiveComplexity.NL and DescriptiveComplexity.LOGSPACE keep the hypothesis while DescriptiveComplexity.PSPACE loses it.

What this file contains

• DescriptiveComplexity.SOTCSpecFree, an SO(TC) specification whose three sentences live over the bare vocabulary expanded by copies of the block, with its semantics: acceptance is defined on structures carrying no order at all.
• DescriptiveComplexity.SOTCSpecFree.toSpec, reading such a specification as an ordinary one (the order symbol is simply never used), and DescriptiveComplexity.SOTCSpecFree.accepts_toSpec_iff.
• DescriptiveComplexity.SOTCSpec.orderFree, the converse construction: the order is guessed into the state, guarded at the source and frozen by every step (DescriptiveComplexity.SOTCSpec.orderFree_accepts_iff).
• DescriptiveComplexity.SOTCDefinableFree and the equivalence DescriptiveComplexity.sotcDefinable_iff_free, whence DescriptiveComplexity.mem_PSPACE_iff_sotcDefinableFree: membership in PSPACE is definability by an order-free specification.

Order-free specifications

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

An SO(TC) specification that does not see a linear order: as in DescriptiveComplexity.SOTCSpec, the states of the walk are the assignments of a block, but the three sentences live over the bare vocabulary expanded by copies of the block, with no order symbol available.

• B : SOBlock

  The block whose assignments are the states of the walk.

• step : ((L.sum self.B.lang).sum self.B.lang).Sentence

  The transition sentence, over two copies of the block: the current state reads the first copy, the next state the second.

• src : (L.sum self.B.lang).Sentence

  The sentence defining the admissible starting states.

• tgt : (L.sum self.B.lang).Sentence

  The sentence defining the accepting states.

@[reducible, inline]

abbrev DescriptiveComplexity.SOTCSpecFree.State {L : FirstOrder.Language} (spec : SOTCSpecFree L) (A : Type) : Type

A state of the walk: an assignment of the block.

Equations

• spec.State A = spec.B.Assignment A

def DescriptiveComplexity.SOTCSpecFree.Step {L : FirstOrder.Language} (spec : SOTCSpecFree L) {A : Type} [L.Structure A] (ρ σ : spec.State A) : Prop

One step of the walk: the transition sentence, read with the current state in the first copy of the block and the next state in the second.

Equations

• spec.Step ρ σ = A ⊨ spec.step

@[reducible, inline]

abbrev DescriptiveComplexity.SOTCSpecFree.Reach {L : FirstOrder.Language} (spec : SOTCSpecFree L) {A : Type} [L.Structure A] : spec.State A → spec.State A → Prop

Reachability in the walk: the reflexive-transitive closure of DescriptiveComplexity.SOTCSpecFree.Step.

Equations

• spec.Reach = Relation.ReflTransGen spec.Step

def DescriptiveComplexity.SOTCSpecFree.IsSrc {L : FirstOrder.Language} (spec : SOTCSpecFree L) {A : Type} [L.Structure A] (ρ : spec.State A) : Prop

A state is a starting state when it satisfies the source sentence.

Equations

• spec.IsSrc ρ = A ⊨ spec.src

def DescriptiveComplexity.SOTCSpecFree.IsTgt {L : FirstOrder.Language} (spec : SOTCSpecFree L) {A : Type} [L.Structure A] (ρ : spec.State A) : Prop

A state is accepting when it satisfies the target sentence.

Equations

• spec.IsTgt ρ = A ⊨ spec.tgt

def DescriptiveComplexity.SOTCSpecFree.Accepts {L : FirstOrder.Language} (spec : SOTCSpecFree L) (A : Type) [L.Structure A] : Prop

The structure is accepted: some accepting state is reachable from some starting state. No order on A is involved.

Equations

• spec.Accepts A = ∃ (ρ : spec.State A) (σ : spec.State A), spec.IsSrc ρ ∧ spec.IsTgt σ ∧ spec.Reach ρ σ

Reading an order-free specification as an ordinary one

The easy direction: a specification that does not mention the order is one that happens never to use it. The language morphism below adds the order symbol to the vocabulary, and the two structures agree on everything else.

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

Adding the order to the vocabulary, over one copy of a block.

Equations

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

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

Adding the order to the vocabulary, over two copies of a block.

Equations

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

theorem DescriptiveComplexity.addOrderOne_isExpansionOn {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ : B.Assignment A) : (addOrderOne L B).IsExpansionOn A

theorem DescriptiveComplexity.addOrderTwo_isExpansionOn {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ σ : B.Assignment A) : (addOrderTwo L B).IsExpansionOn A

def DescriptiveComplexity.SOTCSpecFree.toSpec {L : FirstOrder.Language} (spec : SOTCSpecFree L) : SOTCSpec L

An order-free specification, read as an ordinary one: the three sentences are transported along DescriptiveComplexity.addOrderOne and DescriptiveComplexity.addOrderTwo, so the order symbol is present in the vocabulary and used nowhere.

Equations

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

theorem DescriptiveComplexity.SOTCSpecFree.toSpec_step_iff {L : FirstOrder.Language} {spec : SOTCSpecFree L} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ σ : spec.State A) : spec.toSpec.Step ρ σ ↔ spec.Step ρ σ

theorem DescriptiveComplexity.SOTCSpecFree.toSpec_isSrc_iff {L : FirstOrder.Language} {spec : SOTCSpecFree L} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ : spec.State A) : spec.toSpec.IsSrc ρ ↔ spec.IsSrc ρ

theorem DescriptiveComplexity.SOTCSpecFree.toSpec_isTgt_iff {L : FirstOrder.Language} {spec : SOTCSpecFree L} {A : Type} [instL : L.Structure A] [LinearOrder A] (ρ : spec.State A) : spec.toSpec.IsTgt ρ ↔ spec.IsTgt ρ

theorem DescriptiveComplexity.SOTCSpecFree.accepts_toSpec_iff {L : FirstOrder.Language} {spec : SOTCSpecFree L} {A : Type} [instL : L.Structure A] [LinearOrder A] : spec.toSpec.Accepts A ↔ spec.Accepts A

Acceptance does not depend on the order, for a specification that does not mention it.

The order symbol, eliminated in favor of a state component

The hard direction. The block of the walk is extended by one binary relation variable (DescriptiveComplexity.SOBlock.withOrder, shared with the order elimination of DescriptiveComplexity.SecondOrderOrdered), the three sentences read that variable in place of the order symbol, the source condition adds DescriptiveComplexity.linearGuard and the transition condition adds that the variable does not change.

@[reducible, inline]

abbrev DescriptiveComplexity.ordFstSym (L : FirstOrder.Language) (B : SOBlock) : ((L.sum B.withOrder.lang).sum B.withOrder.lang).Relations 2

The order variable of the current state, as a symbol of the two-copy expansion.

Equations

• DescriptiveComplexity.ordFstSym L B = Sum.inl (DescriptiveComplexity.ordVarSym L B)

@[reducible, inline]

abbrev DescriptiveComplexity.ordSndSym (L : FirstOrder.Language) (B : SOBlock) : ((L.sum B.withOrder.lang).sum B.withOrder.lang).Relations 2

The order variable of the next state, as a symbol of the two-copy expansion.

Equations

• DescriptiveComplexity.ordSndSym L B = Sum.inr B.orderSym

noncomputable def DescriptiveComplexity.fixedOrdS (L : FirstOrder.Language) (B : SOBlock) : ((L.sum B.withOrder.lang).sum B.withOrder.lang).Sentence

The guessed order does not change: the order variables of the two copies of the block agree.

Equations

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

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

The language morphism eliminating the order symbol of the ordered expansion, over two copies of a block: the order is read in the copy holding the current state.

Equations

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

theorem DescriptiveComplexity.realize_fixedOrdS {L : FirstOrder.Language} {B : SOBlock} {A : Type} (instA : L.Structure A) (ρ σ : B.withOrder.Assignment A) : A ⊨ fixedOrdS L B ↔ ∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ σ (Sum.inl ()) w

Realization of DescriptiveComplexity.fixedOrdS: the two copies assign the same relation to the order variable.

theorem DescriptiveComplexity.orderElimTwoLHom_isExpansionOn (L : FirstOrder.Language) (B : SOBlock) (A : Type) (instA : L.Structure A) (lo : LinearOrder A) (ρ σ : B.withOrder.Assignment A) (hord : ∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ w 0 ≤ w 1) : (orderElimTwoLHom L B).IsExpansionOn A

The two-copy analogue of DescriptiveComplexity.orderElimLHom_isExpansionOn: when the current state assigns the linear order of the structure to the order variable, the two-copy block expansion is an expansion along DescriptiveComplexity.orderElimTwoLHom of the ordered one.

The order-free reading of a specification

noncomputable def DescriptiveComplexity.SOTCSpec.orderFree {L : FirstOrder.Language} (spec : SOTCSpec L) : SOTCSpecFree L

The order-free reading of an SO(TC) specification: its state carries one extra binary relation variable holding a guessed order, the source condition checks that the guess is a linear order, every step freezes it, and the three sentences read it in place of the order symbol.

Equations

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

theorem DescriptiveComplexity.realize_orderElim_one {L : FirstOrder.Language} {A : Type} [instL : L.Structure A] [lo : LinearOrder A] {B : SOBlock} (ρ : B.withOrder.Assignment A) (hord : ∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ w 0 ≤ w 1) (φ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : A ⊨ (orderElimLHom L B).onSentence φ ↔ A ⊨ φ

A sentence over the ordered expansion and one copy of a block says, read through DescriptiveComplexity.orderElimLHom at a state whose order variable holds the order, what it says of the underlying assignment.

theorem DescriptiveComplexity.realize_orderElim_two {L : FirstOrder.Language} {A : Type} [instL : L.Structure A] [lo : LinearOrder A] {B : SOBlock} (ρ σ : B.withOrder.Assignment A) (hord : ∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ w 0 ≤ w 1) (φ : (((L.sum FirstOrder.Language.order).sum B.lang).sum B.lang).Sentence) : A ⊨ (orderElimTwoLHom L B).onSentence φ ↔ A ⊨ φ

The two-copy analogue of DescriptiveComplexity.realize_orderElim_one: the order is read in the copy holding the current state.

theorem DescriptiveComplexity.realize_linearGuard_of_hord {L : FirstOrder.Language} {spec : SOTCSpec L} {A : Type} [instL : L.Structure A] [lo : LinearOrder A] {ρ : spec.B.withOrder.Assignment A} (hord : ∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ w 0 ≤ w 1) : A ⊨ linearGuard L spec.B

At a state whose order variable holds the order of the structure, the guard of DescriptiveComplexity.SOTCSpec.orderFree is satisfied.

theorem DescriptiveComplexity.SOTCSpec.orderFree_isSrc_iff {L : FirstOrder.Language} {spec : SOTCSpec L} {A : Type} [instL : L.Structure A] [lo : LinearOrder A] {ρ : spec.B.withOrder.Assignment A} (hord : ∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ w 0 ≤ w 1) : spec.orderFree.IsSrc ρ ↔ spec.IsSrc (spec.B.restPart ρ)

theorem DescriptiveComplexity.SOTCSpec.orderFree_isTgt_iff {L : FirstOrder.Language} {spec : SOTCSpec L} {A : Type} [instL : L.Structure A] [lo : LinearOrder A] {ρ : spec.B.withOrder.Assignment A} (hord : ∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ w 0 ≤ w 1) : spec.orderFree.IsTgt ρ ↔ spec.IsTgt (spec.B.restPart ρ)

theorem DescriptiveComplexity.SOTCSpec.orderFree_step_iff {L : FirstOrder.Language} {spec : SOTCSpec L} {A : Type} [instL : L.Structure A] [lo : LinearOrder A] {ρ σ : spec.B.withOrder.Assignment A} (hord : ∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ w 0 ≤ w 1) : spec.orderFree.Step ρ σ ↔ (∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ σ (Sum.inl ()) w) ∧ spec.Step (spec.B.restPart ρ) (spec.B.restPart σ)

theorem DescriptiveComplexity.SOTCSpec.orderFree_reach {L : FirstOrder.Language} {spec : SOTCSpec L} {A : Type} [instL : L.Structure A] [lo : LinearOrder A] {ρ σ : spec.B.withOrder.Assignment A} (hord : ∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ w 0 ≤ w 1) (h : spec.orderFree.Reach ρ σ) : (∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ σ (Sum.inl ()) w) ∧ spec.Reach (spec.B.restPart ρ) (spec.B.restPart σ)

The guessed order is the same all along a walk, and the rest of the state walks in the original specification.

theorem DescriptiveComplexity.SOTCSpec.orderFree_reach_of {L : FirstOrder.Language} {spec : SOTCSpec L} {A : Type} [instL : L.Structure A] [LinearOrder A] {ρ₁ σ₁ : spec.B.Assignment A} (h : spec.Reach ρ₁ σ₁) : spec.orderFree.Reach (spec.B.joinOrder (fun (w : Fin 2 → A) => w 0 ≤ w 1) ρ₁) (spec.B.joinOrder (fun (w : Fin 2 → A) => w 0 ≤ w 1) σ₁)

The converse walk: a walk of the original specification, run with the order of the structure guessed into every state.

theorem DescriptiveComplexity.SOTCSpec.orderFree_accepts_iff {L : FirstOrder.Language} {spec : SOTCSpec L} (A : Type) [instL : L.Structure A] : spec.orderFree.Accepts A ↔ ∃ (lo : LinearOrder A), spec.Accepts A

Acceptance by the order-free reading is acceptance under a guessed order: the walk accepts exactly when the original one accepts for some linear order on the universe. Together with order-invariance – the equivalence required at every linear order in DescriptiveComplexity.SOTCDefinable – this is what removes the hypothesis.

Order-free SO(TC) definability

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

A decision problem is order-free SO(TC) definable if it is defined by a DescriptiveComplexity.SOTCSpecFree on nonempty finite structures – with no linear order in the statement at all, unlike DescriptiveComplexity.SOTCDefinable.

Equations

• DescriptiveComplexity.SOTCDefinableFree P = ∃ (spec : DescriptiveComplexity.SOTCSpecFree L), ∀ (A : Type) [inst : L.Structure A] [Finite A] [Nonempty A], P.Holds A ↔ spec.Accepts A

theorem DescriptiveComplexity.sotcDefinable_iff_free {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} : SOTCDefinable P ↔ SOTCDefinableFree P

The order of SO(TC) can be guessed: order-invariant SO(TC) definability over ordered structures and order-free SO(TC) definability are the same notion. Left to right the order is guessed into the state (DescriptiveComplexity.SOTCSpec.orderFree) – a linear order exists on every finite universe, and by order-invariance any one of them will do; right to left a specification that never mentions the order is one that ignores it.

theorem DescriptiveComplexity.mem_PSPACE_iff_sotcDefinableFree {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : PSPACE.Mem P ↔ SOTCDefinableFree P

PSPACE needs no order: membership is definability by an order-free SO(TC) specification.