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 everything-list.domain.name.hidden
To unsubscribe from this group, send email to everything-list-unsubscribe.domain.name.hidden
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en
-~----------~----~----~----~------~----~------~--~---
Received on Thu May 31 2007 - 10:23:18 PDT