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 hpcoder.domain.name.hidden
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 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 - 19:29:53 PDT