> > 2) Godel's Theorem (loosely, no consistent formalism can prove its own > consistency) Informally, our skeptic claims, a proof is a compelling > argument. It seems clear to our skeptic that if we are to believe that > the formal theorems in our formalism should be accepted as compelling > arguments, then at the very least it must be the case that we already > believe that our formalism is consistent, and hence, no possible formal > proof within that formalism could be considered to be the evidence that > compels us to believe that the formalism is consistent.
This last sentence is well-written. I strongly agree with it, though it's possible that I might consider such a proof to be in the nature of corroborating evidence.
> And our skeptic > asks, is that not already the essential content of Godel's theorem?
> Even if you argue that Godel's proof is superior because it is actually > formal, you still have to deal with the informal notion of proof: does > Godel's proof compel us to believe that Godel's theorem is actually > true?
Yes. To a mathematical certainty.
> So, our skeptic asks, what is the concrete content to Godel's > theorem?
Godel's First Incompleteness theorem states that if arithmetic (number theory, Peano arithmetic, the theory P which Godel actually was using) is (omega) consistent, then it is incomplete: there will be formulae phi such that neither phi nor not-phi are provable in arithmetic.
The Second Incompleteness theorem states that one of those undecideable-in-P formulae is the formula that formalizes the proposition "P is consistent".
> What does it tell us that is not implicit in the definition of > "proof"?
The question is mis-asked, and has no answer, since it is based on a false assumption.
> How can it be tested?
It doesn't need to be tested, IMO, any more than any other theorem needs to be tested. In any case, it could be falsified by giving a proof in P (or PA, or any equivalent theory) of the formula Con-P (or, respectively, Con-PA, or Con-(eqivalent T)).
Is it anything more than clever > argumentation?
No more or less than any other mathematical theorem.
> How can such a theorem be regarded as one of the most > important theorems in all of mathematics?
That's a good question. The significance of the theorems is still being investigated, 75 years later. I personally think it may not be as significant as its reception has suggested. ( see http://tinyurl.com/zyzzu )
> Why don't mathematicians > raise these kind of questions?
> Why aren't they at least a little bit > skeptical?
'Even the crows on the roofs caw about the nature of conditionals.'