Thanks for the comments. Just a few belated remarks:
1. Axiomatic systems for expected utility are widely used in the machine learning literature, which contains many human-generated proofs concerning expected utility. No essential novelty here.
2. It is straight-forward to devise simple tasks and corresponding consistent axiomatic systems such that there are short and trivial proofs of target theorems. On the other hand, it is possible to construct set-ups where it is impossible to prove target theorems, for example, by using results of undecidability theory.
The point is: usually we do not know in advance whether it is possible or not to change a given initial problem solver in a provably good way. The traditional approach is to invest human research effort into finding out. A G�del Machine, however, can do this by itself, without essential limits apart from those of computability and provability.
Quite a few people seem to think that the undecidability of many problems should worry us, but it shouldn't - what's unprovable is simply out of reach for both GMs and humans. Related questions are addressed in a recent FAQ list: http://www.idsia.ch/~juergen/gmfaq.html
Best regards, JS
-------
To unsubscribe, change your address, or temporarily deactivate your subscription, please go to http://v2.listbox.com/member/[EMAIL PROTECTED]
