Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. 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
    
Cross-posted on math.SE: math.stackexchange.com/questions/122419/… –  Asaf Karagila Mar 20 '12 at 8:52
add comment

1 Answer

up vote 3 down vote accepted

I am not sure I've properly understood the question, but it seems that you are asking whether the Gödel codes of proofs of different formulas must be different, and this seems obvious.

More specifically, one can prove in PA right from the definition you have given that if $\text{Prf}(c,n)$, then $n$ is the exponent of the largest prime dividing $c$. From this it follows immediately that $\text{Prf}(c,n)\wedge\text{Prf}(k,m)\wedge n\neq m\implies c\neq 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.

(I apologize if I have misunderstood the question.)

Let me add that one needn't regard the coding of sequences of formulas as a kind of "super" Gödel coding. Rather, this is just ordinary Gödel coding, a concept that is used generally to refer to any kind of coding of finitary combinatorial objects, including proofs or graphs or groups or sequences of formulas or what have you, with natural numbers.

share|improve this answer
    
@JoelDavidHamkins: My question IS this simple, thank you for the response. I was attempting to give a fitch-style proof that a certain class of theories prove their own consistency, and I was just not sure what rule I would use at the obvious point you pointed out! –  Samuel Reid Mar 20 '12 at 14:29
add comment

Your Answer

 
discard

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.