Standard provability predicate

We know that every theory as expressive as minimal_arithmetic (i.e., $PA$) 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 on what a proof is, we will come to the conclusion that a proof is a sequence of symbols 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 also 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 a provability predicate.

However, due to non-standard models, 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$.

There are non-standard models of $PA$ which contain numbers other than $0,1,2,..$ (called non-standard 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)$. ^[2] This means that there is a non-standard number which satisfies the formula, but nonstandard numbers do not encode standard proofs!

1. ^{^︎}

   Proof

2. ^{^︎}

   This condition is called $\omega$-inconsistency