ABSTRACT
Consider some of the philosophical answers to the question put in the title of this paper. One answer, common especially to some logicians, is that a proof is a finite configuration of signs in an inductively defined class of sign configurations of an elementary formal system. This is the formalist’s conception of proof, the conception on which one can encode proofs in the natural numbers. Then for any elementary formal system in which one can do the amount of arithmetic needed to arithmetize proof, and metamathematics generally, one can prove G6del’s incompleteness theorems. GBdel’s theorems are often described as showing that proof in mathematics, in the formalist’s sense, is not the same thing as truth, or that syntax is not the same thing as semantics.
