Proof predicate in PA and stronger system

Question

It is said that proof predicate of PA is primitive recursive, but I cannot find explicit form of the proof predicate, or how it is defined. What is this proof predicate? What about defining for other theories stronger than PA?

Answer 1

A proof predicate is a fairly complicated arithmetical formula, and although its definition is completely constructive, it is a bit tedious. I recommend you consult a textbook on the incompleteness theorems (Smith and Smullyan are both very good).

In brief, given a formal language and an effective deductive system, we can encode statements and proofs by numbers, just with a simple translation of the syntax. A proof predicate $P(m,n)$ is an arithmetic formula expressing the fact $m$ encodes a proof of the statement encoded by $n.$ Computing this predicate only requires you to translate the Gödel numbers and then check that the proof uses axioms and rules of inference correctly and has the correct conclusion. Intuitively, this can be done with a computer program, moreover one that only uses ‘for loops’, no ‘while loops,’ so it is a primitive recursive predicate. This implies that it can be expressed by an arithmetic formula (in fact one that only has bounded quatifiers)... essentially we just turn the computer program above into some combination of addition, multiplication and logic. Note that there are many ways to implement the above procedure, so many different possible proof predicates.

Also note that I have said precisely nothing about PA so far. I just said a formal language and an effective deductive system. The only important thing was that formal proofs could be checked by an algorithm. So axiomatic systems where there is an effective way to check if a statement is an axiom and if a statement follows from another by a rule of inference qualify. In particular PA does. Also any axiomatizable extension of PA does: it’s just a matter of adding some additional axiom schemes for the program to check against. So yes, stronger systems can have a proof predicate. In fact ZFC (which is in a different language but much stronger in a precise sense) has a proof predicate as well, since at the end of the day it’s just a recursive set of axioms with first order logic as a deductive system, just like PA.