The current consensus in proof complexity, assuming NP is not equal to co-NP, is that polynomial proof systems do not exist

for all propositional formulas \(\phi\), \(\phi \in \sc{VALID}\) if and only if \(\vdash_{\mathcal{P}_i} \phi\) for \(i \in \{1,2,3\}\). In the context of complexity theory, it is convenient to reformulate the definition of a proof system as a mapping \(\mathcal{P}: \{0,1\}^* \rightarrow \sc{VALID}\) whose domain consist of all binary string and whose range is the class of all valid formulas. Recall, for instance, that a Hilbert derivation is a finite sequences of formulas \(\psi_1,\ldots,\psi_