Posted in:
Philosophy

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.*