We revisit the semantic size-cost-capacity technique (Beyersdorff, Blinkhorn & Hinde, 2019) for proof-size lower bounds in proof systems for quantified Boolean formulas (QBF). While the original technique is only applicable to weak proof systems with bounded capacity, we present a fine-grained generalisation of this technique that allows us to attack stronger systems with unbounded capacity. Both the technique and the relevant QBF proof systems are defined semantically and are parametrised by the proof lines permitted in the system.

We demonstrate our approach on the Q-$k$-DNF systems - allowing for $k$-DNFs as lines and forming a QBF analogue of the propositional Res($k$) proof systems (Krajiacek, 2001) - and show that the Q-$k$-DNF hierarchy is strict with exponential separations between all levels, using our refined size-cost-capacity technique.