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?

_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:

* Jean van Heijenoort (editor), From Frege to Gödel: A Source Book in Mathematical Logic (1967), page 600:



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$.