> This may seem wrong, because surely our minds are capable of logical and
> arithmetic reasoning. However I believe in practice we are only capable
> of an approximation to strict perfection in logic and arithmetic, which
> is required by a formal system. For one thing, we are limited in the size
> of the propositions we can consider, understand, and prove. For another,
> we make mistakes. When we find ourselves in a contradiction, we don't
> melt down and find ourselves believing that every proposition is true,
> as a formal system would. Instead we abandon one of our beliefs (or else
> segregate the inconsistencies in our minds somehow).
Why not program computer in a similar way? I think program that uses
guesses could many times finds proof faster than program that thinks
formally. Conjectures would be zero order uncertain proofs.
Does there exist any material about this somewhere?
>From Tibetan - English - Dictionary of Buddhist Teaching & Practice
I found: ma nges pa'i rtags : uncertain proof / reason
;-)
> Now I think Penrose would deny these two points; he would say that even
> very large proofs could in principle be verified if we took them step by
> step, and secondly he says that even if individuals make mistakes, then
> the community of mathematicians notices and corrects them. So you have
> to expand your formal system to include an uploaded community, and now it
> is supposed to incorporate strict, perfect adherence to logic.
I think that he has done just that...
By STFW (searching the fine web) with keywords penrose, goedel, random
I found this:
"REVIEW OF: Roger Penrose (1994) *Shadows of the Mind*."
by Drew McDermott
http://bion.mit.edu/ejournals/b/n-z/.unindexed/Psyche/by_filename/2/psyche-95-2-17-shadows-9-mcdermo
-- LM lm+signature@sip.fi