Using recursion theory to show a particular sentence is not provable in an extension of PA.

49 Views Asked by At

For a natural number $n$, the notation $\underline{n}$ means taking the sucessor of $0$ $n$ times. We denote the Gödel number of a formula $\phi$ by $\lceil \phi \rceil$. We have a function $Sub: \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ such that $Sub(\lceil \phi(x_1) \rceil, y)$ is the Gödel number of $\phi( \underline{y})$.

The exercise is as follows:

Let $T$ be an effectively formalized extension of PA. Suppose $\psi(x_1, x_2) $ represents ‘$n_2$ codes a proof in $T$ of the formula with Gödel number $Sub(n_1, n_1)$’. (I think this is a typo and supposed to be $Sub(x_1, x_2)$.)

Let $n$ be the Gödel number of $\forall x_2 \neg \psi(x_1, x_2)$.

Show that if $T$ is consistent,

$T \nvdash \forall x_2 \neg \psi(\underline{n}, x_2)$

Intuitively, we have that $\psi(\lceil \phi(x) \rceil, x_2)$ is $x_2$ is a proof for $\phi(\underline{\lceil \phi \rceil})$. So $\forall x_2 \neg \psi(\lceil \phi(x) \rceil, x_2)$ says that there is no proof for $\phi(\lceil \underline{\phi(x)} \rceil)$.

I am having trouble finding out what $\forall x_2 \neg \psi(\underline{n}, x_2)$ actually says since it seems to be self referential. My best guess is "there is no proof for the statement "there is no proof for $\forall x_2 \neg \psi(\underline{n}, x_2)$"".

It is likely that we have to use Gödels incompleteness theorem as $T$ is a consistent extension of $PA$, but I don't see how we can relate that there is some undecidable sentence to this particular sentence being undecidable.

1

There are 1 best solutions below

0
On BEST ANSWER

If $T\vdash \forall x_2 \lnot \psi(\underline n, x_2),$ let $m$ encode that proof. Then we have $T\vdash \lnot \psi(\underline n,\underline m),$ which based on what $\psi$ represents, means that $m$ does not encode a proof of the formula with GN $\operatorname{Sub}(n,n).$ But since $n$ is the Gödel number of $\forall x_2\lnot\psi(x_1, x_2)$ the formula with Gödel number $\operatorname{Sub}(n,n)$ is $\forall x_2\lnot\psi(\underline n,x_2),$ so $m$ does not encode a proof of $\forall x_2\lnot\psi(\underline n,x_2).$ Contradiction.