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 thecore of your thesis - the "Interview with the Universal LobianMachine".

`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 havebeen downloading it since 2003. I have not yet come across any info onwhat 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/