> Look at the proof - page after page of work showing how to encode and decode formal propositions using primitive recursive functions. Look at the game. Move

> Look at the proof - page after page of work showing how to encode and decode formal propositions using primitive recursive functions. Look at the game. Move after move of rooks moving in columns and rows and of bishops moving on the diagonals. :) > Goedel's theorem is exactly that mathematics is not a symbolic game - that Hilbert's program is not possible. The proof relies on reducing logical deduction to arithmetic. The point was that thinking of mathematics as a game in the first place requires "...the conceptual leap to thinking about mathematical statements as mathematical objects..." Goedel's proof didn't come out of nowhere, and he was NOT the one to first propose thinking of mathematical statements as mathematical objects. In many ways, Goedel's proof was actually a response to/rejection of "mathematical statements as mathematical objects" Goedel's big leap was... the proof itself. Was it the numberings? Well, I guess, but really it was what he did with the numberings. And then how he related that to arithmetic. It's hard to pick out a single piece of the derivation and say "ah ha! That's the key insight!". So I think "the point is in the details" is pretty accurate.