Le 30-mai-07, à 16:00, Bruno Marchal a écrit :
> > > Le 29-mai-07, à 07:31, Russell Standish a écrit : > >> >> 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. > > > This is due probably because they have not been conceived in that > spirit. Of course when I say that the machine or the theorem prover for PA is self-aware, you have to keep in mind the whole background of the comp assumption, including the main movie-graph consequence which forbids to attach consciousness to any "spatio-temporal-physical activity". PA consciousness is de-localized and distributed in *all* the LRA or UD computations, and it is arguable that any of your own present consciousness is already part of many PA's life (even without comp, you *do* extend PA. ("you" = all of you, not just Russell Standish!). Locally PA's awareness is just the fact that when PA proves p soon or later PA proves Bew('p'), (which I write "modally" as Bp). Now even the UD, or LRA (little robinson arithmetic) are aware in that sense. PA's self-awareness is the fact that for any arithmetical p, PA proves Bp -> BBp. LRA definitely lack that self-awareness. Both LRA and PA are under the consequences of incompleteness, but only PA and its sound logical descendants can overcome it. Actually the mathematical capture of the Universal Dovetailer Argument (UDA) or of Plotinus, can be appreciated without any ontological assumption, and should please to positivist and formalist. On the contrary the original UDA itself asks for some non mathematical assumption like the "yes doctor", and can please only through some (minimal) arithmetical-platonist and cognitive assumptions. Of course I do believe all lobian machine are self-aware in that sense. And thanks to their lack of (human? Aristotelian?) prejudices, they appear to be very close to Plotinus when they describe what they discover by looking inward. In a sense PA, ZF, ... are more self-aware than us ... perhaps more in this time where self-reflection seems to be a bit out of fashion ... I think this is in part due to the mixing of theology religion and politics, where the doubting attitude is discouraged ... (other but related debate). 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 -~----------~----~----~----~------~----~------~--~---