0
$\begingroup$

Let $e_{0},e_{1},...,e_{n}$ be a sequence of wffs or other expressions. Code each $e_{i}$ by a regular godel number $g_{i}$, to yield a sequence of numbers $g_{0},g_{1},...,g_{n}$. Then encode this sequence of regular godel numbers using a super godel number, to get $2^{g_{0}} \cdot 3^{g_{1}} \cdot 5^{g_{2}} \cdot ... \cdot \pi_{n}^{g_{n}}$ where $\pi_{n}$ is the $n+1$-th prime number. Then, define $Prf(m,n)$ to hold just if $m$ is the super godel number of a sequence of wffs that is a $\mathsf{PA}$ proof (Peano Arithmetic) of the closed wff with regular godel number $n$.

I am working on a much wider question to do with Rosser provability, but I am stuck inside of a fifth subproof, where I simply need to show that from $Prf(k,\ulcorner \neg \urcorner \star \ulcorner 0 =1 \urcorner) \wedge Prf(c,\ulcorner 0=1 \urcorner)$, that I can prove $c \neq k$, where $m \star n$ is the standard concatenation function. Here is the start of my attempt, although I am certain there is a very simple way!

Assume $c=k$. Further assume that $(\ulcorner \neg \urcorner \star \ulcorner 0=1 \urcorner)=(\ulcorner 0=1 \urcorner)$. Then, $2^{1} \cdot 3^{21} \cdot 5^{15} \cdot 7^{23} \cdot 11^{21} = 2^{21} \cdot 3^{15} \cdot 5^{23} \cdot 7^{21}$ by the standard godel coding of, $\neg: 1, 0: 21, =:15,S:23$, where $S$ is the successor function. This contradicts the fundamental theorem of arithmetic, so $(\ulcorner \neg \urcorner \star \ulcorner 0=1 \urcorner) \neq (\ulcorner 0=1 \urcorner)$.

Here is where I am stuck. I know previously in the proof that $Prf(k,\ulcorner \neg \urcorner \star \ulcorner 0 =1 \urcorner)$ and $Prf(c,\ulcorner 0=1 \urcorner)$, so how can I derive a contradiction to conclude that $c \neq k$?

Any help is greatly appreciated and if necessary I can explain more of the background problem, but I am certain that this part of the proof can be solved independently without relying on anything else other than simple logic and the definitions I have provided. I suspect that it has something to do with the uniqueness of the super godel number; namely, that there does not exist a number $n$ which is the super godel number of both $\ulcorner \neg \urcorner \star \ulcorner \varphi \urcorner$ and $\ulcorner \varphi \urcorner$. Yet I cannot represent my intuition formally!

  • 1
    @Qu$i$nn: Firstly, **I** left the note on the MO post that this is a cross-post. Secondly, it ma$k$es the OP seem impatient. If I went to as$k$ a professor *in person* then before he can get to answer me I knock on the office next door and ask the other guy because the first one didn't answer "quick enough" or there aren't "many people sitting in that office" do you think I would get anything but a slam in my face?2012-03-20

1 Answers 1

2

The question was answered by Joel David Hamkins on MathOverflow:

one can prove in PA right from the definition you have given that if $\operatorname{Prf}(c,n)$, then $n$ is the exponent of the largest prime dividing $c$. From this it follows immediately that $\operatorname{Prf}(c,n)\wedge \operatorname{Prf}(k,m)\wedge n\ne m\implies c\ne k$ since if $c=k$, then both $n$ and $m$ would be that exponent, contradiction. This answers the question, since it is easy to prove that $\neg 0=1$ and $0=1$ have distinct Gödel codes.