# Proof predicate in PA and stronger system

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?

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.