ABSTRACT. We investigate how to extract alternating time bounds from focussed proofs, treating synchronous phases as nondeterministic computation and asynchronous phases as co-nondeterministic computation. We refine the usual presentation of focussing to account for deterministic computations in proof search, which correspond to invertible rules that do not branch, more faithfully associating phases of focussed proof search to their alternating time complexity.

As our main result, we give a focussed system for affine MALL and give encodings to and from true quantified Boolean formulas (QBFs): in one direction we encode QBF satisfiability and in the other we encode focussed proof search. Moreover we show that the composition of the two encodings preserves quantifier alternation, hence yielding fragments of affine MALL complete for each level of the polynomial hierarchy. This refines the well-known result that affine MALL is PSPACE-complete.