THE PROOF IS IN THE CHECKING

Abstract

Abstract This paper investigates the question: what is a formal logical proof (in general—as opposed to: what is a formal proof in this or that specific proof system)? I begin by setting out a core conception of formal proof and substantiating its designation as ‘core’. The heart of this conception is that there must be an effective or mechanical procedure for checking the correctness of a purported proof. I then consider a proposed strengthening of this conception—one that has become standard in the literature on propositional proof complexity—according to which the proof-checking procedure must be able to be carried out in polynomial time. I discuss a variety of arguments in favour of the strengthened conception—and reject them all. My conclusion is that, when it comes to analysing the very idea of formal logical proof, we have no good reason to move to the strengthened conception and should stick with the core conception.