We have seen that the satisfiability and validity problems for propositional logic are respectively complete for \(\textbf{NP}\) and \(\textbf{coNP}\). Although these problems are characterized in terms of the semantics for propositional logic, certain questions about its proof theory may also be addressed using techniques from complexity theory. By a proof system \(\mathcal{P}\) for propositional logic we understand a definition of the symbol \(\vdash_{\mathcal{P}}\) which characterizes what it means for a formula \(\phi\) to be derivable from a given set of axioms and rules. We write \(\vdash_{\mathcal{P}} \phi\) just in case there is a derivation \(\mathcal{D}\) (e.g. a finite tree or sequence of formulas) with \(\phi\) as its conclusion in the system \(\mathcal{P}\). Examples of such formalisms include standard definitions of Hilbert systems \(\mathcal{P}_1\),[43] natural deduction systems \(\mathcal{P}_2\), and sequent systems \(\mathcal{P}_3\) for propositional logic (see, e.g., Troelstra and Schwichtenberg 2000; Negri and Von Plato 2001). Each of these systems may be shown to be sound and complete for propositional validity – i.e. for all propositional formulas \(\phi\), \(\phi \in \sc{VALID}\) if and only if \(\vdash_{\mathcal{P}_i} \phi\) for \(i \in \{1,2,3\}\).