 Such a system is said to be polynomially bounded if there exists a polynomial \(p(n)\) such that for all \(\phi \in \sc{VALID}\), there is a derivation \(\mathcal{D}\) such that \(\mathcal{P}(\ulcorner \mathcal{D} \urcorner) = \phi\) and \(\lvert \ulcorner \mathcal{D}\urcorner \rvert \leq p(\lvert \phi \rvert)\) – i.e. just in case all tautologies of size \(n\) possess \(\mathcal{P}\)-proofs of size at most \(p(n)\).