  In this work we investigate how to extract alternating time bounds from
'focussed' proof systems. Our main result is the obtention of fragments of
MALLw (MALL with weakening) complete for each level of the polynomial
hierarchy. In one direction we encode QBF satisfiability and in the other we
encode focussed proof search, and we show that the composition of the two
encodings preserves quantifier alternation, yielding the required result. By
carefully composing with well-known embeddings of MALLw into MALL, we obtain a
similar delineation of MALL formulas, again carving out fragments complete for
each level of the polynomial hierarchy. This refines the well-known results
that both MALLw and MALL are PSPACE-complete.
  A key insight is that we have to refine the usual presentation of focussing
to account for deterministic computations in proof search, which correspond to
invertible rules that do not branch. This is so that we may more faithfully
associate phases of focussed proof search to their alternating time complexity.
This presentation seems to uncover further dualities at the level of proof
search than usual presentations, so could be of further proof theoretic
interest in its own right.
