On 9 May 2014 05:07, Bruno Marchal <[email protected]> wrote: > > On 08 May 2014, at 00:35, LizR wrote: > (By the way I think Max Tegmark does a good job of explaining what this > means in his book, even if he doesn't get to the reversal. He says you need > to assume a "capsule theory of memory" and talks about observer moments a > lot, which hammers home the point that any given OM could be instantiated > in a computer, in a Boltzmann brain, in arithmetic etc. > > In arithmetic? >
Or Platonia, or wherever it is the UD lives. > > (to me the term OM is ambiguous, and people confuses easily first person > OM, which I think don't really exist or make sense, and third person OM, > which are "just" relative computational state). > > OK, well this could get confusing then! I forget how Max Tegmark defines an OM in the book. I think probably fairly informally. It seems to me that if consciousness is somehow produced by computation then it has to have states and steps between them, and an OM might be a state. However I admit I don't know what an OM is, and some might say the brain operates on a 1/10th of a second cycle or similar, and hence an OM is quite a long time compared to the possible underlying computational steps. > I think if one doesn't get that point then the steps seem a lot less > intuitive. I just mention this FWIW. I haven't quite finished his book yet > but in places it seems like (Max's version of ) comp for dummies, which is > probably the right level for me) > > Nice. > > >> Now, the machine which believe/assume elementary arithmetic (and perhaps >> more as long as they remain arithmetically sound), will have its rational >> believability notion acquires a non trivial modal logic, known today as G >> (or GL, PrL, KW4, it has some story so get many names). >> >> Actually the machines acquire a couple of logics: G and G*. G is the >> logic of provability (believability) that the machine can believe, and G* >> is the logic of believability (that the machine can believe or not, and >> indeed G* extends properly G. >> > > OK, this is what you lost me! What are G and G* again? (Sorry!) > > Well, we have seen some modal formula, and their Kripke semantic. > > But logicians are not interested in only formula, but in theories, and > notably modal logicians study modal theories. > > Classical modal logicians, as you can guess study classical modal > theories, and this means that they study modal theories (given by some > modal formulas) extending classical propositional logic. > > If you remember, I gave you an axiomatization of classical propositional > logic. It was a finite set of classical propositional formula, and > inference rules, such that all classical tautologies are provable from > them. it was the following system. > > It is the infinities of formula having the following shapes with A for any > formal formula (that is p, s, r, ... and their boolean combinations): > > (A -> (B -> A)) > ((A -> (B -> C)) -> ((A -> B) -> (A -> C))) > (((~B) -> (~A))) -> (((~B) -> A) -> B)) > > You can see, by using the truth table semantic that those are tautologies. > > The inference rule (the only means beyond substitution of A, B, C for > formal formula (like p, q, (p & (p V q)), (p -> (p -> p)), ..), is the > modus ponens rule. > > From A and (A -> B) you can derive B. > > I gave you a proof of (A -> A) as an example, and important theorem. > > I hope you can see that the inference rules preserves tautologicalness. If > A is a tautology (true in all valuations of the atomic formula, p, q, r, > ...; has only "one" in its truth table), and if (A -> B) is a tautology, > then B is a tautology. OK? > > And that theory can be shown to be complete. All tautologies are provable. > > The key notion here is "provable". "A is provable" means that there is a > sequence of formulas, which are either axioms, or are formula derived from > the modus ponens rule from preceding formula in the sequence, ending to A. > > Well, it is exactly the same for the modal theories, except that we allow > modal formulas. > > Let me remind you that the following formula, called K, for Kripke, is > respected in all multiverses, where a multiverse is a set of "worlds", > together with a binary relation, called accessibility relation. I leave the > outer parentheses for reason or readibility. > > K is [](A -> B) -> ([]A -> []B) > > The proof is simple. If there is a world alpha with both [](A -> B) and > []A, but with []B false, contradicting K, > then in all beta such that (alpha R beta) you would have (A -> B) and A, > but ~B, which is impossible (the world obeys classical logic). > > So, all theories having a Kripke semantics have K has axiom. All the modal > logical theories which will interest us (to derive phsyics and theology > from machine's self-reference) will extend that theory. > > But note this: imagine that A is respected in a multiverse (or just > satisfied by one illuminated multiverse, its atomic formula are valued on 1 > or 0), then A is true in all worlds, but then []A has to be true in all > worlds too! > > This means that the following rule of inference: > > from A derive []A > > will preserve the modal tautologicalness (satisfaction in illuminated > multiverse, respect by multiverse). And so is a sound rule of inference. > > So all modal theories (having Kripke semantics) have the two following > rules of inference: > > Modus ponens: from A and (A -> B) you can derive B. > > and > > Necessitation rule: from A, you can derive []A. > > Definition: I will say that a modal theory is *normal*, if it has the > axiom K, that is [](A -> B) -> ([]A -> []B), and if has the modus ponens > inference rule and the necessitation inference rule. > > Let us give names to the formula so that we can describe a normal theory > in a simple way, without retyping complex formula: > > K = [](A -> B) -> ([]A -> []B) > > T = []A -> A > > 4 = []A -> [][]A > > 5 = <>A -> []<>A > > C = <>A -> ~[]<>A > > B = A -> []<>A > > L = []([]A -> A) -> []A > > Grz = []([](A -> []A) -> A) -> A > > All OK so far. > > Typical normal theories are KT, KT4 (known as S4), KT45 (known as S5, the > Leibnizian theory), KTB (the Brouwersche system), KD (deontic logic). > What is D? > > Now, I answer your question: > > G is KL = KL4 > > So G is the theory with axiom > > [](A -> B) -> ([]A -> []B) > []([]A -> A) -> []A > > (4 is derivable from that theory, I might show you this one day. The > Kripke semantics of G is slightly more complex, and two different semantics > are often used. In fact G characterize the finite multiverse with an > irreflexive transitive accessibility relations), but also the class of > multiverse without any infinite path a R b, b R c, c R d, .... (those are > variable for worlds and can be equal, and so this entails irreflexivity). > > Why is G so important? > > By Solovay completeness theorem, G provides the logic of machine > self-reference. It characterizes the logic of what a machine, rich enough > to understand how a machine work, and classical logic, can prove about its > own provability ability. > > G is the logic of arithmetically sound machine provability and its dual, > consistency. > > Cf the "crux of the matter", the Gödel translation of "provable" in > arithmetic. > > > Let me sum up the sequel, and the representation theorems, in a roughly > non rigorous way, to avoid details and give the idea. > > QL is for Quantum logic. It is the logic of quantum mechanics, with the > atomic formula being interpreted by rays in Hilbert spaces and, arbitrary > propositions by subpaces of an Hilbert space. > > B proves R(A) iff QL proves A (where B is the normal theory KTB) > G proves R2(A) iff B proves A > Now I'm lost again. What is R, R2? (etc ... I see more of these below but I will snip the rest to avoid my post having a long tail...) > > PS I wrote this thursday morning, but I can't send any mail. Apparently > this time my computer is not involved, looks like the provider has some > problem. 18h52 Hurray! I heard the mail sending. I send this one, as I have > to go. > > I hope you get your mail sorted out soon (for both our sakes!) -- 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.
