On 9/14/06, Shane Legg <[EMAIL PROTECTED]> wrote:
On 9/14/06, Nick Hay <[EMAIL PROTECTED]> wrote:
> On 9/13/06, Ben Goertzel <[EMAIL PROTECTED]> wrote:
>
> > The basic problem as many have noted is Godelian. Chaitin's version
> > of Godel's Theorem says "You can't prove a 20 pound theorem with a 10
> > pound axiom system." We humans cannot prove theorems about things
> > that are massively more algorithmically complex than ourselves.
>
> That's not true. A trivial example: very simple number theories can
> prove "n = n" for any value of n, no matter how large. In particular
> for extremely complex n.
>
> More interestingly, we can prove some things about the behaviour of
> sufficiently simple programs no matter how complex their input is.
You're both right. Ben's quote is a famous one made my Chaitin,
see
http://www.cs.auckland.ac.nz/CDMTCS/chaitin/georgia.html
The problem is with how you define the "weight" of a theorem.
In this context "weight" means that the theorem itself contains a
large amount of algorithmic information, i.e. has a high Kolmogorov
complexity. Thus "x=x" is a very "light" theorem in this sense.
How is this weight defined, or is it informal? In what precise sense
does "3242356630320032482384029350=3242356630330032482384029350" lack
a large amount of algorithmic information [insert appropriately
complex natural number to suit]. Does this measure also say that
"H(x) > n" and G the Goedel statement of a system have large amounts
of algorithmic information explaining their undecidability?
Calude has shown (I think) that the measure d(x) = H(x) - |x| is such
a valid measure i.e a (sufficently powerful?) system cannot prove any
theorems with d(x) > k for some fixed k. However, I don't understand
how this is a very interesting measure e.g. how it corresponds to a
theorem's "weight".
(For Calude et al's work see http://www.cs.auckland.ac.nz/~cristian/aam.pdf)
The key question is, what would a friendliness theorem be about?
I don't know what kinds of theorems you would prove about these systems.
That said, some theorems could be like machine verification proofs
e.g. that a microprocessor implements floating point operations
correctly. More generally that a particular tractable implemenation
statisifies a given abstract specification. This is a question about
the code in isolation, not the entire universe.
This gives us some added degree of confidence in correctness: if the
computer works, and the abstract specification is correct, the code is
correct too. This doesn't prove the specification correct, of course,
and this "proof" may require less formal reasoning. But proving the
code fits the specification is an improvement in
reliability/safety/etc!
Would it be about a function where the data that goes into and out of
it aren't important? For example, "x=x". Or would it be a theorem about
the complete system of the AGI *and* universe that it interacts with?
A theorem about the complete system + the universe can be "light" if
it's general e.g. proving a multiplication program works in any
universe where the computer stays intact. In this case you don't have
to have a simple theory describing this particular location in our
universe. Unfortunately I can't think of a less trivial example just
yet.
Can you give some examples of theorems about AGI + universe which are
too "heavy" to reasonably prove?
If it is the latter, then the theorem will have to be very heavy, unless
you can come up with a simple theory to explain the universe. As
Chaitin points out, theorems that are "heavy" in this sense cannot
be proven due to Gödel incompleteness.
I don't see the result in the above link. Do you have a precise
statement of the theorem?
-- Nick Hay
Shane
________________________________
This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe
or change your options, please go to:
http://v2.listbox.com/member/[EMAIL PROTECTED]
-----
This list is sponsored by AGIRI: http://www.agiri.org/email
To unsubscribe or change your options, please go to:
http://v2.listbox.com/member/[EMAIL PROTECTED]
