It is possible, though not very pleasant, to produce formal proofs in Peano arithmetic.
Consider, for example, the following proof of the fact that \({ 2 + 2 = 4 }\), which in the language we’re using is written as \({ [ ( 0 '' + 0 '' ) = 0 '''' ] }\).
The first and fourth lines are our second and third arithmetic axioms. The second line is the result of one of our logical rules of inference, eliminating the universal quantifier from the first line and replacing the associated variable with the numerical expression \({ 0 '' }\). Similarly the fifth line is derived from the fourth by eliminating the universal quantifier and replacing the variable by \({ 0 '' }\). Both the sixth line and the ninth are derived from the fifth by removing the universal quantifier and replacing the variable, in one case by \({ 0 }\) and in the other by \({ 0 ' }\). The third line is derived from the second by applying our fourth arithmetic rule of inference and the eighth line is similarly obtained from the seventh. The seventh line is derived from the third and sixth by means of our second arithmetic rule of inference, and the tenth is similarly derived from the eighth and ninth.
Statements more complicated than \({ 2 + 2 = 4 }\) have correspondingly longer proofs. Hofstadter, for example, gives a proof that addition is commutative. It’s 56 lines long. As we saw earlier it’s possible to give a fairly concise statement within the language of Peano arithmetic of the fact that there are infinitely primes. It’s possible to give a formal proof as well, but it’s hardly an enjoyable exercise. Logicians, though, are generally much more interesting in figuring out what can or can’t be proved within a formal system than with actually supplying proofs. In other words, they tend to live in the world of semiformal proofs rather than formal proofs.