Standard provability predicate

[summary: In theories extending [-minimal_arithmetic] there exists a $\exists_1$-formula $\square_T$(x) which defines the existence of a proof in an [ axiomatizable theory] $T$.

The formula satisfies some nice propereties, but fails to capture some intuitions about provability due to non-standard weirdness.]

We know that every theory as [expressiveness_mathematics expressive] as [-minimal_arithmetic] (i.e., [Peano_Arithmetic $PA$]) is capable of talking about [statement_mathematics statements] about itself via [encoding encodings] of [sentence_mathematics 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(x)$ 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 %%note:[ Proof]%% then we can define the $\Delta_1$-formula $Prv(x,y)$ such that $PA\vdash 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\vdash \exists y Prv(\ulcorner S \urcorner, y)$.

This formula is the standard provability predicate, which we will abbreviate as $\square_{PA}(x)$, and has some nice properties which correspond to what one would expect of a Provability predicate.

However, due to [non_standard_model 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\rightarrow A$ [55w 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 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)$. %%note:This condition is called [ $\omega$-inconsistency]%% This means that there is a non-standard number which satisfies the formula, but nonstandard numbers do not encode standard proofs!