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.




Reply via email to