The problem of computing whether any formula in propositional logic is satisfiable is not in P . Therefore, P is not equal to NP . In the first- order theory B, axiomatizing Turing’s theory of computing, three versions of the proofs are presented. First, an informal (conceptual) proof about formal proofs. Second, a more formal proof in Hilbert’s proof theory. Third, a formal proof in Hilbert’s proof theory, using a theorem prover.