Was Gödel's entire argument actually formalizable when it was written?

Question

I was mulling over my understanding of the incompleteness theorems and here is something I'm having trouble with.

Seemingly, the pre-Gödel understanding of arithmetic can be modeled as $PA+\square$ where $\square$ is a modality meaning "it is provable that". We have as an inference rule that $A \vdash \square A$, so that anything we can prove, we can prove is provable. While completely useless for proving additional facts, the language allows us to express statements like $\neg \square 0=1$ ("$PA + \square$ is consistent"), as well as something we should like to interpret as the second incompleteness theorem, $\square \neg \square 0=1 \implies \square 0 = 1$.

So with this device we can characterize the Hilbertites as believing $\neg \square 0=1$, and any extremists who hold that arithmetic is complete are described by an additional axiom schema $\square X \iff \neg \square \neg X$.

Now here enters my alt-history Gödel with an indisputable proof of the PA-sentence:

$\text{Prov}(\#\{\text{Con}(PA+\square)\}) \iff \neg \text{Con}(PA+\square)$.

But that's not the only thing he accomplished. Apparently, he somehow convinced the rest of the world to also accept the following as an axiom schema:

$\text{Prov}(\#X) \iff \square X$

which combined with the theorem gives us its standard interpretation, that this theory is inconsistent if it can prove its own consistency:

$\square \neg \square 0=1 \iff \square 0=1$

What I am trying to understand is, how did he pull off this amazing trick?

From a modern point of view, I think we can untangle this issue using set theory. We can give a formal definition of exactly what we believe a proof is and then formally show the equivalence of the modality to the arithmetized provability predicate.

Was Gödel's result disputed on a similar basis after its announcement? It seems to me that in order for the result to be accepted by his contemporaries they would have had to all be in prior agreement about what exactly constitutes a formal proof. Otherwise, someone could claim that while the proof of $\text{Prov}(\#\{\text{Con}(PA+\square)\}) \implies \neg \text{Con}(PA+\square)$ is valid, $\text{Con}(T)$ doesn't actually mean $T$ is consistent and $\neg \square 0=1$ still holds.

Was it actually the case that this universal agreement existed or did the lack of it specifically create friction?

Also, what is the best modern resolution of this issue? Going back in time to 1931, what would we say to any doubters?

Answer 1

Firstly, let me point out that the incompleteness theorems can be proven in extremely weak meta-systems.$ \def\t#1{\text{#1}} \def\con{\t{Con}} \def\ross{\t{Ross}} $ Essentially all you need is the ability to reason about finite (binary) strings or equivalent, and you can already prove $(\con(S)⇒\con(S+\ross(S))\land\con(S+¬\ross(S)))$, where $\ross(S)$ is the Rosser sentence for $S$. This sentence can be seen to be a sentence about natural numbers, which can in turn via Godel's coding be seen to be a sentence about strings. Because we believe our meta-system to be meaningful, we hence expect that this sentence is in actual fact true about real-world strings, which forces us to believe that in reality any formal system $S$ that can be arithmetized (or equivalently has a proof verifier program) cannot be both consistent and complete; if $S$ is consistent then $\con(S)$ is true and hence both $\con(S+\ross(S))$ and $\con(S+¬\ross(S))$ are true, which implies that in reality $S+\ross(S)$ and $S+¬\ross(S)$ are both consistent.

Now of course Godel did not prove Rosser's version, but in any case he effectively proved for any arithmetizable formal system $S$ that $(ω\con(S)⇒\con(S+\con(S))\land\con(S+¬\con(S)))$, where $ω\con(S)$ is some arithmetical sentence stating ω-consistency of $S$. As before, it can be observed that for any such $S$ we really have that $S$ is ω-consistent iff $ω\con(S)$ is true in reality. Therefore his argument is very convincing to anyone who believes in the existence and basic properties of finite strings.

This perspective also explains why it was completely unobjectionable to talk about proofs as sequences, because the original notion is literally that a proof is a sequence of finite strings of naturals, which obviously can be encoded as a single string of naturals (add one and separate by zeros), which in turn can be encoded as a binary string (use unary). The fact that Godel encoded a proof as a natural number is incidental to the underlying accepted understanding of strings.

The only possible remaining concern is that perhaps Godel's encoding of symbol strings as natural numbers is problematic somehow, or that in reality we do not have a model of PA$^-$. But (speaking to doubters here) do you accept TC as meaningful? TC has only one binary operation representing string concatenation, and as shown in the linked post TC is so weak that it does not even prove cancellation. But yet every formal system that can interpret TC will be inconsistent or incomplete with respect to mere sentences about strings, and the proof would not need any number-theoretic facts such as Godel used.

But if you do reject the meaningfulness of PA$^-$ and even TC, perhaps due to apparent real-world physical constraints, then we are quite at a dead end, because there is no alternative. Suffice to say that mathematicians at that time did not doubt the meaningfulness of basic arithmetic, but I do think that there is no ontologically justifiable reason for believing in the existence of a perfect physical representation of a model of TC, much less PA$^-$, due to finiteness of the observable universe. Yet PA is incredibly accurate at human scales under any ordinary interpretation.

Anyway if you want the historical responses to Godel's work, you could ask on History of Science and Mathematics SE.

Answer 2

I think the question boils down to: why does/did the community accept that the arithmeticized provability predicate matches the actual provability predicate?

There is a lot to say about it, but the simplest answer is that there was a sense of a formal derivation as a sequence of statements, each of which is an axiom or is derivable from previous ones by an inference rule. (These are now called "Hilbert-style" derivations.) Gödel made no effort to justify that this was the correct way to look at a formal derivation, and he had previously proved the completeness theorem, which also requires a formal definition of derivability.

The formalization/arithmeticization of derivability in arithmetic exactly matches the regular mathematical definition, except that statements are replaced with their Gödel numbers and sequences are coded using arithmetical techniques. So most people quickly come to the conclusion that the formalization matches the intuitive notion. (Similarly, the formula $(\exists x)[y = x + x]$ in PA could be viewed as only a formal reflection of the intuitive statement "$y$ is even", but most people quickly see that the formula is an accurate formalization.)

Gödel's paper referenced a system ''P'' meant to resemble Principia Mathematica, but in light of the then-new computability theory, it was realized very quickly that the same techniques would apply to any effective formal system, because the definition of a formal derivation would be similar in any such system.

More recently, there have been some philosophical comments on whether the arithmeticized provability predicate in ''unsound'' theories (i.e. not in PA) can be fairly identified with "provability" in the normal sense. But that gets beyond Gödel's original paper, because he looked at $\omega$-consistent theories, which are always $\Sigma^0_1$ sound, so that $T \vdash \Box_T \phi$ implies $T \vdash \phi$.