No ${}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}$

@MauroALLEGRANZA Aren't S(0) and S(S(0)) constants though, or are S(0) and S(S(0)) variables?

They are terms : terms are : (i) individual variables : $x_i$; (ii) individual constants : in arithmetic $0$; (iii) every string built up from an $n$-ary function letter $f_i^n$ (in arithemtic : the unary $S$) and $n$ terms. Example from arithemtic : $S(0), S(x_1), S(S(0)), \ldots$

Goedel numbering applies one level "lower" than I think you're giving it credit for: it applies to the a priori meaningless string of symbols. So, for example, the string "$S(()()(((()SSSS$" has a Goedel number, even though it's completely meaningless.

@MauroALLEGRANZA So, they are strings, which are terms. But, aren't strings which are not variables, still constants even if not individual constants?

@NoahSchweber So, the meaningless string 'ab' could have a Goedel number of "S(0)S(S(0))". But, isn't S(0) a non-individual constant, S(S(0)) a non-individual constant, and thus 'S(0)S(S(0))' a non-individual constant, even if the author originally intended both 'a' and 'b' in 'ab' as individual variables?

Or can we have more than one successor of 0? Can there exist more than one successor of the successor of 0?

@DougSpoonwood I have no idea what a "non-individual constant" is. The Goedel number of the string 'ab' is $2^13^2$ (say). It doesn't matter how we represent this; the Goedel number of a string is a number.

Now let's say you never want to talk about numbers, only strings. Fine. Let $T$ be a theory in a language rich enough to talk about numbers and strings (so, the language of arithmetic, plus some constant symbols $a, b, ...$ and appropriate language for these, including a symbol $\nu$ for Goedel number, and reasonable axioms). Then the meaningless string "$\nu(ab)=SSSSSSSSSSSS(0)$" (omitting some parentheses for clarity) is a theorem (= derivable string) of $T$; and so is "$\nu(ab)=SSS(0)\times SSSS(0)$".

@NoahSchweber You say that the Goedel number of a string is a number. Aren't all numbers constants? Isn't every number a constant?

@DougSpoonwood You are confusing the Goedel number of a string with the canonical representation of the Goedel number of a string. I would say the answer to your question is no - a constant is a kind of symbol, and a number is, well, a number.

@DougSpoonwood Let's simplify things: do you think the length of a string is a problematic concept? Again, this is a map that assigns a number (which can be written a variety of ways) to a string . . .

@NoahSchweber No, I don't think the length of a string is problematic (though one can argue against assigning the same length to 'abc' and 'ade'). But, once we pick a definition for length, that length is a constant for a given particular string.

@DougSpoonwood So is the Goedel number (once we choose a particular Goedel encoding scheme). It doesn't matter that we can represent the Goedel number in two different ways, any more than it does that we can represent the length in two different ways: "the length of 'aabb' is $SS(0)+SS(0)$" and "the length of 'aabb' is $SSSS(0)$" are both true statements (assuming the usual definition of "length").

@NoahSchweber So you haven't you now indicated that a Goedel number has the sense of a constant? But, the sense of 'a', 'b', and 'c' in CCabCCbcCac do not have the sense of a constant, they have the sense of variables. In the first-order formula $\Pi$xC$\phi$x$\phi$r, $\phi$ is a function, $\Pi$ is universal quantification, while 'x' and 'r' have the sense of variables, don't they?

@DougSpoonwood I genuinely have no idea what "sense of a constant" means. The Goedel number map is exactly the same type of thing as the length map; if one makes sense, then so does the other.

@NoahSchweber Anything would have the "sense of a constant" if it can only refer to a single object over time (variables on the other hand can refer to more than object over time). The length map returns a constant. If the length of something is six units, that 'six' is not a variable, but a constant. So, won't the Goedel number map also return a constant? If a Goedel number has the same type as a length, and you believe Goedel numbers do not have the type constant, then I don't see how you avoid that length does not have the type constant. But doesn't length have the type constant?

