Necessity of arithmetic truths into Godel sentences

Question

My layman but hopeful to understand self is slowly trying to understand some of Godel and the philosophical implications of his work (uh oh).

Currently my understanding is that on some level:

Godel leveraged the “necessary” structure of arithmetic and primes into declarative linguistic statements, like “this sentence is not provable in this system” (1st incompleteness I think), hoping those too would be necessary (and thus true) by being tied at the hip to basic mathematics.

I can understand wanting to attach as much as possible to something necessary, (I know not every mathematician views math as necessary but I think most do), as we try to do that with scientific theories all the time, that is connect scientific theory to math.

The science one makes plain sense to me, as science has a lot of clear structure and obvious points to connect to mathematics. Once a linkage to math is established, the science benefits and sometimes takes a backseat to the math: our best explanations of honeycomb structure leans mostly on the math (not just my claim).

But it seems like any sentence can be laid upon mathematical structure. It doesn’t matter that Godel found/made one that speaks of truth outside the formalism. Any and every sentence is possible right? Just change the word and letter numberings to different primes.

Now I don’t have a knockdown argument to say science clearly maps into math in specific ways and natural language doesn’t, as science changes and new math may serve as a better model. And probably most people think Godel’s lettering isn’t arbitrary.

My main point is, did Godel hope to extend the necessity of math to linguistically parseable sentences? (seems like yes), and how can any result of this be necessary and not arbitrary? (It seems like I could encode any sentence, and I don’t want to, as that leads to things like math proves “fairies are pink” or whatever.) This just doesn’t work like the honeycomb example. It’s not math doing anything toward making sentences true or false, because any sentence with the same number of letters could be attached to the same numbers just with different encoding. Or a contradictory one could be encoded with different encoding rules. It’s (mainly the encoding rules) too arbitrary. By the encoding rules not being necessary, the necessity of math is not transferred unto anything.

Answer 1

"But it seems like any sentence can be laid upon mathematical structure. It doesn’t matter that Godel found/made one that speaks of truth outside the formalism. Any and every sentence is possible right? Just change the word and letter numberings to different primes. ... It seems like I could encode any sentence, and I don’t want to, as that leads to things like math proves “fairies are pink” or whatever"

I've noticed that some popular articles on Gödel's theorem like this one and this one may give the impression that the meat of Gödel's proof was his scheme of "Gödel numbering", i.e. deciding on a rule for mapping symbols in statements about provability to purely arithmetical symbols, so that any given statement could be "translated" into an arithmetical equation. I think this is potentially misleading, since in itself this is pretty trivial and would prove nothing. In relation to your question about encoding an English statement like "fairies are pink", it's true you could find cipher to encode any ordinary english language statement, say "I'm feeling hungry", as a well-formed formula in arithmetic (like 'let the letter I correspond to 5, let an apostrophe correspond to +, ...'). But it would be absurd to expect that determining the truth or falsity of the arithmetical statement would let us deduce whether I'm actually hungry or not.

From the summaries I've read by mathematicians, what Gödel did was a lot more involved than just Gödel numbering--he came up with a way of proving by construction that for any metamathematical statement about provability within an axiomatic system, one could find a corresponding arithmetical statement S such that S will be true if and only if the metamathematical statement is true (and when I say 'S will be true', I mean it's a true statement about arithmetic, which could be in principle be judged by some being who's sufficiently good at proving statements about numbers, even if they have no idea that Gödel has mapped it to a metamathematical statement).

For example, see the page titled "Proof properties" in this summary from a course on computational logic:

Gödel then showed that for any recursive set of axioms A, there is a definable expression Proof(x,y) such that Proof(n,m) is true iff n is the code of a proof whose premises are members of A and whose conclusion is a sentence whose code is m (for this you use the Axiom(x) and Implies(x,y) expressions).

This means that there is also a formula Provable(x) = ∃y Proof(y,x) that defines the property of being provable from A.

So there wouldn't be any analogous result for English-language statements where there'd be an algorithmic mapping from English statements to arithmetical statement such that you could prove the English statement is true if and only if the corresponding arithmetical statement is true.

Even if we leave aside the vagaries of natural language and just talk about non-arithmetical claims in pure mathematics, it's not in general possible to find an algorithmic way of mapping such claims to arithmetical claims in a way that's guaranteed to preserve truth-value. In the specific case of mathematical claims that are computably true or false, then it actually has been shown that statements about whether a Turing machine program produces some result can be mapped to arithmetical statements about solutions of Diophantine equation in a way that preserves truth-value (for example, p. 72 of this paper says that 'every Turing machine is represented by a diophantine equation and vice versa', and also see this answer from the math stack exchange). But the same cannot be the case for non-computable statements. As I discussed in this answer, a non-computable system that starts from the Peano axioms of arithmetic and uses the inference rules of first-order logic combined with an extra non-computable inference rule, the ω-rule, can prove the truth or falsity of all statements about arithmetic expressible in first-order logic; this means there can't be any arithmetical statement that's a "Gödel sentence" for this non-computable inference system S (i.e. a statement G that is equivalent in truth-value to 'G can never be proven by the non-computable system S'), otherwise you'd get a logical paradox.

In his original proof Gödel said that he was showing that any formal system capable of proving certain kinds of arithmetical claims must be incomplete or inconsistent, but in retrospect that is understood to be equivalent to the notion of a computable system. The book Gödel, Tarski and the Lure of Natural Language by Juliette Kennedy has a comment on this on p. 19:

When Gödel proved his Incompleteness Theorems he left open what an effectively given formal system means. Only after Turing’s fully mathematical definition of effective computability was given, was Gödel ready to declare the concept of a formal system to be clearly defined: a formal system can be thought of as any mechanical procedure for producing formulas.

On p. 55-56 Kennedy also quotes some of Gödel's own remarks from a 1965 postscript to a collection of his 1934 lectures:

In consequence of later advances, in particular of the fact that, due to A. M. Turing’s work, a precise and unquestionably adequate definition of the general concept of formal system can now be given, the existence of undecidable arithmetical propositions and the non-demonstrability of the consistency of a system in the same system can now be proved rigorously for every consistent formal system containing a certain amount of finitary number theory.

…Turing’s work gives an analysis of the concept of “mechanical procedure” (alias algorithm or computation procedure or “finite combinatorial procedure”). This concept is shown to be equivalent with that of a “Turing machine.” A formal system can simply be defined to be any mechanical procedure for producing formulas, called provable formulas. For any formal system in this sense there exists one in the [usual] sense that has the same provable formulas (and likewise vice versa)

So Gödel's original result should not be understood as applying to anything other than computational procedures for determining truth-values of arithmetical statements, in particular it can't be applied to natural language or non-computable procedures. @user21820 mentions that since Gödel's original proof, there have been expanded incompleteness results that would also apply to some types of non-computable procedures, however I believe this would only imply some types of weaker oracle machines will inevitably have statements in first-order arithmetic they can't decide, while other types of stronger oracle machines can decide every possible WFF in first-order arithmetic.