On 15 Feb 2009, at 23:00, russell standish wrote:

## Advertising

> > On Sun, Feb 15, 2009 at 06:41:08PM +0100, Bruno Marchal wrote: >>>> >>>> A good and important exercise is to understand that with the Kripke >>>> semantics, ~Dt, that is B~t, that is Bf, that is "I prove 0=1", is >>>> automatically true in all cul-de-sac world. It is important because >>>> cul-de-sac worlds exists everywhere in the Kripke semantics of the >>>> self-reference logic G. >>>> >>>> If you interpret, if only for the fun, the worlds as state of life, >>>> then Bf is really "I am dead". >>>> >>>> Bruno >>> >>> Yes, but I have difficulty in _simultaneously_ interpreting logic >>> formulae in terms of Kripke frames and B as provability. In the >>> former, Bp means in all successor worlds, p is true, whereas in the >>> latter it means I can prove that p is true. >>> >>> How does one reconcile such disparate notions? >> >> >> By Godel's theorems, Löb's theorems and Solovay theorems. >> > > ... > > The following snip did not answer my question on how one can > simultaneously have Kripke semantics and provability semantics. Never > mind. It is technical. It just happen that the logic of the self- referential, or Gödelian Beweisbar provability predicate is completely and soundly axiomatized by the modal logic G and G*. And the modal logic G belongs to the type of logic which possesses a characterization in term of a Kripke semantics. (note that G* losses the Kripke semantics). > > > I'm helping Kim Jones with the translation - maybe it'll make more > sense when we get to that bit. Thanks for helping. I will think about how to explain AUDA in simple terms. UDA shows that physics is in your head. AUDA shows that physics is in the head of any universal digital machine. This transforms the mind-body problem into a pure mathematical problem, or sequence of mathematical problems. Then we can compare the physics in the head of the machine and physics "out there", and so we can test the comp hyp. Let me give a short try, for helping to answer your question of the reconciliation of Kripke multiverse and provability. It is standard material. Godel's second incompleteness theorem 1931 says that if the formal system Principia Mathematica PM is consistent then PM cannot prove that PM is consistent. Gödel did already completely understand that PM was able to prove its own incompleteness theorem (although the detailed proof will be given by Bernays and Hilbert later (and then brillantly simplified by Löb)). PM can prove that if PM is consistent then PM cannot prove that PM is consistent. More simply: PM proves that "IF I am consistent, then I cannot prove that I am consistent": PM proves NOT(BEWEISBAR(FALSE)) -> NOT(BEWEISBAR(NOT(BEWEISBAR(FALSE))) where BEWEISBAR is Gödel's 1931 provability predicate, and FALSE is some Gödel number representing the statement "0 = 1" in PM language. The whole is a first order arithmetical sentence. Now that first order arithmetical sentence look like a modal statement. Writing NOT with "~", BEWEISBAR with a box "B", and FALSE with f, the formal, that is really the one output by the machine or by the formal system becomes ~Bf -> ~B~Bf or with the diamond (B~p is equivalent with ~Dp, and D~p is equivalent with ~Bp). t is ~f. Dt -> DBf, which provides the reading that "If I am consistent then it is consistent that I am inconsistent". Already here, given that this is a modal statement, it is natural to ask oneself if there is a Kripke "multiverse" satisfying that modal statement. A Kripke multiverse satisfies a statement when the statement is true in all worlds of the multiverse. A multiverse here is just a set of worlds with an accessibility relation. How to find an accessibility relation making the statement "Dt -> DBf" true in all worlds of a multiverse? If Dt is true in a world ALPHA, say, you need to have DBf true in that world ALPHA too (you want "Dt -> DBf" true everywhere!). But to have DBf true in ALPHA, you have to be able to access (by the accessibility relation) a world where Bf is true. (By the definition of Kripke semantics). But Bf can be true only in cul-de-sac worlds (if not f would be true in some world). So ti have Dt->~BDt, or Dt->DBf, you have to live in what I called a Papaioannou multiverse, or a realist multiverse (in Conscience et Mecanisme), that is a multiverse where all worlds have an access to a culd-de-sac world. The same remains for the generalisation Dp -> ~BDp (equivalently Dp -> DB~p). Now, if you remember that ~p is equivalent to p -> f (or redo the two lines truth table), you can write consistency, Dt, that ~Bf as Bf->f, by simple transformations: ~Bf -> ~B~Bf is equivalent with B~Bf -> Bf by contraposition. And this is equivalent (by Bf equivalent with Bf -> f). B(Bf->f)->Bf The generalization (f/p) of this formula gives the Löb formula B(Bp- >p)->Bp, which is the formal (machine) version of the theorem of Löb, which indeed says that if PM proves BEWEISBAR('p') -> p then PM proves p. (Curiously enough, Boolos 1993 gives five reasons to be astonished!). See the arithmetical placebo in the same2004, or the "proof" of the existence of Santa Klaus, in the archive or Bools' books, or better Smullyan which varies about that theme in Forever Undecided. Solovay shows that in the normal modal logics, Löb's formula, B(Bp->p)- >Bp, axiomatizes completely the logic (G) of provabilty. Now B(Bp->p)->Bp has more complex Kripke semantics, but one of them is given by the finite transitive irreflexive multiverse. You can verify this by hand on simple examples. Not only you have always access to dead end (cul-de-sac world), but all your path end somewhere. In term of life (which fortunately will NOT concern the first person), not only you can die at each "om", but you will eventually die. But as I say, and Torkel Franzen did see something similar here, the G world are not "OMs"; the G logic is really third person self-reference (its modal world are not OMs: it is more a logic of scientific communication than a logic a first person knowledge. The amazing things which I exploit, is that we can study the logic of the first person knowledge attached to the machine, despite it can be shown that the first person is not definable by the machine, or by PM, PA, ZF, whatever rich classical theory or Löbian machine. You cannot define the notion of first person, or of consciousness, or even the notion of Truth in the language of any (consistent) machines. Yet machines can reason about those notion indirectly. The trick is already in the Theaetetus of Plato, or even used by Plotinus (as Bréhier, the first french translator of Plotinus, suggested). All this will concern all the mechanical or less mechanical consistent extensions of those machine or theories. Hope this gives some clues. I guess we can come back on this. AUDA is technical for sure. G and G* is just two hypostases, but the others come from them. 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-l...@googlegroups.com To unsubscribe from this group, send email to everything-list+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/everything-list?hl=en -~----------~----~----~----~------~----~------~--~---