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.

theorem DescriptiveComplexity.SOGameSpec.preOneLHom_isExpansionOn {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p : Phase) (ρ : B.Assignment A) (σ : M.Assignment A) : (preOneLHom L B M).IsExpansionOn A

theorem DescriptiveComplexity.SOGameSpec.realize_preOne {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p : Phase) (ρ : B.Assignment A) (σ : M.Assignment A) (ψ : (((L.sum B.lang).sum FirstOrder.Language.order).sum M.lang).Sentence) : A ⊨ (preOneLHom L B M).onSentence ψ ↔ A ⊨ ψ

theorem DescriptiveComplexity.SOGameSpec.preSndLHom_isExpansionOn {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : Phase) (ρ ρ' : B.Assignment A) (σ σ' : M.Assignment A) : (preSndLHom L B M).IsExpansionOn A

theorem DescriptiveComplexity.SOGameSpec.realize_preSnd {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : Phase) (ρ ρ' : B.Assignment A) (σ σ' : M.Assignment A) (ψ : (((L.sum B.lang).sum FirstOrder.Language.order).sum M.lang).Sentence) : A ⊨ (preSndLHom L B M).onSentence ψ ↔ A ⊨ ψ

theorem DescriptiveComplexity.SOGameSpec.preTwoLHom_isExpansionOn {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : Phase) (ρ ρ' : B.Assignment A) (σ σ' : M.Assignment A) : (preTwoLHom L B M).IsExpansionOn A

theorem DescriptiveComplexity.SOGameSpec.realize_preTwo {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : Phase) (ρ ρ' : B.Assignment A) (σ σ' : M.Assignment A) (ψ : ((((L.sum B.lang).sum FirstOrder.Language.order).sum M.lang).sum M.lang).Sentence) : A ⊨ (preTwoLHom L B M).onSentence ψ ↔ A ⊨ ψ

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)

theorem DescriptiveComplexity.SOGameSpec.realize_phaseF {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : Phase) (ρ : B.Assignment A) (σ : M.Assignment A) : A ⊨ phaseF L B M p ↔ p = q

theorem DescriptiveComplexity.SOGameSpec.realize_atPhaseF {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : Phase) (ρ : B.Assignment A) (σ : M.Assignment A) : A ⊨ atPhaseF L B M p ↔ p = q

theorem DescriptiveComplexity.SOGameSpec.exists_preAssign {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (τ : (preBlock B M).Assignment A) (h : A ⊨ (B.cons M).tagGuardF Phase) : ∃ (p : Phase) (ρ : B.Assignment A) (σ : M.Assignment A), τ = preAssign p ρ σ

A well-formed state: one whose tag bits name a phase.

theorem DescriptiveComplexity.SOGameSpec.tagArg_subsingleton {B M : SOBlock} {A : Type} {r : Phase} (y z : Fin ((preBlock B M).arity (Sum.inl r)) → A) : y = z

The argument tuple of a tag variable is the empty one, whatever it is.

theorem DescriptiveComplexity.SOGameSpec.realize_phaseTwoF' {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (r : Phase) (τ τ' : (preBlock B M).Assignment A) (x : Fin ((preBlock B M).arity (Sum.inl r)) → A) : A ⊨ phaseTwoF L B M r ↔ τ' (Sum.inl r) x

The tag bit of the second copy, read at an arbitrary state.

theorem DescriptiveComplexity.SOGameSpec.realize_phaseTwoF {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : Phase) (τ : (preBlock B M).Assignment A) (ρ' : B.Assignment A) (σ' : M.Assignment A) : A ⊨ phaseTwoF L B M p ↔ p = q

theorem DescriptiveComplexity.SOGameSpec.realize_atPhaseTwoF {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : Phase) (τ : (preBlock B M).Assignment A) (ρ' : B.Assignment A) (σ' : M.Assignment A) : A ⊨ atPhaseTwoF L B M p ↔ p = q

