Standard provability predicate

We know that every theory as expressive as minimal_arithmetic (i.e., Peano Arithmetic) is capable of talking about statements about itself via encodings of sentences of the language of arithmetic into the natural numbers.

Of particular interest is figuring out whether it is possible to write a formula $Prv\left(x\right)$ which is true iff there exists a proof of $x$ from the axioms and rules of inference of our theory.

If we reflect about what it is a proof, we will come to the conclusion that a proof is a sequence of letters which follows certain rules. Concretely, it is a sequence of strings such that either:

1. The string is an axiom of the system or...
2. The string is a theorem that can be deduced from previous strings of the system by applying a rule of inference.

And the last string in the sequence corresponds to the theorem we want to prove.

If the axioms are a computable set, and the rules of inference are also effectively computable, then checking whether a certain string is a proof of a given theorem is perfectly computable.

Since every computable set can be defined by a ${\Delta }_1$-formula in arithmetic ^[1] then we can define the ${\Delta }_1$-formula $Prv(x,y)$ such that $PA⊢Prv(n,m)$ iff $m$ encodes a proof of the sentence of arithmetic encoded by $n$.

Then a sentence $S$ is a theorem of $PA$ if $PA⊢\exists yPrv(┌S┐,y)$.

This formula is the standard provability predicate, which we will abbreviate as ${\square }_{PA}\left(x\right)$, and has some nice properties which correspond to what one would expect of the provability predicate ^[2].

However, there are some intuitions about provability that the standard provability predicate fails to capture. For example, it turns out that ${\square }_{PA}A\to A$ is not always a theorem of $PA$. The reason why this happens is due to nonstandard numbers.

There are models of $PA$ which contain numbers other than $0,1,2,..$. Those are called nonstandard models of arithmetic. In those models, the standard predicate ${\square }_{PA}x$ can be true even if for no natural number $n$ it is the case that $Prv(x,n)$. ^[3] This means that there is a non-standard number which satisfies the formula, but nonstandard numbers do not encode standard proofs!

1. ^{^︎}

   Proof

2. ^{^︎}

   See the Hilbert-Bernais derivability properties

3. ^{^︎}

   This condition is called $\omega$-inconsistency