> 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...
That's an interesting possibility, but it raises a confusing issue.
By making the formal system inconsistent, Godel's proof of incompleteness
no longer applies.
However, for Godel's theorem to even be applicable, we have to be dealing
with a formal system in the first place. A formal system which can prove
theorems both true and false is inconsistent, but strictly speaking
it can then prove all theorems true. This is not how your program is
intended to work.
I think the problem is that my claim yesterday that an AI program running
on a computer was "automatically" a formal system was not quite right.
Or more accurately, we could set up a formal system which characterized
all beliefs of the AI, but ironically it would not be powerful enough for
Godel's system to apply. Specifically, it would not be a superset of
logic and arithmetic.
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).
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.
You can judge for yourself how persuasive this is.
Hal