As a natural extension of the SAT problem, different proof systems for quantified Boolean formulas (QBF) have been proposed. Many of these extend a propositional system to handle universal quantifiers.

By formalising the construction of the QBF proof system from a propositional proof system, by the addition of the universal reduction rule (Beyersdorff, Bonacina & Chew, ITCS '16), we present a new technique for proving proof size lower bounds in these systems. This lower bound technique relies only on two semantic properties: the cost of a QBF, and the capacity of a proof. By examining the capacity of proofs in several proof systems, we are able to use this technique to obtain lower bounds in these systems based on cost alone.

As applications of this technique, we first prove exponential lower bounds for a new family of simple QBFs representing equality. The main application is in proving exponential lower bounds with high probability for a class of randomly generated QBFs, the first `genuine' lower bounds of this kind, which apply to the QBF analogues of resolution, Cutting Planes, and Polynomial Calculus.