SO(TC): second-order logic with transitive closure

The logic that captures polynomial space on ordered structures (Immerman 1999, ch. 10): a transitive closure taken not over tuples of elements, as in DescriptiveComplexity.TransitiveClosure, but over tuples of relations. A state of the walk is an assignment of relations to a second-order quantifier block, so a structure of size n has 2^(n^a) states and a walk through them is a computation of exponentially many steps – each one first-order, hence cheap – on a polynomial amount of remembered information. That is exactly the resource PSPACE measures.

Why no fragment of plain SO would do

DescriptiveComplexity.SigmaSODefinable and its levels give the polynomial hierarchy, and plain second-order logic gives PH as a whole (Fagin 1974; Stockmeyer 1976), so no fragment of plain SO can define PSPACE without collapsing PH. Some iteration operator is unavoidable, and the transitive closure is the cheapest one: it needs no positivity condition, no stage or inflationary machinery, and no syntax of its own.

The operator as data

As in DescriptiveComplexity.TransitiveClosure (and for the same reasons – not touching Mathlib's FirstOrder.Language.BoundedFormula), the operator lives at the Lean level. A DescriptiveComplexity.SOTCSpec bundles

• a second-order quantifier block B, whose assignments are the states of the walk;
• a step sentence over the base vocabulary expanded by the order and by two copies of the block – the current state and the next one;
• src and tgt sentences over one copy of the block.

Reachability itself is Relation.ReflTransGen, and a structure is accepted when some tgt state is reachable from some src state (DescriptiveComplexity.SOTCSpec.Accepts). A single application of TC in front of a first-order matrix is taken as the definition, exactly as a single existential block is taken as the definition of Σ₁-definability.

No modes, no tuples

DescriptiveComplexity.TCSpec carries a finite mode beside its tuple of elements, because a tuple of elements cannot hold finite data on a one-element universe. Here nothing of the sort is needed: a relation variable of arity 0 is a bit, so finite control is already inside a block, and a relation variable of arity 1 holding a singleton is an element register. A state is therefore a bare DescriptiveComplexity.SOBlock.Assignment and the walk carries no extra components – which also makes the pullback of a specification through an interpretation (DescriptiveComplexity.SecondOrderTransitiveClosurePull) purely a matter of pulling the block back.

What this file contains

The semantics (DescriptiveComplexity.SOTCSpec.Step, DescriptiveComplexity.SOTCSpec.Reach, DescriptiveComplexity.SOTCSpec.Accepts), its isomorphism-invariance, the transfer of acceptance along a bijection of states (DescriptiveComplexity.SOTCSpec.accepts_congr, the workhorse of the pullback), and the definability notion DescriptiveComplexity.SOTCDefinable. The class DescriptiveComplexity.PSPACE itself is built on top of it in DescriptiveComplexity.PSpace, once closure under reductions is available.

Expanding a structure by one or two copies of a block

theorem DescriptiveComplexity.realize_sentence_of_equiv {L' : FirstOrder.Language} {M N : Type} {instM : L'.Structure M} {instN : L'.Structure N} (e : L'.Equiv M N) (φ : L'.Sentence) : M ⊨ φ ↔ N ⊨ φ

FirstOrder.Language.StrongHomClass.realize_sentence with the two structures passed explicitly rather than by instance search. The structures a walk is read against are built from block assignments (DescriptiveComplexity.SOBlock.structure₁, DescriptiveComplexity.SOBlock.structure₂) and are never instances, so every transport in this file and in DescriptiveComplexity.SecondOrderTransitiveClosurePull goes through this form.

@[instance_reducible]

def DescriptiveComplexity.SOBlock.structure₁ {L : FirstOrder.Language} (B : SOBlock) {A : Type} [inst : L.Structure A] (ρ : B.Assignment A) : (L.sum B.lang).Structure A

The structure over L expanded by one copy of a block's vocabulary, interpreted by an assignment.

Equations

• B.structure₁ ρ = L.sumStructure B.lang A

@[instance_reducible]

def DescriptiveComplexity.SOBlock.structure₂ {L : FirstOrder.Language} (B : SOBlock) {A : Type} [inst : L.Structure A] (ρ σ : B.Assignment A) : ((L.sum B.lang).sum B.lang).Structure A

The structure over L expanded by two copies of a block's vocabulary – the current state and the next one – interpreted by two assignments.

Equations

• B.structure₂ ρ σ = (L.sum B.lang).sumStructure B.lang A

def DescriptiveComplexity.SOBlock.extendEquiv' (B : SOBlock) {L' : FirstOrder.Language} {M N : Type} {instM : L'.Structure M} {instN : L'.Structure N} (e : L'.Equiv M N) (ρ : B.Assignment M) : (L'.sum B.lang).Equiv M N

DescriptiveComplexity.SOBlock.extendEquiv with the two structures passed explicitly rather than by instance search, for the same reason as DescriptiveComplexity.realize_sentence_of_equiv: the layers a walk is read against are block expansions, which are not instances.

Equations

• B.extendEquiv' e ρ = B.extendEquiv e ρ

def DescriptiveComplexity.SOBlock.assignEquiv (B : SOBlock) {A A' : Type} (e : A ≃ A') : B.Assignment A ≃ B.Assignment A'

Transport of block assignments along an equivalence of universes, as an equivalence: the states of the walk are in bijection with the states of the transported walk.

Equations

• B.assignEquiv e = { toFun := B.mapAssign e, invFun := B.mapAssign e.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem DescriptiveComplexity.SOBlock.assignEquiv_apply (B : SOBlock) {A A' : Type} (e : A ≃ A') (ρ : B.Assignment A) : (B.assignEquiv e) ρ = B.mapAssign e ρ

def DescriptiveComplexity.SOBlock.extendEquiv₂ {L : FirstOrder.Language} (B : SOBlock) {A A' : Type} [L.Structure A] [L.Structure A'] (e : L.Equiv A A') (ρ σ : B.Assignment A) : ((L.sum B.lang).sum B.lang).Equiv A A'

An L-isomorphism extends to L expanded by two copies of a block, the two assignments being transported.

Equations

• B.extendEquiv₂ e ρ σ = B.extendEquiv (B.extendEquiv e ρ) σ

Specifications

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

A single-TC definition over a second-order block: the states of the walk are the assignments of the block B, and the transition, source and target conditions are first-order sentences over the base vocabulary expanded by the order and by copies of the block. The transition sentence sees two copies – the current state and the next one.

The order is visible to all three sentences, as the ordered setting of the capture theorem allows; the problem itself does not see it (see DescriptiveComplexity.SOTCDefinable).

• B : SOBlock

  The block whose assignments are the states of the walk.

• step : (((L.sum FirstOrder.Language.order).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 FirstOrder.Language.order).sum self.B.lang).Sentence

  The sentence defining the admissible starting states.

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

  The sentence defining the accepting states.

@[reducible, inline]

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

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

Equations

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

def DescriptiveComplexity.SOTCSpec.Step {L : FirstOrder.Language} (spec : SOTCSpec L) {A : Type} [L.Structure A] [LinearOrder 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.SOTCSpec.Reach {L : FirstOrder.Language} (spec : SOTCSpec L) {A : Type} [L.Structure A] [LinearOrder A] : spec.State A → spec.State A → Prop

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

Equations

• spec.Reach = Relation.ReflTransGen spec.Step

def DescriptiveComplexity.SOTCSpec.IsSrc {L : FirstOrder.Language} (spec : SOTCSpec L) {A : Type} [L.Structure A] [LinearOrder 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.SOTCSpec.IsTgt {L : FirstOrder.Language} (spec : SOTCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (ρ : spec.State A) : Prop

A state is accepting when it satisfies the target sentence.

Equations

• spec.IsTgt ρ = A ⊨ spec.tgt

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

The structure is accepted: some accepting state is reachable from some starting state.

Equations

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

Transfer along a bijection of states

Acceptance only depends on the walk up to a bijection of its states. Stated for two specifications over two vocabularies, since the pullback through an interpretation relates a specification over the base structure to one over the interpreted structure.

theorem DescriptiveComplexity.SOTCSpec.reach_map {L L' : FirstOrder.Language} {spec₁ : SOTCSpec L} {spec₂ : SOTCSpec L'} {A B : Type} [L.Structure A] [LinearOrder A] [L'.Structure B] [LinearOrder B] (e : spec₁.State A ≃ spec₂.State B) (hstep : ∀ (ρ σ : spec₁.State A), spec₁.Step ρ σ ↔ spec₂.Step (e ρ) (e σ)) {ρ σ : spec₁.State A} (h : spec₁.Reach ρ σ) : spec₂.Reach (e ρ) (e σ)

theorem DescriptiveComplexity.SOTCSpec.accepts_congr {L L' : FirstOrder.Language} {spec₁ : SOTCSpec L} {spec₂ : SOTCSpec L'} {A B : Type} [L.Structure A] [LinearOrder A] [L'.Structure B] [LinearOrder B] (e : spec₁.State A ≃ spec₂.State B) (hstep : ∀ (ρ σ : spec₁.State A), spec₁.Step ρ σ ↔ spec₂.Step (e ρ) (e σ)) (hsrc : ∀ (ρ : spec₁.State A), spec₁.IsSrc ρ ↔ spec₂.IsSrc (e ρ)) (htgt : ∀ (ρ : spec₁.State A), spec₁.IsTgt ρ ↔ spec₂.IsTgt (e ρ)) : spec₁.Accepts A ↔ spec₂.Accepts B

Acceptance transfers along a bijection of states carrying steps to steps and endpoints to endpoints.

Isomorphism-invariance

theorem DescriptiveComplexity.SOTCSpec.step_equiv {L : FirstOrder.Language} (spec : SOTCSpec L) {A A' : Type} [L.Structure A] [LinearOrder A] [L.Structure A'] [LinearOrder A'] (e : (L.sum FirstOrder.Language.order).Equiv A A') (ρ σ : spec.State A) : spec.Step ρ σ ↔ spec.Step (spec.B.mapAssign e.toEquiv ρ) (spec.B.mapAssign e.toEquiv σ)

One step is preserved by an isomorphism of the ordered expansions, the states being transported.

theorem DescriptiveComplexity.SOTCSpec.isSrc_equiv {L : FirstOrder.Language} (spec : SOTCSpec L) {A A' : Type} [L.Structure A] [LinearOrder A] [L.Structure A'] [LinearOrder A'] (e : (L.sum FirstOrder.Language.order).Equiv A A') (ρ : spec.State A) : spec.IsSrc ρ ↔ spec.IsSrc (spec.B.mapAssign e.toEquiv ρ)

Starting states are preserved by an isomorphism of the ordered expansions.

theorem DescriptiveComplexity.SOTCSpec.isTgt_equiv {L : FirstOrder.Language} (spec : SOTCSpec L) {A A' : Type} [L.Structure A] [LinearOrder A] [L.Structure A'] [LinearOrder A'] (e : (L.sum FirstOrder.Language.order).Equiv A A') (ρ : spec.State A) : spec.IsTgt ρ ↔ spec.IsTgt (spec.B.mapAssign e.toEquiv ρ)

Accepting states are preserved by an isomorphism of the ordered expansions.

theorem DescriptiveComplexity.SOTCSpec.accepts_equiv {L : FirstOrder.Language} (spec : SOTCSpec L) {A A' : Type} [L.Structure A] [LinearOrder A] [L.Structure A'] [LinearOrder A'] (e : (L.sum FirstOrder.Language.order).Equiv A A') : spec.Accepts A ↔ spec.Accepts A'

Acceptance is isomorphism-invariant (for isomorphisms of the ordered expansions, the order being visible to the sentences).

SO(TC) definability

def DescriptiveComplexity.SOTCDefinable {L : FirstOrder.Language} (P : DecisionProblem L) : Prop

A decision problem is SO(TC) definable if, on nonempty finite ordered structures, it is defined by a single transitive closure over the assignments of a second-order quantifier block: there is a DescriptiveComplexity.SOTCSpec whose accepting states are reachable from its starting states exactly on the yes-instances.

As for DescriptiveComplexity.TCDefinable and the clausal fragments, the equivalence is required for every linear order on the universe, so this is order-invariant SO(TC) definability: the problem itself does not see the order, while the three sentences may.

Equations

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

theorem DescriptiveComplexity.sotcDefinable_congr {L : FirstOrder.Language} {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : SOTCDefinable P ↔ SOTCDefinable Q

SO(TC) definability only depends on the finite instances of a problem.