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 

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



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