Alternating acceptance is `Σₖ`-definable #

The membership half of the machine bridge for the polynomial hierarchy: ATMAccept (k+1) true is Σₖ₊₁-definable, hence in Σₖ₊₁ᵖ, and ATMAccept (k+1) false is Πₖ₊₁-definable, hence in Πₖ₊₁ᵖ. The two are the same sentence at the two starting polarities.

The proof is the assembly of the four layers below it:

alternating acceptance is the k-round game (DescriptiveComplexity.ATMData.altAccepts_iff_altGame), and the game is an implication ladder (DescriptiveComplexity.ATMData.altGame_iff_altLadder), provided a start state exists – which is what DescriptiveComplexity.akStartExClause contributes to the kernel;
the ladder over walks is the ladder over the relations a block guesses (DescriptiveComplexity.ATMData.altLadder_iff_runAltLadder);
the ladder's own quantifiers are the alternating prefix over one guess per round (DescriptiveComplexity.ATMData.altBlockQuant_runMatrix), leaving the quantifier-free matrix behind;
the matrix is the kernel (DescriptiveComplexity.realize_akKernel), and the prefix is k+1 copies of one block (DescriptiveComplexity.sorealize_repBlocks).

source

theorem DescriptiveComplexity.ATMData.altAccepts_iff_start_and_altLadder {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hwf : M.WellFormed) (hbwf : M.BlocksWellFormed k) (hk : 0 < k) (start : Bool) :

M.AltAccepts start ↔ (∃ (q : A), M.Start q) ∧ M.AltLadder start k

Acceptance is the ladder, together with the existence of a start state. The second conjunct is the one existence clause the ladder cannot carry itself (see DescriptiveComplexity.Problems.Machine.AltLadder); it is first-order, so the kernel states it outright.

Dependency graph

Definability #

source

theorem DescriptiveComplexity.atmAccept_sigmaSODefinable (k : ℕ) :

SigmaSODefinable (k + 1) (ATMAccept (k + 1) true)

Alternating acceptance with an existential first block is Σₖ₊₁-definable: one block guesses the run of each round, and the first-order kernel checks the ladder.

Dependency graph

source

theorem DescriptiveComplexity.atmAccept_piSODefinable (k : ℕ) :

PiSODefinable (k + 1) (ATMAccept (k + 1) false)

Alternating acceptance with a universal first block is Πₖ₊₁-definable, by the same sentence at the other starting polarity.

Dependency graph

source

theorem DescriptiveComplexity.atmAccept_mem_sigmaP (k : ℕ) :

(SigmaP (k + 1)).Mem (ATMAccept (k + 1) true)

Alternating acceptance is in Σₖ₊₁ᵖ.

Dependency graph

source