theorem DescriptiveComplexity.SOGameSpec.exists_preAssign_two {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p : Phase) (τ τ' : (preBlock B M).Assignment A) (h : A ⊨ atPhaseTwoF L B M p) : ∃ (ρ' : B.Assignment A) (σ' : M.Assignment A), τ' = preAssign p ρ' σ'

The guarded phase of the second copy pins its shape: a move that asserts it lands on a well-formed state.

Freezing, read

theorem DescriptiveComplexity.SOGameSpec.realize_frozenAtS {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : Phase) (ρ ρ' : B.Assignment A) (σ σ' : M.Assignment A) (i : B.ι) : A ⊨ frozenAtS L B M i ↔ ∀ (x : Fin (B.arity i) → A), ρ i x ↔ ρ' i x

theorem DescriptiveComplexity.SOGameSpec.realize_frozenS {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : Phase) (ρ ρ' : B.Assignment A) (σ σ' : M.Assignment A) : A ⊨ frozenS L B M ↔ ρ = ρ'

The prefixed game

theorem DescriptiveComplexity.SOGameSpec.realize_sumInl_two {L : FirstOrder.Language} {B M : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] (τ τ' : (preBlock B M).Assignment A) (ψ : ((L.sum FirstOrder.Language.order).sum (preBlock B M).lang).Sentence) : A ⊨ FirstOrder.Language.LHom.sumInl.onSentence ψ ↔ A ⊨ ψ

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.

theorem DescriptiveComplexity.SOGameSpec.exBlock_isStart {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} (p : Phase) (ρ : B.Assignment A) (σ : spec.State A) : (exBlock L B pol spec).IsStart (preAssign p ρ σ) ↔ p = Phase.pick

theorem DescriptiveComplexity.SOGameSpec.exBlock_isWon {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} (p : Phase) (ρ : B.Assignment A) (σ : spec.State A) : (exBlock L B pol spec).IsWon (preAssign p ρ σ) ↔ p = Phase.play ∧ spec.IsWon σ

theorem DescriptiveComplexity.SOGameSpec.exBlock_isUniv {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} (p : Phase) (ρ : B.Assignment A) (σ : spec.State A) : (exBlock L B pol spec).IsUniv (preAssign p ρ σ) ↔ p = Phase.pick ∧ pol = false ∨ p = Phase.play ∧ spec.IsUniv σ

theorem DescriptiveComplexity.SOGameSpec.exBlock_move {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} (p q : Phase) (ρ ρ' : B.Assignment A) (σ σ' : spec.State A) : (exBlock L B pol spec).Move (preAssign p ρ σ) (preAssign q ρ' σ') ↔ p = Phase.pick ∧ q = Phase.start ∨ (p = Phase.start ∧ q = Phase.play) ∧ ρ = ρ' ∧ spec.IsStart σ' ∨ (p = Phase.play ∧ q = Phase.play) ∧ ρ = ρ' ∧ spec.Move σ σ'

theorem DescriptiveComplexity.SOGameSpec.exBlock_move_shape {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} {τ τ' : (preBlock B spec.B).Assignment A} (h : (exBlock L B pol spec).Move τ τ') : ∃ (q : Phase) (ρ' : B.Assignment A) (σ' : spec.State A), τ' = preAssign q ρ' σ'

Every move lands on a well-formed state: each disjunct guards the tag bits of the state it enters.

What the prefixed game wins

theorem DescriptiveComplexity.SOGameSpec.inner_wins_of_wins {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} {τ : (exBlock L B pol spec).State A} (h : (exBlock L B pol spec).Wins τ) {ρ : B.Assignment A} {σ : spec.State A} (hτ : τ = preAssign Phase.play ρ σ) : spec.Wins σ

The playing phase plays the inner game, from a win of the prefixed game back to one of the inner one.

theorem DescriptiveComplexity.SOGameSpec.wins_play_of_inner {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} (ρ : B.Assignment A) {σ : spec.State A} (h : spec.Wins σ) : (exBlock L B pol spec).Wins (preAssign Phase.play ρ σ)

The playing phase plays the inner game, from a win of the inner game to one of the prefixed game.

theorem DescriptiveComplexity.SOGameSpec.wins_play_iff {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} (ρ : B.Assignment A) (σ : spec.State A) : (exBlock L B pol spec).Wins (preAssign Phase.play ρ σ) ↔ spec.Wins σ

theorem DescriptiveComplexity.SOGameSpec.accepts_of_wins_start {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} {τ : (exBlock L B pol spec).State A} (h : (exBlock L B pol spec).Wins τ) {ρ : B.Assignment A} {σ : spec.State A} (hτ : τ = preAssign Phase.start ρ σ) : spec.Accepts A

The starting phase chooses a starting state of the inner game: it is existential, and it is stuck exactly when the inner game has no starting state.

theorem DescriptiveComplexity.SOGameSpec.wins_start_iff {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} (ρ : B.Assignment A) (σ : spec.State A) : (exBlock L B pol spec).Wins (preAssign Phase.start ρ σ) ↔ spec.Accepts A

theorem DescriptiveComplexity.SOGameSpec.quantB_accepts_of_wins_pick {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} {τ : (exBlock L B pol spec).State A} (h : (exBlock L B pol spec).Wins τ) {ρ : B.Assignment A} {σ : spec.State A} (hτ : τ = preAssign Phase.pick ρ σ) : quantB pol fun (ρ₀ : B.Assignment A) => spec.Accepts A

The picking phase quantifies the block, existentially or universally as the polarity says.

theorem DescriptiveComplexity.SOGameSpec.wins_pick_iff {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} (ρ : B.Assignment A) (σ : spec.State A) : (exBlock L B pol spec).Wins (preAssign Phase.pick ρ σ) ↔ quantB pol fun (ρ₀ : B.Assignment A) => spec.Accepts A

theorem DescriptiveComplexity.SOGameSpec.exBlock_accepts_iff {L : FirstOrder.Language} {B : SOBlock} {A : Type} [instL : L.Structure A] [LinearOrder A] {pol : Bool} {spec : SOGameSpec (L.sum B.lang)} : (exBlock L B pol spec).Accepts A ↔ quantB pol fun (ρ₀ : B.Assignment A) => spec.Accepts A

What a prefixed game accepts: what the inner game accepts, under the quantified block.

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.

theorem DescriptiveComplexity.SOGameSpec.realize_kernel_won {L : FirstOrder.Language} {A : Type} [instL : L.Structure A] [LinearOrder A] (φ : L.Sentence) (τ : SOBlock.trivial.Assignment A) : (kernelGame L φ).IsWon τ ↔ A ⊨ φ

theorem DescriptiveComplexity.SOGameSpec.wins_kernel_iff {L : FirstOrder.Language} {A : Type} [instL : L.Structure A] [LinearOrder A] (φ : L.Sentence) (τ : (kernelGame L φ).State A) : (kernelGame L φ).Wins τ ↔ A ⊨ φ

theorem DescriptiveComplexity.SOGameSpec.accepts_kernelGame {L : FirstOrder.Language} {A : Type} [instL : L.Structure A] [LinearOrder A] (φ : L.Sentence) : (kernelGame L φ).Accepts A ↔ A ⊨ φ

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_sigmaP {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} {k : ℕ} (h : (SigmaP k).Mem P) : SOGameDefinable P

Every level of the polynomial hierarchy is a second-order alternating game. Level 0 goes through PTIME ⊆ NP, the other levels are the definition of DescriptiveComplexity.SigmaP read through DescriptiveComplexity.SigmaSODefinable.soGameDefinable.

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

theorem DescriptiveComplexity.ExpExpansion.soGameDefinable_of_fo_on_expansion {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (φ : (X.E.sum FirstOrder.Language.order).Sentence) (Q : DecisionProblem L) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [inst_2 : Finite A] [inst_3 : Nonempty A], Q.Holds A ↔ X.Map A ⊨ φ) : SOGameDefinable Q

A first-order property of an exponential expansion is a second-order alternating game: its quantifiers become second-order blocks over the base (DescriptiveComplexity.ExpExpansion.exists_translate) and the blocks become moves. This is the game reading of DescriptiveComplexity.ExpExpansion.mem_PH_of_fo_on_expansion, and it is what a guard of a fixed-point rule over an expansion will be evaluated by.