Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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!

share|improve this question
I have also posted this question on MO: mathoverflow.net/questions/91693/…, but it does not seem to be getting much coverage over there. –  Samuel Reid Mar 20 '12 at 8:19
You are not supposed to do that. Post it in one place or the other and wait before crossposting. –  Zhen Lin Mar 20 '12 at 8:28
Can't you just use the fact that if an expression $\sigma$ is longer than an expression $\tau$, then the largest prime dividing $\ulcorner \sigma \urcorner$ is strictly greater than the largest prime dividing $\ulcorner \tau \urcorner$? –  Arthur Fischer Mar 20 '12 at 8:44
Sam, there are quite a few logicians roaming the wilderness of MathOverflow, many of which are also writing here. You have waiting a whopping half an hour for "some coverage". The fact that this thread gets more views is not a reason that it gets better coverage. Next time please wait a day or two before cross-posting (unless you were advised to cross-post in the comments). Impatience is frowned upon in places were people freely give from their time to answer your question. –  Asaf Karagila Mar 20 '12 at 8:49
@Quinn: Firstly, I left the note on the MO post that this is a cross-post. Secondly, it makes the OP seem impatient. If I went to ask 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? –  Asaf Karagila Mar 20 '12 at 11:35

1 Answer 1

up vote 2 down vote accepted

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.

share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.