We know that every theory as expressive as minimal_arithmetic (i.e., ) 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 which is true iff there exists a proof of 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:
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 -formula in arithmetic [1] then we can define the -formula such that iff encodes a proof of the sentence of arithmetic encoded by .
Then a sentence is a theorem of if .
This formula is the standard provability predicate, which we will abbreviate as , 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 is not always a theorem of .
There are non-standard models of which contain numbers other than (called non-standard models of arithmetic). In those models, the standard predicate can be true even if for no natural number it is the case that . [2] This means that there is a non-standard number which satisfies the formula, but nonstandard numbers do not encode standard proofs!
This condition is called -inconsistency