The results summarized in Sections   4.2 and   4.3 underscore just how severe these problems are. Note first that the problem of deciding whether a given formula is a tautology is \(\textbf{coNP}\)-complete, and hence very likely to be intractable. But we have also seen that results from proof complexity strongly suggest that any proof system which an agent is likely to adopt for reasoning about propositional logic (e.g. natural deduction) will be such that there are infinitely many statements whose simplest proofs are of length at least exponential relative to their size. It is thus likely that there will exist ‘short’ tautologies – e.g. with fewer than 100 propositional letters – whose shortest proof in a conventional natural deduction system will be astronomically long. Similar remarks apply to the problem of determining whether a finite set of sentences \(\{\psi_1, \ldots, \psi_n\}\) is consistent – a task which is surely of epistemic import in everyday reasoning. In particular, it is readily seen that consistency checking is simply a re-description of the canonical \(\textbf{NP}\)-complete problem \(\sc{SAT}\).