The matrix of the ladder

The ladder of DescriptiveComplexity.Problems.Machine.AltLadder alternates its own quantifiers; a Σₖ sentence puts the alternation in the prefix and leaves a quantifier-free chain behind. This file is that reshuffling, at the level of the semantics: DescriptiveComplexity.ATMData.runMatrix is the ladder with its quantifiers stripped – a conjunction where the round is existential, an implication where it is universal (DescriptiveComplexity.polConn) – read at a family of assignments, one per round, and DescriptiveComplexity.ATMData.altBlockQuant_runMatrix puts the quantifiers back as the alternating prefix DescriptiveComplexity.altBlockQuant.

The two lemmas that make it work pull a condition on the round already chosen out of the quantifiers over the rounds still to come (DescriptiveComplexity.altBlockQuant_and_left and DescriptiveComplexity.altBlockQuant_imp_left); both need the assignments to form a nonempty type, which they do – the empty relation is one.

Pulling a condition out of the prefix

def DescriptiveComplexity.polConn (pol : Bool) (X Y : Prop) : Prop

The connective a round of the ladder uses: a conjunction where the round is existential, an implication where it is universal.

Equations

• DescriptiveComplexity.polConn true X Y = (X ∧ Y)
• DescriptiveComplexity.polConn false X Y = (X → Y)

theorem DescriptiveComplexity.altBlockQuant_and_left {A : Type} {B : SOBlock} (ρ₀ : B.Assignment A) (m : ℕ) (F : Prop) (P : (Fin m → B.Assignment A) → Prop) (pol : Bool) : altBlockQuant A B m (fun (ρs : Fin m → B.Assignment A) => F ∧ P ρs) pol ↔ F ∧ altBlockQuant A B m P pol

A conjunct that does not mention the quantified rounds comes out of the prefix.

theorem DescriptiveComplexity.altBlockQuant_imp_left {A : Type} {B : SOBlock} (ρ₀ : B.Assignment A) (m : ℕ) (F : Prop) (P : (Fin m → B.Assignment A) → Prop) (pol : Bool) : altBlockQuant A B m (fun (ρs : Fin m → B.Assignment A) => F → P ρs) pol ↔ F → altBlockQuant A B m P pol

A hypothesis that does not mention the quantified rounds comes out of the prefix.

The matrix

def DescriptiveComplexity.ATMData.RunGuard {A : Type} (M : ATMData A) (i : ℕ) (prev : Option (tmGuessBlock.Assignment A)) (ρ : tmGuessBlock.Assignment A) : Prop

The condition round i puts on its guess, with the round before it – or nothing at all, at the first round, which only has to be legal.

Equations

• M.RunGuard i none ρ = M.RunLegalBelow ρ 1
• M.RunGuard i (some ρp) ρ = M.RunRoundCond ρp ρ i

def DescriptiveComplexity.ATMData.runMatrix {A : Type} (M : ATMData A) (start : Bool) (m _i : ℕ) : Option (tmGuessBlock.Assignment A) → (Fin m → tmGuessBlock.Assignment A) → Prop

The ladder with its quantifiers stripped. runMatrix M start m i prev ρs is the chain of the m rounds still to play, starting at round i with prev the round before it – none at the very first round, which has nothing to inherit. When no round is left the last guess must accept.

Equations

• One or more equations did not get rendered due to their size.
• M.runMatrix start 0 x✝ none x_5 = False
• M.runMatrix start 0 x✝ (some ρp) x_5 = M.RunAccAt ρp

theorem DescriptiveComplexity.ATMData.altBlockQuant_runMatrix {A : Type} {M : ATMData A} {start : Bool} (n : ℕ) : altBlockQuant A tmGuessBlock n (M.runMatrix start n 0 none) start ↔ M.RunAltLadder start n

The prefix puts the rounds back, at the first round: the alternating second-order prefix over one guess per round says exactly what the ladder does.