Goedel numbering is incoherent as a concept.  The difficulty, apparently not noticed, or ignored, lies in that logical and mathematical theories involve the concept of a variable.  A variable consists of something which can vary.  If something consists of a single object, then it cannot vary, for it is but one object.  Thus, it is not coherent to think of a variable as representing a single object.  A constant consists of a single object.  But, Goedel numbering involves assigning a constant to what previously got intended as a variable.

Thus, since a variable can vary, if we could logically assign a constant to a variable such that we have a one to one correspondence between the variable and the constant, that would imply that the variable can no longer vary, since constants cannot vary.

Goedel numbering does not respect the structure of variables.  Consequently, it cannot analyze variables.  To understand logic and mathematics, the concept of a variable must get understood.  Goedel numbering is a woefully inadequate tool for understanding mathematics and logic.

Suppose we look at something like the associative law for addition (or any universal law in logic or mathematics):

+(a, +(b, c)) = +(+(a, b), c).

How is it possible that we can infer that 1. +(65613, +(4, 3)) = +(+(65613, 4), 3) from that law?

How can we also infer that 2. +(567, +(28, 17)) = +(+(567, 28), 17)?

I answer that such is possible, because that law has variables 'a', 'b', and 'c' which range over all of the constants that we recognize as natural numbers, and because we take certain sequences of symbols and certain symbols as intending to convey natural numbers.

But, what would happen if we Goedel number the associative law?  Whatever we correspond to 'a', to 'b', and to 'c' get intended as representing constants.  But, constants don't range over anything.  If we could get both 1. and 2. from the above, then whatever constant would correspond to the variable 'a', would somehow have to correspond to '65613' and then to '567'.  A constant though consists of a single object, so we would have a single object corresponding to two objects such that the single object has enough structure to produce two objects, *while still remaining one object*.  But, this just doesn't have any coherence.  It is never the case that is possible that one object can equal two objects in terms of it's basic properties, since it is simply not possible for the natural number one to equal the natural number two.

The following I've learned with the help of the late William McCune's program Prover9 https://www.cs.unm.edu/~mccune/mace4/  2005-2010.

In the following the symbol '0', given a context, stands for a constant false propositions.  The sense behind the idea of '0' thus may get captured by the following sentence:

"When you are awake, The Earth is exactly the same as The Sun."

Suppose we consider the following basis for classical propositional logic.  The small letters for this system only get taken from the second half of the English abc's for small letters.  We might also subscript them with numeral symbols so long as each symbols can get clearly distinguished from other symbols.


1. C x Cyx.  Recursive Meaningful Expression Prefixing

2. C CxCyz C Cxy Cxz.  C-Distribution

3. C CCxy0 x.  Arbitrary Implication to Falsum to the Antecedent of the Implication.

Suppose also we have the following definitions:



def. 1: Nx is defined as Cx0.

def. 2: Axy is defined as CCxyy.

def. 3: Kxy is defined as CCxCy00.

def. 4: Exy is defined as CCCxyCCyx00.

The third axiom along with the above definitions allows us to deduce a few theorems in just a few steps. 

Applying def. 1 to 3. we obtain 4

4 C NCxy x. Negation of an arbitrary conditional to the antecedent of that conditional.

Now putting 0 in the place of y in 4 we obtain 5 (we can abbreviate that as x/0 * 5 following the scheme x/y * z, which I will use hereafter):

5 C NCx0 x.

Applying def. 4 to CNx0 in 5 we obtain 6:

6 C NNx x.  Double negation to the small letter of the meaningful expression.

3 y/Cy0 * 7

7 C CCxCy00 x.

Applying def. 3 to CCxCy00 in 7 we obtain 8:

8 C Kxy x.  Arbitrary conjunction to it's left meaningful expression.

1 y/Cyx * 9

9 C x CCyx x.

Applying def. 2 to CCyxx in 9 we obtain 10:

10 C x Ayx.  Arbitrary proposition to a disjunction with that proposition on the right of the disjunction.

3 x/Cxy, y/CCyx0 * 11

11 C CCCxyCCyx00 Cxy.

Applying def. 4 to CCCxyCCyx00 in 11 we obtain 12:

12 C Exy Cxy.   Arbitrary equivalence to a similar conditional.