Le 26-mai-07, à 22:32, Russell Standish a écrit : > > On Fri, May 25, 2007 at 04:00:40PM +0200, Bruno Marchal wrote: >> >> >> Le 25-mai-07, à 04:12, Russell Standish a écrit : >> >>> I don't think anyone yet has managed a self aware formal system, >> >> I would say all my work is about that. You can interpret Godel's >> theorem, or more exactly the fact that machine can prove their own >> provability logic, and even guess correctly the true but non provable >> part, as a general statement of self-awareness. Sometimes, >> self-awareness is defined more precisely by the "4" modal formula: Bp >> -> BBp. This is a theorem for PA, but not for LRA. >> When LRA proves p, then soon or later, if not already, LRA will prove >> Bp (that is LRA will prove that she prove p). So Bp -> BBp is true for >> LRA, but only PA can prove such a proposition on itself. >> > > Absolutely your work is all about that. And constructing a formal > self-aware system will just as likely come from an approach like > yours as anything else. My only statement was that it hasn't been done > already, and certainly I wasn't aware of you claiming self-awareness > already.

## Advertising

Of course many things depends on definitions, but I thought it was clear that I consider that any theorem prover machine, for a theory like ZF or PA, is already self-aware. And of course such theorem prover already exist (not just in platonia). The "interview" of the lobian machine has already begun, through the papers of Godel, Lob, ... Then Solovay's results have captured, through the modal logic G and G*, the whole (infinite) conversation we can have with and about such machines (G gives (self-) science and G* gives the (self) correct hope/bet/interrogation/theology). The technical part of my thesis is really the *result* of the interview of such self-aware (and even aware of being self-aware) machine. But frankly I am glad with Smullyan (rather classical) definition of self-awareness in his little book "FOREVER UNDECIDED": A machine M is self-aware if, having proved p, she will prove soon or later if not already, Bp. A machine M is self-aware of its self-awareness if for any p she proves Bp -> BBp (that is: she knows the preceding line for any proposition p). No need to put too much philosophy here, it could be prematured. As a platonist (or just mathematician), no need to have the interview with an "incarnate" machine, we can stay in Platonia, where such machine and their interviews exist out of space and time. That is good given that the goal (made necessary by the UDA) is to derived the structure of space and time from the interview! But yes, indeed I consider already PA or ZF as person, and this with or without terrestrial local implementations. > Admittedly, I miss some of the conclusions you do make, such as the > Theatetic axioms encapsulating knowledge, ... I remember. You said some times ago that the definition of knowledge of P (Kp) by true justified opinion (Bp & p) is debatable, and you are right; it is somehow debated since, well, a very long time, and in many places: China, India, Greece up to Plato. I postpone a bit a debate on that. Note that this idea is used implicitly at step 6 of the Universal Dovetailer Argument. It is related to the use of dream in metaphysics. And such a definition has to be nuanced, at least if we trust Socrate's critics of Theatetus, or Plotinus or ... the lobian machine itself!!! Indeed, by incompleteness we have the new Bp & Dp nuances, and we have the Bp & Dp & p nuances, etc. Actually those who criticize the definition of knowledge by "Bp & p" have to maintain that they are able to distinguish their dream and awakeness states. But with comp, the thought experiments (or their arithmetical godelian translation) show that we cannot, locally, or in a bounded finite time, make that distinction. This explains why a philosopher like Malcolm (ref in my thesis), who reasons very rigorously, and who believes the theaetetical definition of knowledge is wrong, is forced both to disbelieve in comp, and to disbelieve in consciousness in dreams (like with lucidity, but not necessarily). Very interestingly, Barnes (ref in my theses) makes a similar move to escape Maudlin's "~ comp or ~ materialism" argument. I am writing (albeit slowly) a paper on that for the journal of philosophy as a rejoinder to Maudlin and Barnes. We can come back on this later. > ....and also Kripke frames being > the phenomena of time (I can see that they could be a model of time, > but that is another thing entirely). I don't remember having said that "Kripke frames" *are* the phenomena of times? What would that means? All I say is that assuming comp (well the weak acomp) then the soul or the first person generates its subjective time, and that this is confirmed by the fact that the first-person hypostasis (the one given by the theaetetical definition of knowability) has a temporal-intuitionistic logical semantics. That this corresponds on the "real subjective time" for the self-observing machine already follows from the UDA, where 1) comp-practitioners does not modelize their brain with an artificial one, but really accept it as a new brain + 2) the non distinction between "real", virtual and arithmetical. >> >>> although self-reproducing systems have been known since the 1950s, >>> and >>> are popularly encountered in the form of computer viruses. >> >> The principle is really the same. That is what I show in my paper >> "amoeba, planaria, and dreaming machine". self-reproduction and >> self-awareness are a consequence of the closure of the set of partial >> computable function for the daigonalization procedure. >> > > Incidently, I read your Elsevier paper the other day. It has inspired > me to take a look at combinators for artificial life applications. I > discovered that Pietro Speroni di Fenizio has spent a PhD looking at > this. He was a student of Walter Banzhaf and Peter Dittrich - I met > Walter shortly before I caught up with you in Brussels in 2003. Peter > I met in the Lausanne ECAL in 1999. Are you aware of any of this work? > AFACT, he never achieved self-reproduction, which is a precursor to > evolution, but alas he didn't publish any of his code. Thanks for the information. I didn't know him. But I know the work by Fontana and some of its followers in Artificial Chemistry, and which is based on lambda calculus (the little cousin of combinatory logic). Lambda expressions and combinators are very useful to analyze computation with some fine graining (as my Elsevier paper illustrates a bit). But theology needs more the notion of computability (which is independent of the choice of formal systems) than the notion of computation, which is far more involved. Of course there are some links. Bruno http://iridia.ulb.ac.be/~marchal/ --~--~---------~--~----~------------~-------~--~----~ You received this message because you are subscribed to the Google Groups "Everything List" group. To post to this group, send email to [EMAIL PROTECTED] To unsubscribe from this group, send email to [EMAIL PROTECTED] For more options, visit this group at http://groups.google.com/group/everything-list?hl=en -~----------~----~----~----~------~----~------~--~---