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_n\) each of whose members is either a logical axiom or follows from earlier members by modus ponens.  A finite sequence of formulas  can be encoded as a binary string so that it is may be recognized in polynomial time if  \(x \in \{0,1\}^*\) is the code of a well-formed proof.  \( \mathcal{P}\) can now be defined so if \( x\) encodes such a derivation, then \( \mathcal{P}(x) = \psi_n \) (i.e. the conclusion of the derivation) and \( \mathcal{P}(x)\) is some fixed tautology otherwise.