🚀 go-pugleaf

The way I understand Penrose, his argument takes the form:

     Suppose that human reasoning about arithmetic is captured exactly
     by some formal system T. This means that any statement of
     arithmetic that human mathematicians can come to know is true
     is provable by T, and that T uses only methods of reasoning
     (inference rules, axioms, etc.) that humans believe to be valid.

     Then, since the basic mathematical principles humans use are
     simple, clear, and obviously true, we could then study theory T
     and see that it only generates true statements. Therefore, we
     conclude that T is consistent (a false theory can be consistent,
     but a true theory can't be inconsistent). Then, by Godel's
     theorem, we can produce an arithmetic statement G(T) such that
     (1) is true, and (2) cannot be proved by T. Since we have just
     convinced ourselves that G(T) is true, and T cannot prove G(T),
     that implies that T does *not* capture all of our reasoning about
     arithmetic. Contradiction. Therefore, there is no such T.

First of all, this argument doesn't show that human reasoning is more
powerful than formal reasoning, at all. It shows that human reasoning
is more powerful than any formal reasoning that we can see is clearly
valid. Penrose' argument cannot be used, for instance, to show that NF
(Quine's New Foundations, an alternative set theory) fails to capture
all of human reasoning about arithmetic. We could get to the
construction of G(NF), the Godel statement for NF, and then we would
be stuck; if NF is consistent, then G(NF) is true but unprovable from
NF, but we are (so far, anyway) unable to prove that NF is consistent.
So while NF may be unable to prove G(NF), neither can we.

Therefore, Penrose' claim is reduced from the boast "Human reasoning
is more powerful than any consistent formal system" to the much more
modest "Human reasoning is more powerful than any system that human
reasoning can prove is consistent". This modest claim is just as true
if you replace "human reasoning" by "reasoning within PA" or
"reasoning within ZFC", or any other formal system. Not a very
convincing argument that human reasoning is not algorithmic.

Daryl McCullough
ORA Corp.
Ithaca, NY