# Gödel number for contradicting modus ponens?

When Gödel numbered statements, for instance modus ponens and connectives got their own numbers, does it matter which number each connective gets as long as they are different?

Sometimes I'm not sure if a statement is ¬($~A\to B$) or $~A\to ¬B$.

What is the Gödel number for ¬($~A\to B$) ("not modus ponens") e.g. saying for example "just because we change the interest rate doesn't mean that the trade deficit will narrow", or is it arbitrary as long as it is unique?

I read in a paper that implication has number 13. Is implication always number 13, regardless of which proof or formula we are working with?

• If we are working in number theory, to be specific, then $\lnot(A\to B)$ is not a formula. But if we replace the letters $A$ and $B$ by formulas, the resulting formula has an index that can be expressed in terms of the indices of the formulas $A$ and $B$ are replaced by. May 21 '16 at 17:12
• @AndréNicolas The difference between a statement and a formula is beyond my current knowledge. I will look it up. Thank you for the information. May 21 '16 at 17:20
• First a terminological point: "Modus ponens" is not the same as "implication" and it is not the name of a sort of formula; it is the name of a rule of inference ("From $A\to B$ and $A$, infer $B$.") Second: There is no particular reason for $\to$ to have the number $13$, but whatever number it gets should be used consistently, in all formulas where it occurs. May 21 '16 at 17:23
• I do not recall (if I ever knew) whether Godel indexed inference rules such as Modus Ponens. I do know that the standard indexing schemes, such as the one of Kleene, does not. That is done in an indirect way in the definition of what it means for $e$ to be the index of a proof. May 21 '16 at 17:26
• The proof will have a Goedel number. A proof is a particular kind of sequence of formulas, and that sequence will have a Goedel number. May 21 '16 at 17:57

Long Comment

There are many possible "numbering schema" but in any case, you have to take care of the details of the syntax.

For Gödel original numbering, see:

The symbol $\supset$ [i.e. $\to$] is an abbreviation, and thus for modus ponens we have:

A formula $c$ is called an immediate consequence of $a$ and $b$ if $a$ is the formula $(\lnot (b)) \lor (c)$.

"$\lnot$" is codified with $5$ while "$\lor$" is codified with $7$ and we need $11$ and $13$ for "(" and ")" respectively.

Having said that, $a$ will be codified by [if I've made no mistakes...]:

$2^{11}3^55^{11}7^{\#b}11^{13}13^{11}17^719^{11}23^{\#c}29^{13}$

where I've abbreviated with $\#p$ the code for the formula $p$.