> Leevi Marttila, <lm+mail@sip.fi>, writes:
> > Hal Finney <hal@rain.org> writes:
> > > theorem and are unable to recognize certain truths. Since people are
> > > (according to Penrose) unlimited in their ability to recognize mathematical
> > > proof, this would mean that they are not formal systems and therefore no
Another argument against it is that human is not infallible in
deciding truth value. Another way to foil argument is to use program
that is inconsistent but still could decide right truth value for
'certain percentage' of theorems. Simplest (and useless) algorithm
would be to enumerate theorems and decide that even numbered theorems
are true ;-) Much more interesting algorithm would be such that it
could decide truth value for remarkable number of theorems without
using actual proof. Something like simulation of good human
mathematician... Does Penrose take into account inconsistent
algorithms? Is there study of fuzzy proofs and/or proofing process?
Something like humans probably use before finding actual proof.
[...]
> Penrose's argument is weak enough IMO that it should be fought on its
> own grounds. We accept that machines have limitations; the absurdity is
> the claim that humans have none. (Keep in mind my repeated disclaimer
> not to have a deep understanding of his argument.)
Neither do I.
-- LM lm+signature@sip.fi