The Meaning of the Conjecture P � NP for Mathematical Logic
Jan Mycielski · American Mathematical Monthly · 1983
I think that the conjecture P + NP is not as widely taught in courses of mathematical logic as it should be, in view of its capital importance for the foundation of mathematics. Therefore I am writing this note in the hope that all logicians will always include it in the introductory courses of their subject although it does not appear yet in the appropriate books. The original paper of S. Cook [1], where the conjecture was formulated, was indeed written from the point of view of logic but it became the domain of computer scientists (see [2]), particularly because of a paper of Karp [3] where the combinatorial or computational aspects of the conjecture were developed in a very suggestive way. Let us assume that the teacher has already presented the concept of a first order theory and the concept of a Turing machine (neither the concepts of a decidable theory nor that of a recursive function are needed). Then he may proceed as follows: By a normal theory we shall mean a theory which is formalized with a finite alphabet in first order logic with equality and is axiomatizable by a finite set of axioms and axiom schemata in which one can prove 3xy [ x + y ]. (In [4] it is proved that every theory which is recursively axiomatizable and contains a minimal amount of arithmetic or set theory is normal.) By a proof in a normal theory we mean a Hilbert style proof from the axioms. Let E be a finite alphabet and E* the set of all words, i.e., finite sequences of elements of E. For any E*, I denotes the length of (. Now we introduce a more abstract concept of a theory which we will call a T7T-theory. A T7T-theory is a set of pairs T c E* x E* such that there exists a polynomial P(x, y) and a Turing machine M such that, for any (T, 1) E E* x E*, M can decide in time < P(ITI, I7TI) if (T, 7T) E T. If (i, 7T) E T, thenT is called a theorem of T and 7 is called a proof of i-in T. Every normal theory defines a Tg-theory since the time necessary to check the correctness of a Hilbert style proof in a normal theory can be estimated from above by a polynomial in the length of that proof. Now, a T7n-theory T will be called amenable (to automatization) iff there exists another polynomial Po(x, y) and another Turing machine Mo such that, given any word XE * and any positive integer n, MO can decide in time < Po(ITi-, n) if there exists a X E =* with Ig I < n and such that (i, s) E T. (Notice that if we replaced the condition < Po(iTI, n) by the condition < Po(ITI, Cn) where c = card E, then the concept would trivialize since every T7T-theory would be amenable. In fact, given a time Po(lTI, cn), the machine can form all sequences of symbols of length n and find out if any of them is a proof of i.) It is clear that, after Godel's 1931 discovery that all sufficiently strong theories are undecidable,