On Tue, May 29, 2007 at 03:05:52PM +0200, Bruno Marchal wrote: > > > 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).
No it wasn't clear. Also theorem proving software exists already in the real world, and has been used to validate elementary circuit design. Unfortunately, more complicated circuits such as Pentium processors are beyond these programs. But I've never heard of anyone considering these programs self-aware before. > 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). I will try to borrow a copy of this book to read his justification. These definitions you give are not at all obvious. Sydney Uni has a copy in its library - unfortunately there is a bit of administrative hassle for me to organise borrowing priveleges there. > 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). Well this is different from me. I don't believe the theatetical definitions are wrong as such, I just don't really understand their justification. If it were a question of terminology, I could happily call it "Theatetical knowledge", and prove all sorts of wonderful results about it, but still never know what it corresponds to in the real world. Maybe Smullyan has some justification for this? > > ....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 This is exactly what I meant. Time for me is subjective (unless one is talking about coordinate time, which one does in physics, but is not what we're talking about here). > first-person hypostasis (the one given by the theaetetical definition > of knowability) has a temporal-intuitionistic logical semantics. This is the point I never understood. Something about it "quacks like a duck", so must therefore be a duck? > 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. > > > > > 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. > Fontana had a paper about this at the Brussels ECAL, which you attended IIRC. I missed the Brussels ECAL due to having to return to Australia before it (I was living in Germany in 1992), otherwise I would have been there. I remember feeling very disappointed about it. Speroni di Fenizio builds on Fontana's model in several important respects, but is certainly in that tradition. > > Bruno > > > > > http://iridia.ulb.ac.be/~marchal/ > > > > -- ---------------------------------------------------------------------------- A/Prof Russell Standish Phone 0425 253119 (mobile) Mathematics UNSW SYDNEY 2052 [EMAIL PROTECTED] Australia http://www.hpcoders.com.au ---------------------------------------------------------------------------- --~--~---------~--~----~------------~-------~--~----~ 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 -~----------~----~----~----~------~----~------~--~---