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.
>
>> 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?
Actually Smullyan use the Theaetical definition without going in any
details. He just say that he will say that a machine believes p when
the machine asserts p, and that the machine knows p when both p is true
and the machine asserts p.
More involved explanations and critics occur in the original Theaetetus
by Plato, and all along the philosophical litterature.
Wittgenstein makes a case in his late writing for it when he realize
that knowledge and beliefs could corresponds to the same mental state
in different context.
What is really not obvious at all, is that the theaetical definition
works for the provability of correct machine. Why? Because obviously if
the machine is correct then Bp and Bp & p are obviously equivalent. The
key is that this equivalence cannot be proved or asserted by the
machine, because no correct (lobian) machine can ever know being
correct. She would know that Bp -> p, and in particular she would know
that Bf -> f, that is ~Bf, that is: she would know that she is
consistent, contradicting Godel II.
Same reasoning for all the hypostases: they are all equivalent, in term
of provability or assertability, but yet, from the machine point of
view, they obey drastically different logics.
>
>
>>> ....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?
It is know that intuitionistic logic has a temporal flavor, and this is
nice from the point of view of informal intuitionistic philosophy which
is already a theory of "subjective time" à-la Bergson or Brouwer.
Now, Godel already suggested in 1933 (and btw Kolmogorov discovered
this in 1932) that the modal logic S4 provides an epistemic
interpretation of intuitionistic logic. Godel suggests to translate
intuitionistic logic in the (classical) modal logic S4 by using the
following recursive translation t_int:
t_int(p ) = Bp (atmic p)
t_int(~p) = ~B(t_int(p))
t_int(p -> q) = B(t_int(p) -> B(t_int(q)
t_int(p & q) = t_int(p) & t_int(q)
t_int(p V q) = B(t_int(p) V B(t_int(q)
McKinsey and Tarski will prove this works well later, and Grzegorczyk
will extend that result for S4Grz (that is S4 + the Grz formula). In
the Kripke frame, the Grz makes the accessibility relation
antisymmetrical, making this even more palatable for a theory of
subjective sense.
This is related to G, because as Boolos, Goldblatt (and also Kusnetzov
and Muravitsky in the ex-soviet union) will show that S4grz is sound
and complete for the provability-and-truth notion, that is for the
application of theatetus to provability. I have extend this with the
"weaker" provability-and-consistency, and
provability-and-consistency-and-truth, etc.
Gosh, I realize the translation above is more correct than the one I
put in my Plotinus (SIENA) paper. I always put typo errors ... Hmmm...
I will try a succinct summary of the arithmetical interpretations of
the Plotinian hypostases. Good preparation for me, indeed I have 20m in
Sienna to sum up years and years of work, not counting the work of the
many multi-disciplinay predecessors! But at least in Siena the
audience is suspected to know logic, and seems very open minded for
"less-logical things" ...
Hope I have not been too technical for the non technical people. I
really recommend the reading of Plato's Theatetus for the best
introduction to the arithmetical hypostases appearing when we interview
universal machines.
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 Wed May 30 2007 - 10:00:33 PDT