Matt, I suppose you don't care about Steve's "do not comment" request? Oh well, I want to discuss this anyway. 'Tis why I posted in the first place.
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. More generally, all AIXI's world-models are computable. What do I mean when I say "to reason about non-computable entities"? Well, Goedel's Incompleteness Theorem is a fine example. Another example is the way humans can talk about whether a particular program will halt. This sort of thing can be done in logical systems by adding basic non-computable primitives. A common choice is to add numbers. (Numbers may seem like the prototypical computable thing, but any logic of numbers is incomplete, as Goedel showed of course.) The broader issue is that *in general* given any ideal model of intelligence similar to AIXI, with a logically defined class of world-models, it will be possible to point out something that the intelligence cannot possibly reason about-- namely, its own semantics. This follows from Tarski's indefinability theorem, and hinges on a few assumptions about the meaning of "logically defined". I am not altogether sure that the Novamente/OCP design is really an approximation of AIXI anyway, *but* I think it is a serious concern. If the Novamente/OCP design really solves the (broader) problem, then it also solves some key problems in epistemology (specifically, in formal theories of truth), so it would be very interesting to see it worked out in these terms. --Abram On Sat, Oct 18, 2008 at 9:12 PM, Matt Mahoney <[EMAIL PROTECTED]> wrote: > --- On Sat, 10/18/08, Abram Demski <[EMAIL PROTECTED]> wrote: > >> Non-Constructive Logic: Any AI method that approximates AIXI >> will lack the human capability to reason about non-computable >> entities. > > Then how is it that humans can do it? According to the AIXI theorem, if we > can do this, it makes us less able to achieve our goals because AIXI is > provably optimal. > > Exactly what do you mean by "reason about" non-computable entities? > > Do you claim that a computer could not discover a proof of Goedel's > incompleteness theorem by brute force search? > > -- 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/?member_id=8660244&id_secret=117534816-b15a34 Powered by Listbox: http://www.listbox.com
