# From QBFs to MALL and back via focussing: fragments of multiplicative additive linear logic for each level of the polynomial hierarchy

## TL;DR

This paper establishes a correspondence between fragments of multiplicative additive linear logic and each level of the polynomial hierarchy by leveraging focussed proof systems and encoding techniques.

## Contribution

It introduces a method to extract polynomial hierarchy levels from focussed proof systems, refining the understanding of MALL and MALLw complexity.

## Key findings

- Fragments of MALLw complete for each polynomial hierarchy level
- Encoding QBF satisfiability within focussed proof systems
- Refined focussing to account for deterministic proof search phases

## Abstract

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.