[SamBam]

Indeed. It reminds me of Penrose in The Emperor's New Mind (or one of his other books), where a large chunk of his argument that human consciousness and understanding can't be fully explained by computational processes, because humans can understand and see the truth of certain statements that formal systems cannot.

Mathematicians have spilled a bunch of ink explaining why Penrose didn't understand Godel's proof.

[omnicognate]

The linked article is ridiculous, but your comment is a misrepresentation of the Penrose debate. The main weak point of Penrose's argument isn't that he "didn't understand Godel's proof". He rightly observed that Godel's incompleteness theorem requires that either human minds are capable of things algorithms are not capable of, or that their perception of mathematical truth is limited in certain ways, an observation that Godel himself made. The main point of disagreement with his critics is not the mechanics of Godel's theorem which, unsurprisingly, this Nobel prize winning mathematician (*) understands perfectly well, but whether human perception of mathematical truth is limited in these ways.

The question of whether human perception of mathematical truth is infallible is open to philosophical debate. Penrose distinguishes between mistakes, which all mathematicians make but which in principle they can later come to recognise as mistakes, and true incorrect perception of mathematical truth, where no amount of checking, re-derivation, etc. could possibly right the incorrect perception. His view is that the latter type of error does not exist, that there is a mathematical ground truth that we can directly perceive and that is infallible, and that the mistakes made by mathematicians are of a different nature to inconsistencies in that perception of mathematical ground truth.

Penrose went too far in presenting this argument as a proof of the impossibility of strong AI based on algorithms. The point about human perception of mathematical truth can very reasonably be disputed, and is part of a much larger debate about the fundamental nature of maths that is far from settled. Personally, though, my intuition is that Penrose is right about the human perception of mathematical truth, and I therefore find the Godel-based argument persuasive. It's not a proof because it rests on an assumption that has not been proven, but I find it convincing to the extent that I tend to think that the assumption is probably true.

So the debate is a philosophical one more than it is a mathematical one, and while Penrose may be guilty of some rather bad PR, accusing him of "not understanding Godel's proof" does him a disservice.

* Yes, there's no Nobel prize in mathematics, but he is a mathematician (as well as a physicist) and he has won a Nobel prize.

[mistermann]

Could you possibly expand on this?

> He rightly observed that Godel's incompleteness theorem requires that either human minds are capable of things algorithms are not capable of...

[sdwr]

Not OP, feel free to correct me, but Godel proved that any formal system of logic can be shown to be logically inconsistent at at least one point.

"Formal system of logic" maps well onto Turing machines, and Turing machines map onto "any computer system" if you are very abstract about it.

Now, people are wrong about mathematical facts, but seemingly not forever. We puzzle it over, come back to it, someone makes a breakthrough. It doesn't seem like there is a fixed blind spot where our logic breaks down.

So what are people doing that is not captured by a formal system of logic?

Options:

1. The mapping of Turing machines to computers isn't airtight - they are doing something "more" than a TM with infinite time + space is capable of

2. People are not "more than" an infinite TM either, we just romantically believe we are, and ignore our own flaws

3. People are doing something special that is not captured by our theory of computation

[roywiggins]

> Godel proved that any formal system of logic can be shown to be logically inconsistent at at least one point.

He proved they can be inconsistent, or incomplete. The ones that mathematicians work with are incomplete and assumed to be consistent[0], namely that there are statements which are true, but not provable, within that system. Consistent-but-incomplete systems don't have any contradictions or logical holes; they just can't determine the truth of every possible statement.

From an incomplete system you can build a "more powerful" system- one with another axiom that makes more things provable without contradicting anything in the original one.

In inconsistent systems, everything is provable, even statements' own negations, so they aren't very useful.

[0] one statement that you can't prove within a (sufficiently powerful) system is "this system is consistent."