--- On Sat, 10/18/08, Abram Demski <[EMAIL PROTECTED]> wrote: > No, I do not claim that computer theorem-provers cannot > prove Goedel's Theorem. It has been done. The objection applies > specifically to AIXI-- AIXI cannot prove goedel's theorem.
Yes it can. It just can't understand its own proof in the sense of Tarski's undefinability theorem. Construct a "predictive" AIXI environment as follows: the environment output symbol does not depend on anything the agent does. However, the agent receives a reward when its output symbol matches the next symbol input from the environment. Thus, the environment can be modeled as a string that the agent has the goal of compressing. Now encode in the environment a series of theorems followed by their proofs. Since proofs can be mechanically checked, and therefore found given enough time (if the proof exists), then the optimal strategy for the agent, according to AIXI is to guess that the environment receives as input a series of theorems and that the environment then proves them and outputs the proof. AIXI then replicates its guess, thus correctly predicting the proofs and maximizing its reward. To prove Goedel's theorem, we simply encode it into the environment after a series of other theorems and their proofs. -- Matt Mahoney, [EMAIL PROTECTED] ------------------------------------------- agi Archives: https://www.listbox.com/member/archive/303/=now RSS Feed: https://www.listbox.com/member/archive/rss/303/ Modify Your Subscription: https://www.listbox.com/member/?member_id=8660244&id_secret=117534816-b15a34 Powered by Listbox: http://www.listbox.com
