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!