Hi Kim,
Le 27-déc.-05, ŕ 01:06, Kim Jones a écrit :
> for some time now you have been building up to what appears to be the
> core of your thesis - the "Interview with the Universal Lobian
> Machine".
OK. I would say that there is really two cores in my thesis. The
Universal Dovetailer Argument (UDA), and the interview of the Lobian
Machine.
- The UDA is an informal (but I think definite and rigourous) argument
showing that if we believe that we are (digitalisable) machine (comp)
then we should believe that the laws of physics (the laws of observable
predictions) are derivable from computer science/ machine's
psychology/machine theology/number theory (cf the naming issue). The
whole of physics must be derivable: this includes space, time,
constants, etc. The UDA does presuppose some amount of folk psychology
for making sense to the expression "yes doctor", when the doctor
proposes to *you* an artificial digital brain.
- The interview of the lobian machine is just what logicians call "the
logic of provability", or "the logic of consistency" or "the logic of
arithmetical self-reference". Such an interview has begun when Godel
discovered the gap between provability *by* or *in* a formal system
(like PRINCIPIA MATHEMATICA, or PEANO ARITHMETICS, or ZERMELO-FRAENKEL
SET THEORY, to name typical examples) and truth *about* such a formal
system.
I identify such "theories" with their theorem provers (all
axiomatisable theory have some canonical theorem prover capable of
generating all their proofs).
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).
Now, all the (self)-references here are third person references, and
the UDA has shown that physics appears within first person
self-references. Tomorrow I will explain how to get first person
notions from third person references. The key ideas appear already in
Plato.
Tell me if all this helps you, and don't hesitate to ask ANY questions.
> I've processed the concepts emerging from this discussion - and I have
> been downloading it since 2003. I have not yet come across any info on
> what the Lobian machine interview reveals.
I think you could find many earlier posts of mine on G and G*. But it
is ok I re-explain. The archive "escribe" seems to be dead, and I
should correct some links in my web pages.
Best,
Bruno
http://iridia.ulb.ac.be/~marchal/
Received on Tue Dec 27 2005 - 11:07:07 PST