Interesting thoughts by Quine on Gödel’s proof:
In fact, you know, Gödel’s proof shows us a byproduct - maybe I should go back a step: Gödel’s proof applies to any formalism, formalism being sharply defined, but what the definition comes to is that rules of proof are formal if they could be programmed on a computer. And a proof procedure is formal if it can be tested on a computer to see whether it was carried through correctly or not. So, this is very liberal, and anything that could be thought of really as a proof beyond pure adventure surely should be formal.
The point is that Gödel’s proof is always carried out relative to some given formalism; he doesn’t give the formalism, but given any formalism that fulfills these requirements for a formalism, relative to that you can construct this sentence, which cannot be proved by that formalism, unless the formalism is such that you could prove a falsity. In fact, if you could prove it, it would be false. What I wanted to bring out here is that it also comes out of Gödel’s proof that this formula, this undecidable formula, is in fact true. And that you can, then, adopt it as a further axiom, strenghten your system, now there is a system, in which that previously undecidable theorem is a theorem. But then reconstruct Gödel’s whole argument relative to this extended system, you get another. And that’s so, but - surely Gödel wouldn’t have conceded either that this shows that formalism is a dead end, and that something else should be found; but on the contrary, this is where formalism really in an informal way has vindicated itself, in showing the thing to be true. (Pause) It says that you can extend your horizon, but there’s always a further step with which yout horizon could be extended, and that’s Gödel’s theorem.