A second-order quantifier prefix, played as a game

The theorem: every second-order sentence – an alternating prefix of block quantifiers over a first-order kernel – defines a second-order alternating game (DescriptiveComplexity.SOGameSpec.accepts_gameOfSO), whence DescriptiveComplexity.SigmaSODefinable.soGameDefinable and SO ⊆ SO-GAME.

It is the game counterpart of DescriptiveComplexity.sotcDefinable_soProblem, which peels the same prefix into the state of a walk. A walk can only guess, so a universal block has to be complemented away there; a game has universal moves, so the prefix is peeled one block at a time with no complementation (DescriptiveComplexity.SOGameSpec.exBlock).

The construction

DescriptiveComplexity.SOGameSpec.exBlock prefixes a game with one quantified block. Its states are the assignments of SOBlock.cons B spec.B extended by a phase (DescriptiveComplexity.SOGameSpec.Phase, three arity-0 tag bits, as DescriptiveComplexity.SOBlock.withTag supplies them):

• pick – the quantified block is chosen, by the existential or the universal player according to the polarity;
• start – the existential player chooses a starting state of the inner game. This phase is always existential and it is what a stuck position means: a specification with no starting state loses here, which is exactly DescriptiveComplexity.SOGameSpec.Accepts being false;
• play – the inner game is played, the chosen block frozen by every move (DescriptiveComplexity.SOGameSpec.frozenS).

Splitting pick from start is what makes the universal case correct: were the choice of a starting state folded into a universal pick move, a block assignment admitting no starting state would contribute no move at all and so be silently skipped by the universal clause of DescriptiveComplexity.SOGameSpec.Wins, instead of refuting it.

The phases

inductive DescriptiveComplexity.SOGameSpec.Phase : Type

The three phases of a prefixed game.

• pick : Phase

  The quantified block is being chosen.

• start : Phase

  A starting state of the inner game is being chosen.

• play : Phase

  The inner game is being played.

@[instance_reducible]

instance DescriptiveComplexity.SOGameSpec.instDecidableEqPhase : DecidableEq Phase

Equations

• DescriptiveComplexity.SOGameSpec.instDecidableEqPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.SOGameSpec.instFintypePhase : Fintype Phase

Equations

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

The state block

@[reducible, inline]

abbrev DescriptiveComplexity.SOGameSpec.preBlock (B M : SOBlock) : SOBlock

The states of a prefixed game: an assignment of the quantified block, one of the inner game's block, and a phase.

Equations

• DescriptiveComplexity.SOGameSpec.preBlock B M = (B.cons M).withTag DescriptiveComplexity.SOGameSpec.Phase

def DescriptiveComplexity.SOGameSpec.preAssign {B M : SOBlock} {A : Type} (p : Phase) (ρ : B.Assignment A) (σ : M.Assignment A) : (preBlock B M).Assignment A

The state of a prefixed game at a phase, a chosen block and an inner state.

Equations

• DescriptiveComplexity.SOGameSpec.preAssign p ρ σ = DescriptiveComplexity.SOBlock.tagAssign p (DescriptiveComplexity.consAssign ρ σ)

@[simp]

theorem DescriptiveComplexity.SOGameSpec.dropTag_preAssign {B M : SOBlock} {A : Type} (p : Phase) (ρ : B.Assignment A) (σ : M.Assignment A) : SOBlock.dropTag (preAssign p ρ σ) = consAssign ρ σ

Reading the inner game's sentences

def DescriptiveComplexity.SOGameSpec.preOneLHom (L : FirstOrder.Language) (B M : SOBlock) : ((L.sum B.lang).sum FirstOrder.Language.order).sum M.lang →ᴸ (L.sum FirstOrder.Language.order).sum (preBlock B M).lang

The inner game's one-copy vocabulary, read in a prefixed state: the quantified block and the inner block land in their components.

Equations

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

def DescriptiveComplexity.SOGameSpec.preSndLHom (L : FirstOrder.Language) (B M : SOBlock) : ((L.sum B.lang).sum FirstOrder.Language.order).sum M.lang →ᴸ ((L.sum FirstOrder.Language.order).sum (preBlock B M).lang).sum (preBlock B M).lang

The inner game's one-copy vocabulary, read in the second copy of a prefixed state – what the move into the playing phase needs, the inner game's starting condition being about the state the move enters.

Equations

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

def DescriptiveComplexity.SOGameSpec.preTwoLHom (L : FirstOrder.Language) (B M : SOBlock) : (((L.sum B.lang).sum FirstOrder.Language.order).sum M.lang).sum M.lang →ᴸ ((L.sum FirstOrder.Language.order).sum (preBlock B M).lang).sum (preBlock B M).lang

The inner game's two-copy vocabulary, read in a prefixed move: the quantified block is read in the first copy, which every move freezes.

Equations

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

The phase, and freezing the quantified block

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.SOGameSpec.phaseF (L : FirstOrder.Language) (B M : SOBlock) (p : Phase) : ((L.sum FirstOrder.Language.order).sum (preBlock B M).lang).Sentence

The tag bit of a phase, in a one-copy state.

Equations

• DescriptiveComplexity.SOGameSpec.phaseF L B M p = (B.cons M).tagBitF DescriptiveComplexity.SOGameSpec.Phase p

noncomputable def DescriptiveComplexity.SOGameSpec.atPhaseF (L : FirstOrder.Language) (B M : SOBlock) (p : Phase) : ((L.sum FirstOrder.Language.order).sum (preBlock B M).lang).Sentence

The state is a well-formed one at the phase p.

Equations

