The round game as an implication ladder

The last semantic step before the Σₖ sentence of the membership half. The game of DescriptiveComplexity.Problems.Machine.AltGame quantifies its rounds with DescriptiveComplexity.guardQ, whose universal case carries an existence clause: a universal player with no legal move loses rather than winning vacuously. Over configurations that clause is harmless, but over walks it is an existential second-order quantifier sitting inside a universal block, and a sentence built on it would not be Σₖ at all.

The clause is however redundant. A round always has a move available: follow the previous round's walk as far as it is committed, and from the entry into the round's own block run greedily – step while a step is available, stand still once stuck – which is DescriptiveComplexity.ATMData.greedyFrom. So the game can be restated with the unguarded DescriptiveComplexity.bareQ, and DescriptiveComplexity.ATMData.AltLadder is that restatement: an alternating chain of conjunctions and implications, which is exactly the shape a first-order kernel can have.

The one clause that is not redundant is at the top: round 0 has no previous walk to extend, so a legal walk exists only if an initial configuration does. That is first-order – it is ∃ q, Start q, the rest being supplied by DescriptiveComplexity.TMData.exists_isInit – and it is carried into the sentence as a plain conjunct rather than as a quantifier.

Unguarded alternation

def DescriptiveComplexity.bareQ (pol : Bool) {α : Type} (C P : α → Prop) : Prop

Quantification with a polarity, unguarded: existentially the guard is conjoined, universally it is assumed. Unlike DescriptiveComplexity.guardQ nothing here asks the guard to be satisfiable, which is what makes this shape expressible by a first-order kernel under a second-order prefix.

Equations

• DescriptiveComplexity.bareQ true C P = ∃ (a : α), C a ∧ P a
• DescriptiveComplexity.bareQ false C P = ∀ (a : α), C a → P a

The greedy continuation of a round

Every round has a move

The ladder

def DescriptiveComplexity.ATMData.gameLadder {A : Type} (M : ATMData A) (start : Bool) (i : ℕ) : ℕ → (A → Config A) → Prop

The game from round i on, unguarded: the shape a first-order kernel can express, an alternating chain of conjunctions and implications.

Equations

• One or more equations did not get rendered due to their size.
• M.gameLadder start i 0 x✝ = M.AccAt x✝

def DescriptiveComplexity.ATMData.AltLadder {A : Type} (M : ATMData A) (start : Bool) : ℕ → Prop

The whole k-round ladder, with the first round peeled off as in DescriptiveComplexity.ATMData.AltGame.

Equations

• One or more equations did not get rendered due to their size.
• M.AltLadder start 0 = False

theorem DescriptiveComplexity.ATMData.altGame_iff_altLadder {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) (hinit : ∃ (c₀ : Config A), M.IsInit c₀) (start : Bool) : M.AltGame start k ↔ M.AltLadder start k

The whole game is the whole ladder. The hypothesis is the one existence clause that is not redundant: round 0 extends no previous walk, so it needs an initial configuration to exist.