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 
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 
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 



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 

Reply via email to