[extropy-chat] Victoria News: Singularitarians in the City of Gardens

[Marc Geddes]

There are all sorts of wonderful things happening all
over the world as regard AI development - I about them
every day in the news lists, journals etc.  Check out
the wonderful list of links I recently compiled:

http://www.agiri.org/forum/index.php?showtopic=108&pid=182&st=0&#entry182

There are tens of thousands of hobbyists working on AI
all the time all over the world and new projects
popping up everywhere.  

Whilst there's probably only a hand-ful of people
really 'in the know', what the 'leading edge' thinkers
actually do know is really no secret.  There's plenty
of info available in open-source journals.  For
instance check out these Bayesian papers at the Center
for the Study of Rationality (The Hebrew University of
Jerusalem) here:

http://www.ratio.huji.ac.il/dp.asp

The sort of things that would need to be done in
mathematical logic to create AGI are also no secret. 
The importance of Godel's theorem , Lob's theorem and
Solovay theorem are not a secret.  

"In 1931 Godel discovered the existence of true but
unprovable propositions in all such systems/machines.
The most typical true but unprovable proposition
(unprovable by the machine/theory) is the consistency
assertion: "I am consistent". A machine or a theory is
said to be consistent if the theory or the machine
does not prove false proposition. That is: 
PA cannot prove the true proposition that PA is
consistent.
ZF cannot prove the true proposition asserting that ZF
is consistent.
Note that nobody doubt that PA is consistent. In the
case of ZF this is slightly less obvious (but I will
suppose so, and in any case, I will deliberately limit
myself on the discourse of consistent machines). The
general Godel's result, known as Godel's second
incompleteness theorem, is that no consistent machine
can prove its own consistency: 

            IF M is consistent then M cannot prove its
consistency

[in modal logic, if you represent the "provability
predicate" by a modal box B, then consistency can be
written by NOT PROVABLE FALSE, or by the shorter ~Bf,
with "~" put for the "not", the "B" put for the
"provability" predicate, the "f" put for some falsity.
With such notation, and reminding that "IF pTHEN q" is
written "p -> q" by logician, Godel's second
incompleteness theorem can be written: ~Bf -> ~B(~Bf),
or remembering that ~Ba = D~a (NOT PROVABLE A =
CONSISTENT NOT A), the second theorem by Godel can be
written also with the diamond; Dt -> DBf. I guess
people see that this is the formula of my
"tiniest-theory-of-life-and-death". It is
Kripke-semantically characterised by the "Papaioannou"
multiverses.]. 

Now Godel showed that in each "sufficiently rich"
machine/theory, the provability predicate can be
defined in or by the theory/machine itself, and that
such theories/machines *can* prove their own "Godel"s
second incompleteness theorem". 

M can prove "IF M is consistent then M cannot prove
its own consistency". 

This can be written:

M can prove "IF I am consistent then I cannot prove I
am consistent"

But please note that "I" is a third person form of
self-reference, not a first person one. The machine
talk really about itself through a "scientific"
description of itself. 

I call such "sufficiently rich" machine a LOBIAN
MACHINE (Loebian, or Löbian, but "Lobian" is easier
for the e-mail). The reason is that in 1955 M. Loeb
(Löb) will prove a significant generalisation of
Godel's theorem, and here too, it can be shown that
the lobian machine can prove their own lob's theorem.
In French (I mean in English) Lob's theorem says that
if a lobian machine (PM, PA, or ZF for example) proves
Bp -> p, for some proposition p, then soon or later
the machine will prove p (if it has not been done
already). This is rather weird, because it shows that
(sufficiently rich) machines are "vulnerable" to some
placebo effect. If you prove to such a machine that if
she ever prove the existence of Santa Klaus then Santa
exists, then you already have proved the existence of
Santa Klaus to the machine. Much more on that can be
find in my paper "the origin of the physical laws". 

[modally: Lob's theorem can be written B(Bp -> p) ->
Bp (known as Lob's formula L). If you remember that
"~A" is the same as "A -> f", and if you substitute p
by f in Lob's formula, you get B(Bf -> f) -> Bf, that
is B(~Bf) -> Bf, and if you remember that A -> B is
equivalent with ~B -> ~A, you know that B(~Bf) -> Bf
is equivalent with ~Bf -> ~B(~Bf). So you see that
Lob's theorem is a generalization of Godel's second
incompleteness theorem. Smullyan and Parick interpret
Lob's formula as a form of super-modesty principle] 

So the interview of the lobian machine gives those
nice propositions: a sort of humility principle (if I
am consistent then I cannot prove I am consistent),
and a form of modesty principle: provability entails
truth (Bp -> p) only when p is proved. 

In 1976, Solovay shows that Lob's formula formalises
completely what the machine can prove about herself.
Like you can derived most QM proposition from the SWE,
you can derive the whole of what a machine can prove
about herself from Lob's formula. Solovay defined the
logic G. Its main assumption is the formula of Lob.
This is called Solovay Arithmetical's completeness
theorem. It is amazing at first because it is a
COMPLETENESS theorem, showing that a modal logic (G)
does capture completely what the machine can prove
about its own INCOMPLETENESS phenomenon! 

You see what the interview of the introspective
machine gives: the machine discovers its own
incompleteness, and can say non obvious fact about it.


Still more important (for our comp TOE quest) is that
Solovay will prove a second arithmetical COMPLETENESS
theorem, and that's its discovery of the modal logic
G*. G* formalises the whole incompleteness phenomenon,
i.e. not just what the machine can say about it, but
also what the machine cannot say about (without
loosing consistency). The most typical example of a
theorem in G*, and not in G, is the consistency
assertion Dt, but also all of DDt, DDDt, etc., and
also DBf, DBBf, etc. 

To sum up:
G = the discourse provable by an introspective
self-referentially correct machine. G* = the truth
*about* such introspective machine (includes the non
provable one). "

I think Eliezer thinks we're all some kind of frigging
dummies.  The behavior of the 'team' at Singularity
Institute is really quite sad.  It's actually
bordering on pathetic actually.

Like I said, there's tens of thousands of hobbyists
working it and new projects popping up everywhere.  We
don't need some arsehole sitting in an 'Institute'
thinking he's savior of the world to tell us the
answer.

Let's all work on AGI together.  We're set for many
different AI's and a plularity of 'Singularity'.








"Till shade is gone, till water is gone, into the shadow with teeth bared, screaming defiance with the last breath, to spit in Sightblinder’s eye on the last day”


		
____________________________________________________ 
Do you Yahoo!? 
Find a local business fast with Yahoo! Local Search 
http://au.local.yahoo.com