But: it seems to me that, in the same sense that AIXI is incapable of "understanding" proofs about uncomputable numbers, **so are we humans** ...
On Sun, Oct 19, 2008 at 6:30 PM, Abram Demski <[EMAIL PROTECTED]> wrote: > Matt, > > Yes, that is completely true. I should have worded myself more clearly. > > Ben, > > Matt has sorted out the mistake you are referring to. What I meant was > that AIXI is incapable of understanding the proof, not that it is > incapable of producing it. Another way of describing it: AIXI could > learn to accurately mimic the way humans talk about uncomputable > entities, but it would never invent these things on its own. > > --Abram > > On Sun, Oct 19, 2008 at 4:32 PM, Matt Mahoney <[EMAIL PROTECTED]> > wrote: > > --- 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/?&; > > Powered by Listbox: http://www.listbox.com > > > > > ------------------------------------------- > 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/?&; > Powered by Listbox: http://www.listbox.com > -- Ben Goertzel, PhD CEO, Novamente LLC and Biomind LLC Director of Research, SIAI [EMAIL PROTECTED] "Nothing will ever be attempted if all possible objections must be first overcome " - Dr Samuel Johnson ------------------------------------------- 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
