EXPTIME is second-order alternating reachability

The theorem: DescriptiveComplexity.exptime_eq_soGame –

P ∈ EXPTIME ↔ SOGameDefinable P,

the deterministic exponential class is the value of a second-order alternating game. One direction is DescriptiveComplexity.SOGameDefinable.mem_EXPTIME, the second-order shadow of GAME ∈ PTIME; the other is DescriptiveComplexity.SOLFPDefinable.soGameDefinable, assembled here, and it is Chandra–Kozen–Stockmeyer's half of APSPACE = EXPTIME (Chandra–Kozen–Stockmeyer 1981) with the machine removed.

How the pieces meet

SOLFPDefinable P is ExpDefinable PTIME P (DescriptiveComplexity.solfpDefinable_iff_expDefinable), so P A is a PTIME property of an exponential expansion X.Map A; DescriptiveComplexity.GAME is PTIME-hard under ordinary ordered reductions (DescriptiveComplexity.game_hard_ordered), so that property is GameWon of the AND/OR graph an interpretation I draws on the expanded universe. Its four defining relations are first-order over the expansion, hence alternating block prefixes over the base (DescriptiveComplexity.ExpExpansion.exists_translate), and a prefix is a sequence of moves. DescriptiveComplexity.ExpExpansion.graphGame plays that graph:

• DescriptiveComplexity.ExpExpansion.wins_pre – the prefix phases evaluate the six questions;
• DescriptiveComplexity.ExpExpansion.target_of_wins and DescriptiveComplexity.ExpExpansion.wins_of_winsOn – the node phases play the graph;
• DescriptiveComplexity.ExpExpansion.graphGame_accepts_iff – putting them together at the starting phase.

The one thing that never happens is a sentence over the base that quantifies a point: a quantifier over the expanded universe is a second-order block over the base, never a first-order one. That is the obstruction the whole design works around, and it works around it by the observation that it does not apply to a move.

theorem DescriptiveComplexity.ExpExpansion.graphGame_accepts_iff {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {d n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (hdn : 2 * d ≤ n) {hn : n = 2 * d + Dm} {D : Sub → T → T → ℕ} {hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm} {K : Sub → T → T → ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence} (hK : ∀ (s : Sub) (tx ty : T), KernelSpec I hdn (n - D s tx ty) (D s tx ty) s tx ty (K s tx ty)) : (X.graphGame hn D hD K).Accepts A ↔ GameWon (I.Map (X.Map A))

The graph game accepts exactly when the interpreted graph is won.

EXPTIME ⊆ SO-GAME

theorem DescriptiveComplexity.SOLFPDefinable.soGameDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : SOLFPDefinable P) : SOGameDefinable P

A second-order least fixed point is a second-order alternating game. The converse of DescriptiveComplexity.SOGameDefinable.mem_EXPTIME, and the half of Chandra–Kozen–Stockmeyer that has content.

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

EXPTIME is second-order alternating reachability: the deterministic exponential class is exactly the class of second-order alternating games. Read on the definitions this is SO(≤, LFP) = SO-GAME; read on the machines it is Chandra–Kozen–Stockmeyer's APSPACE = EXPTIME, with the machine replaced by the game it plays.