@DougSpoonwood The Goedel number map also returns a number, in the same sense that the length map does. So the Goedel number of a fixed string is a constant; identically to how the length of a fixed string is a constant. But note that this means that "the Goedel number of $\varphi$ is $SSSS(0)$" and "the Goedel number of $\varphi$ is $SS(0)\times SS(0)$" mean exactly the same thing. That is, the Goedel number is $SSSS(0)$, not '$SSSS(0)$'. Maybe the following helps: in the formula Cab, b is a variable; but in the string "Cab", b is a specific symbol, and hence a constant. (cont'd)

Goedel numbering operates on the level of strings, not formulas-with-meaning. I think your confusion is coming from conflating a sentence with the string representing it, and hence demanding that the Goedel number map "respects more structure" than is actually relevant. And again, I really do not see how one could possibly be okay with the length map, but not the Goedel number map: each takes in a string, and outputs a number.

@DougSpoonwood It occurs to me that you might find the following interesting, and also that it might help assuage fears that the Goedel number map is somehow illegal: a machine-verified proof of the incompleteness theorem and other theorems.

@Noah Schweber p. 599 of Jean van Heijenoort's "From Frege to Goedel" reads "The primitive signs of the system P are the following: ... II. Variables of type 1 (for individuals, that is, natural numbers including 0): "x_1", "y_1", "z_1", ...; Variables of type 2 (for classes of individuals): "x_2", "y_2", "z_2", ...;" ['_' isn't in the text, I'm using it to indicate a subscript] And on p. 601 it reads...

@NoahSchweber "... to the variables of type n we assign the numbers of the form p^n [I'm using ^ to indicate a superscript] (where p is a prime number > 13). Thus we have a one-to-one correspondence by which are a finite sequence of natural numbers is associated with every finite sequence of primitive signs (hence also with every formula)."

@NoahSchweber Also, consider a string of variables, where all of the letters standing for variables stand for at least two objects, such as 'ab'. If we Goedel number that as 'S(0)S(S(0))', then the first part 'S(0)' is a constant since '0' is a constant, and the second part 'S(S(0))' is a constant, since S(S(0)), correct? But, 'ab' isn't composed of constants. So, I do not see any way that such a correlation faithful represents the structure of the string of variables 'ab'.

@NoahSchweber At the very least a constant is a completely inadequate tool to analyze the structure of a variable. A variable has a one-to-many relation with it's values. A variable with a one-to-one relation with it's values may as well get disregarded as a variable entirely and just get regarded as a constant. A constant does not have a one-to-many relation with it's values. A constant indicates exactly one value.

@NoahSchweber And as interesting as that machine-verified proof of the incompletness theorem, what of it? Garbage in, garbage out is a well-known refrain with computers for a good reason. If the incompleteness theorems rely on analyzing variables as constants, then there exists a serious conceptual problem with them. Or would you disagree with that?

We're going around in circles. The Goedel number assigns a number to a string. The length function assigns a number to a string. Neither of them respect the "meaning" of the symbols in the string, since they're not looking at them in that way. They are just treating the string, directly, as a meaningless string of symbols. Some of those symbols could be things we designate as variable symbols, some of them could be otherwise, it simply doesn't matter.

Or, treat it this way: consider the map that takes a string - with some symbols $a$ and $b$ that we think of as variables - and spits out the string gotten by replacing every "a" with "0" and every "b" with "S(0)". Do you have a problem with this map? It's a map from strings to strings, but it "confuses" variables and constants! If you really have a problem with this kind of map, I can't help you - you have to learn to distinguish the symbol from what it represents.

OK, I'm done here, I tried.

@NoahSchweber Yes, I have a problem with that map. You told me to think of the symbols 'a' and 'b' as variables. But, each of them can only take on the value of one constant. So, it's as if you had told me those things could represent more than one thing, but really those things could only represent one thing. It is impossible that two can equal one! You may as well just take 'a' and 'b' as constants in such a case. But, logic needs variables (and so does arithmetic).