> > > > >> >> It is the p in []p & p, which makes "machine's knowledge" not definable >> in term of number and machine. S4Grz formalizable at a level, what the >> machine cannot formalize about herself (but can bet on, ...). >> >> Thanks to incompleteness, the Theaetetus' definition makes sense, and >> distinguish the knower from the rational believer for the machine. >> >> Don't hesitate to ask precision. I am very literal here: the knower is >> defined by the true believer. It is a modest definition of knowledge, and >> it is not similar with "I know for sure that", which needs some amount of >> consistency (like <>t, or <><>t, or <><><> t, etc.). >> > > What's the difference between <>t and <><>t and so on? > > > In the Kripke semantics, <>p means that you can, by starting form the > world you are in, access to another world where t is true. It means that > you are not in a cul-de-sac world. It means that you are "alive", you can > access some world. But <>t -> <>[]f. So you despite being alive, you might > be dead in that next world. That next world might be a cul-de-sac world, > where <>t is false, and thus []f is true. Now, if you are in a world where > <><>t is true, then you can access a world in which <>t is true, so that > you are still alive. > > <>t = I can access some world (t is true in all worlds), but that world > might be a cul-de-sac world. > <><>t = I can access some world where <>t is true, so from there I can > access some other world. > > Put differently: > > <>t I am alive (but can die at the next instant) > <><>t, I am alive and I can access to an instant where I am still alive. >
Ok, but it's not obvious to me how temporality (a sequence of instants) is introduced here. > > > > > > >> >> [0]p = []p, and obeys to G, and fully described by G* (at the >> propositional level). >> [1]p = []p & p, and obeys to S4Grz, >> [2]p = []p & <>t obeys and define the logic Z >> [3]p = []p & <>t & p >> > > I definitely don't understand [2]p and [3]p. > > > []p & <>t is a weakening of []p & p. Instead of asking p being true, we > ask only for p being consistent > (([]p & <>t) -> ([]p & <>p)). > > If you can prove for all p that []p -> p (like with [1]), then you can > prove for all p []p -> <>t or []p & <>p. > > So the logic of provability-and-consistency is weaker than the logic of > provability-and-truth. > > Provability and consistency avoids the probability one for the false, > which would exist if we take []p as provability. The passage []p =====> []p > & <>p, approximate the main things for a probability one. > What does "provability one" mean? > It models what the guy in Helsinki can be sure if, like drinking a cup of > coffee (in the protocol where he get a cup in both W and M). It abstract > (locally) from the cul-de-sac world. It use the bet on <>t implicit in the > yes-doctor. > I don't know about the cup of coffee protocol either, could you explain it? Thanks! Telmo. -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
