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.
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 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 Tue May 29 2007 - 09:06:18 PDT