• DescriptiveComplexity.SOGameSpec.atPhaseF L B M p = (B.cons M).tagGuardF DescriptiveComplexity.SOGameSpec.Phase ⊓ DescriptiveComplexity.SOGameSpec.phaseF L B M p

noncomputable def DescriptiveComplexity.SOGameSpec.phaseTwoF (L : FirstOrder.Language) (B M : SOBlock) (p : Phase) : (((L.sum FirstOrder.Language.order).sum (preBlock B M).lang).sum (preBlock B M).lang).Sentence

The tag bit of a phase, in the second copy of a two-copy state.

Equations

• DescriptiveComplexity.SOGameSpec.phaseTwoF L B M p = FirstOrder.Language.Relations.formula (Sum.inr ⟨Sum.inl p, ⋯⟩) Fin.elim0

noncomputable def DescriptiveComplexity.SOGameSpec.atPhaseTwoF (L : FirstOrder.Language) (B M : SOBlock) (p : Phase) : (((L.sum FirstOrder.Language.order).sum (preBlock B M).lang).sum (preBlock B M).lang).Sentence

The second copy is a well-formed state at the phase p: its bit is set and every other is not.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.SOGameSpec.preFstSym (L : FirstOrder.Language) (B M : SOBlock) (i : B.ι) : (((L.sum FirstOrder.Language.order).sum (preBlock B M).lang).sum (preBlock B M).lang).Relations (B.arity i)

The relation variable i of the quantified block, in the first copy.

Equations

• DescriptiveComplexity.SOGameSpec.preFstSym L B M i = Sum.inl (Sum.inr ⟨Sum.inr (Sum.inl i), ⋯⟩)

@[reducible, inline]

abbrev DescriptiveComplexity.SOGameSpec.preSndSym (L : FirstOrder.Language) (B M : SOBlock) (i : B.ι) : (((L.sum FirstOrder.Language.order).sum (preBlock B M).lang).sum (preBlock B M).lang).Relations (B.arity i)

The relation variable i of the quantified block, in the second copy.

Equations

• DescriptiveComplexity.SOGameSpec.preSndSym L B M i = Sum.inr ⟨Sum.inr (Sum.inl i), ⋯⟩

noncomputable def DescriptiveComplexity.SOGameSpec.frozenAtS (L : FirstOrder.Language) (B M : SOBlock) (i : B.ι) : (((L.sum FirstOrder.Language.order).sum (preBlock B M).lang).sum (preBlock B M).lang).Sentence

The quantified block's variable i is unchanged by the move.

Equations

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

noncomputable def DescriptiveComplexity.SOGameSpec.frozenS (L : FirstOrder.Language) (B M : SOBlock) : (((L.sum FirstOrder.Language.order).sum (preBlock B M).lang).sum (preBlock B M).lang).Sentence

The quantified block is frozen: every move of the playing phase leaves it alone.

Equations

• DescriptiveComplexity.SOGameSpec.frozenS L B M = DescriptiveComplexity.listInf (List.map (DescriptiveComplexity.SOGameSpec.frozenAtS L B M) Finset.univ.toList)

Freezing, read

The prefixed game

noncomputable def DescriptiveComplexity.SOGameSpec.exBlock (L : FirstOrder.Language) (B : SOBlock) (pol : Bool) (spec : SOGameSpec (L.sum B.lang)) : SOGameSpec L

A game, prefixed with one quantified block: the block is chosen at the phase pick by the player the polarity names, a starting state of the inner game at the phase start, and the inner game is played from there with the block frozen.

Equations

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

What the prefixed game wins

The kernel, as a game with no move

noncomputable def DescriptiveComplexity.SOGameSpec.kernelGame (L : FirstOrder.Language) (φ : L.Sentence) : SOGameSpec L

The game that decides a first-order sentence: no move, and the sentence decides the only position.

Equations

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

The prefix, peeled one block at a time

noncomputable def DescriptiveComplexity.SOGameSpec.gameOfSO (Bs : List SOBlock) (L : FirstOrder.Language) : (soLang L Bs).Sentence → Bool → SOGameSpec L

The game a second-order sentence defines: one quantified block per block of the prefix, and the kernel at the end.

Equations

• DescriptiveComplexity.SOGameSpec.gameOfSO [] x✝² x✝ x✝¹ = DescriptiveComplexity.SOGameSpec.kernelGame x✝² x✝
• DescriptiveComplexity.SOGameSpec.gameOfSO (B :: Bs) x✝² x✝ x✝¹ = DescriptiveComplexity.SOGameSpec.exBlock x✝² B x✝¹ (DescriptiveComplexity.SOGameSpec.gameOfSO Bs (x✝².sum B.lang) x✝ !x✝¹)

theorem DescriptiveComplexity.SOGameSpec.accepts_gameOfSO (Bs : List SOBlock) (L : FirstOrder.Language) (A : Type) (instL : L.Structure A) [LinearOrder A] (φ : (soLang L Bs).Sentence) (pol : Bool) : (gameOfSO Bs L φ pol).Accepts A ↔ SORealize L A Bs φ pol

A second-order sentence is a second-order alternating game.

SO ⊆ SO-GAME

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

Every Σₖ-definable problem is a second-order alternating game.

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

Every Πₖ-definable problem is a second-order alternating game.

theorem DescriptiveComplexity.SOGameDefinable.of_mem_PH {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : PH.Mem P) : SOGameDefinable P

PH ⊆ SO-GAME: every problem of the polynomial hierarchy is the value of a second-order alternating game. Read with DescriptiveComplexity.SOGameDefinable.mem_EXPTIME it re-proves PH ⊆ EXPTIME, this time through a game rather than through PSPACE.

A first-order property of an expansion