Please note there is a 40 KB size limit on messages. If you have something longer please put it up on a web site and post a link to it. I had to truncate the following post in order for it to go through.
----- Forwarded message from Marchal ----- Date: Mon, 28 May 2001 08:31:12 -0700 Subject: Re: Consistency? + Programs for G, G*, ... From: Marchal To: <[EMAIL PROTECTED]> X-Diagnostic: Diverted & unprocessed X-Diagnostic: Submission size exceeds 40000 bytes Hi Levy, I hope you have take some rest because this is a long reply :-) Still too technical without doubt, but read it carefully: perhaps it will help us to make some back and forth between on one hand the intuitive and informal (but rigorous with comp) UDA and, on the other hand its formal and counter-intuitive translation in arithmetic through G and G*. Sometimes I recall things, not for you, but for others. >Your expose in a "nutshell" is far too technical to convince me... >unfortunately I believe I would have to obtain a post grad education >in logic to appreciate your position as you state it. Post grad ? Well, perhaps ..., these days ... :-) >Yet I believe that what you are saying sounds >valid. So even though I would like to give you the prize, I'm >afraid, I'm not qualified. Damned! (but I appreciate the honesty). >However, all is not lost. I believe that your position can be >stated much more simply without having to review all of >modern logic theory. Thanks for that optimistic statement. Now, when I eliminate all the "modern logic theory" ..., well, only the UDA remains. The role of "Modern Logic" is just to give tools to tranlate UDA in the language of a sound machine (or arithmetic). I recall what's UDA for the (possible) others. The UDA (Universal Dovetailer Argument), is a thought experiment showing that the computationalist hypothesis implies a reversal between physics and (machine) psychology. The UD is a program which generates and executes all computer programs, and the UDA shows my "immediately next futur" is determined by the set of all my consistent extension emulated by the UD (or belonging to UD* as I say sometimes). The reversal occurs at both the ontological level and at the epistemological level: -Ontologically: UDA shows matter emerges on consciousness (roughly speaking: it is actually the belief in matter which emerges and interferes) -Epistemologically: Physics becomes a branch of the psychology of machine (with psychology taken in the large sense of science of consciousness, you can call that theology if you prefer. For my purpose the (double) theory of mind will be given by G and G*, see below). A version of the UDA can be found in the archive at http://www.escribe.com/science/theory/m1726.html The UDA illustrates also the incompleteness of Schmidhuberian-like TOE approach, and more generally it gives a clue on the extreme non triviality of the mind/body problem (even) with the computational hypothesis. (Some materialist believes that comp *is* the solution of the mind-body problem, alas for them, materialism is not even compatible with mechanism. This can be derived from UDA + OCCAM, or directly from the Movie Graph Argument, or from Maudlin's paper. Ref in my thesis at http://iridia.ulb.ac.be/~marchal). The UDA shows that whatever you do, the next "conscious" event has a probability uniquely determined by the set of all your consistent extensions in the UD* (= accessed by the UD). It is a special and precise version of the measure problem recurrently discussed on this list. It is apparently not so precise because the "measure" is not defined (through the UDA). But the "rigorous" result remains: you don't need to know the measure for understanding 1) that comp reduces physics into the *search* of that unique measure, and 2) that this search must be made only through the machine's psychology. Nevertheless I search to isolate that measure, and I do that by the interview of the machine through G (going to the "meta" level as says Georges) and its angel/truth theory (through G*). See below definitions and programs. For understanding the UDA (and the reversal psycho/physico), people need only a passive amount of computer science and elementary comp philosophy. The best (IMO) book is, still today, "Mind's I" edited by Hofstadter and Dennett, even if both Dennett and Hofstadter seem to close their eyes where I insist maintaining them wide open; in particular both Dennett and Hofstadter fail to see the comp indeterminacy, although they both proposed some versions of the duplication experiment.). I like also to mention Daniel Galouye Sc Fi book "Simulacron 3", and the more recent "permutation city" by Greg Egan. Of course UDA stretches a lot such similar thought experiences. >It may be >that you know too much as one of the famous scientists said when he heard >about >the accomplishment of a younger and less experienced colleague (I think it >was >Wofgang Pauli... "Ach! I know too much!"). > >Let's see if we can summarize your position in simple terms. Mmh ... let us try. But before I would like to say that the modal mathematics really simplify the matter because the needed self-reference makes you walk on the counter-intuitive border of consistency. But you are surely right in insisting to make things simpler, in some way. >1) What are the axioms and rules of inference supporting your system. This >answer >should be answerable in a few lines. Please don't mention Kripke, Leibnitz or >anyone else. Do not give any reference. State your system from the ground up. I have not really a system. Perhaps a "realm" would be better. A third person (minimal) ontology. You know it and we know that it is not what you appreciate the more, for it is just numbers. Arithmetical truth, in a large sense including computer science, provability logics and other "intensional" (modal) variations. Since Godel we know arithmetical truth is not completely axiomatisable. No *complete* TOE for numbers and/of machines. Now having just a realm we need a strategy to isolate the measure on "my" relative consistent extensions appearing in UD*. (That move is made obligatory by the UDA). My strategy is infinitely naive. I just ask the machine. The sound self-referentially correct machines. The Lobian (Loebian) machine as I call it in my thesis. It is difficult to imagine a more simple minded idea, isn't it? I ask her first about her provability ability. Actually this is what *has been done* by Godel, Lob etc. and the whole interview is *completely* captured by the modal theory G. And you get miraculously G*, the guardian angel, a system which proves *all* the *true* sentences about probability (and unprovability, concistency, etc.). G is included in G* of course. These two theories are really an embryon (at least) of the self referentially correct machine's laws of mind. G and G* are really what I call machine psychology. G is actually machine's machine psychology, explaining what the machine can say about her own psychology, and G* is *all* machine's psychology including explanation why the machine remains silent on some question. (All, but without quantifying in the scope of the provability predicate, but let us not be distracted now by too technical remarks). I limit my interview to sound machine talking classical logic and sharing my belief in elementary provable number statements (by which I mean provable in Peano aritmetic or ZF, etc.). Those number truth contains "intensional" one (thanks to Godelian like coding, or better thanks to "programming"), containing statements like "the machine coded by i will stop on input coded by number j". So "my" system, if you want, are G and G*. But of course they are not my system, but the provably logic machine's systems (also known as the logic of self-reference). You can translate "G proves []p -> [][]p" by [for all p in the machine language, the machine proves "if I can prove p then I can prove that I can prove p"], and you can translate "G* proves []p -> [][]p", by [for all p in the machine language, if the machine can prove p then the machine can prove that she can prove p"]. >2) Derive the "Little Abstract Schroedinger Equation" from these axioms. >Again this should be short.(note that I have not said anyting about >uncertainty yet. This comes below) You ask it. You get it! But this cannot *not* be technical. And I cannot be more short than the proof allows me (why don't you ask Andrew Wiles for a shorter proof of Fermat theorem!) You ask for the crux of the crux, here it is. I recall LASE (the Little Abstract Schroedinger Equation) is: p -> []<>p, This is because the system B, with the following axioms and inference rules: AXIOMS [](p -> q) -> ([]p -> []q) K []p -> p T p -> []<>p LASE RULES p p -> q p -------- Modus Ponens --- Necessitation, q []p provide a modal representation of (minimal) Quantum Logic. Now "my systems" are G and G*. I recall once more that G is a sound and complete formalisation of of all modal sentences such that their interpretation (where the atomic sentence are interpreted by any sentence in the language of the machine, and "[]p" is interpreted by "I prove p", also in the language of the machine) are *provable by the machine*. G* is a sound and complete formalisation of of all modal sentences such that their interpretation are *true on the machine* instead of just provable. The soundness of the machine makes G include in G*. I recall that a formal presentation of G is: AXIOMS [](p -> q) -> ([]p -> []q) K []([]p -> p -> []p L RULES p p -> q p -------- Modus Ponens --- Necessitation q []p and G* is AXIOMS Any theorem of G []p -> p RULES p p -> q -------- Modus Ponens (only! No Necessitation rule!!!) q (Plus some "obious but tedious" substitution rules) G and G* are really the laws of mind (of the *ideal* machine if you want). Now remember that my goal is to ask the machine about the measure on its (personal) consistent extensions. In particular I define the "measure of p is equal to one" by "provable p and consistent p" []p & <>p A motivation here is giving by the Kripke semantics (if I can mention that!). Indeed remember that []p is always true in terminal world. A terminal world has no extension at all. For having a measure one on the consistent extension, I must explicitely state that consistent extensions exists, that is p is sure (measure one) if p is provable (true in all accessible extension/world) and consistent (there is at least one accessible world). That is I define "m(p) = 1" by [€]p = []p & <>p. Now "p" must belong to UD*. It can be shown that it is enough to restrict the interpretation of p (in the language of the machine) by so called \Sigma_1 sentences (a UD generates sentences equivalent to \Sigma_1 sentences, and reciprocaly a generation of all \Sigma_1 sentences gives something equivalent to a UD). A sigma_1 sentence is a sentence provably equivalent to a sentence with the form "It exist a number n such that P(n)" with P algorithmically decidable. You can convince yourself that if such a sentence is true then it is provable. Actually the sound machine I interview can prove this fact in some sense: the sound machine can prove p -> []p for all p which are sigma_1. We must prove that G* proves the theorem of B (T and LASE) and are closed for modus ponens. (I loose the necessitation rule, and the substitution rule must be weakened). You can ask me "why" at any point. Don't hesitate. The main point is the proof by G* of LASE. That is when p is \Sigma_1: G* proves p -> [€]<€>p Let us do it in detail (you ask!, and I let you prove that G* prove [€]p->p, the other axiom of B, by yourself. It is really easy). Remember that [€]p is []p & <>p So <€>p = -[€]-p (definition of <€> !) = -([]-p & <>-p) = (-[]-p v -<>-p) = <>p v []p = []p v <>p (recall -(A & B) = (-A v -B) and other elementary propositional equivalence), so [€]<€>p = []<€>p & <><€>p = []([]p v <>p) & <>([]p v <>p) So, all what we need to show is that G* proves, for p corresponding to the \sigma_1 sentence : p -> []([]p v <>p) & <>([]p v <>p) Now if G* proves p -> A and if G* proves p -> B, then G* proves p -> (A & B), so it is enough to prove: that 1) G* proves p -> []([]p v <>p), and 2) G* proves p -> <>([]p v <>p). And this for p \Sigma_1 sentences. Modally "\Sigma_1-ness" can be shown to be characterised by the modal sentence "p -> []p".(Visser's result). You see that the true \Sigma_1 sentence are verifiable (if they are true they are provable, they are necessarily accessible by the UD). Let us prove 1). a) G proves p -> []p (p \Sigma_1) b) G proves p -> ([]p v <>p) (elementary propositional calculus) c) G proves []p -> []([]p v <>p) This is because if G proves A->B, then G proves []A -> []B (indeed if G proves A->B, then G proves [](A->B) by the necessitation rule, but G proves [](A->B) -> ([]A -> []B) because it is an instance of the K axiom, so by modus ponens G proves []A -> []B. We say that G is a regular logic. A regular logic is any logic which proves []A -> []B when it proves A -> B. d) G proves p -> []([]p v <>p) by a) and c). e) G* proves p -> []([]p v <>p) because G is included in G*. 1) is proved. I have begin with G (and not G*) because G* is not a regular logic! G* prove t -> <>t, but G* does not prove that []t -> []<>t (t = TRUE, easy exercice once you get familiar with G). Let us prove 2). It works even on non \Sigma_1 propositions. a) G* proves []p -> p (axiom of G*) b) G* proves -p -> -[]p (elementary propositional calculus) c) G* proves --p -> -[]-p (subst -p for p) d) G* proves p -> <>p (from c, cf. p <-> --p, <>p = -[]-p) e) G* proves p -> ([]p v <>p) (elem. prop. calc.) f) G* proves ([]p v <>p) -> <>([]p v <>p) (subst ([]p v <>p) for p in d). g) G* proves p -> <>([]p v <>p) by e) and f). 2) is proved. And so LASE is proved. The machine's guardian angel tell us that the "measure one on the consistent extensions" obeys some sort of quantum logic. >3) How does consciousness - i.e., first person point of view - >come about from >the axioms and rules of inference. Why is this set of axioms unique in >allowing >consciousness to arise? It depends how you define consciousness in the language of the machine, of course. Once you find such definition you can interrogate G and G* by yourself! Note that G and G* are really unique as far as you interview sound machines "believing" (proving, communicating) enough elementary arithmetical truth. A brouwerian sort of "animal" consciousness seems to be captured by t v <>t, which is just <o>t in the first variant of the bew box []. (cf [o]p = []p & p, so <o>p = t v <>t, just use again that <o> is -[o]-. This gives the S4Grz logic with its asymmetrical bifurking temporal description of evolving knowledge states. It is a "plenitude" in the sense that G* does not add a thing to G. From the point of view of that first person subject provability *is* equal to truth. But immediate perception is given by the []p & <>p variant of the box. With p sigma_1 that gives our LASE, classifying our possible *verifiable* experiences. I mention the subtle mariage of symmetry and antisymmetry provided by []p & <>p & p for the "true" immediate experiences. This makes possible to distinguish (astonishingly enough) phantom pains from "referentially correct pains! It proves also LASE. It seems that the quanta is not a long way from the qualia! If you add to the machine some self-anticipating ability, you get an evolving machine able to speed-up itself by "building their own consistent extensions" (The speed-up is a consequence of some other result by Godel). It can be shown that such machine is always risking loosing consistency in the process by anticipating to much. >4) How does the world come about from the existence of consciousness and >axioms >and rules of inference. How does third person point of view arise? If we are machine (comp) we will never know if there is a world or any consistent extensions. That would be akin to []<>t (a falsity G* says). Appearances, and even solid and stable, and locally true, appearances of (many) worlds is explained by the measure on the consistent extensions. Third person arises when the machines smell (infere) Plato Heaven. Plato heaven, of course, does not arise. (By which I mean that the truth of arithmetical sentences like "2+2=4", "8 divides n -> 4 divides n" or Fermat, Goldbach, etc." are independent of myself and yourself (with my respect). >5) How does LASE introduce uncertainty, superposition, and the violation of >Bell's inequality, in the perception of the world by consciousness. Give an >example as a thought experiment involving consciousness and world as >described above. Important questions, no doubt. Difficult one I'm afraid. You enter the territory of the open problems ... Well, going from LASE to uncertainty is not obvious at all , even for "real" quantum logician. And it is not easier for our arithmetical quantum logic. It is a good research project! Nevertheless the compatibility of observable admit plenty quantum logical definition and are easy to translate in the modal system. So that part is less difficult (except you must find the right representation). For the same reason, superposition are more easily handled, by translating the quantum logical disjunction modally: A + B can be translated (thanks to the link between the modal B system and quantum logic) by [€]<€>([€]<€>A v [€]<€>B). Bell's inequality: here is a (purely arithmetical) version of it, [€]<€>A & [€]<€>B -> [€]<€>(([€]<€>A & [€]<€>C) v ([€]<€>B & [€]-[€]<€>C)). Note it is a purely arithmetical sentence because the arithmetical interpretation of [€]p is Bew('p') & Con ('p') ;Con ('p') = -Bew('-p') where bew and con has been arithmetized (like Godel did) and 'p' is for a godel number (of p). I programmed a computer (some years ago) to prove it or refute it, but it is intractable by brute programming ... (so it is an open problem). You asked a thought experiment involving consciousness and world as described above? That question is a little fuzzy for me. Is not UDA enough? >6) Is it possible to write a computer program to illustrate all of this? A program now! What an exam! I thought you want me not being too technical. But y're the master. You ask, I give :-) Below is a program for G, G*, S4Grz, and Z and Z* (Z are the KD logics coming with the []p & <>p variant, but without the restriction to the sigma_1 sentences). IL is for intuitionistic logic. gip, g*ip, ilip are G, G*, IL, working on infix presentation of formula. So (g '(->(bw p) (bw (bw p))) gives the same answer as (gip '(bw p -> bw bw p)). []p is represented by (bw p). (g A) gives NIL if the formula A is a theorem of g, meaning the list of counterexample is empty, otherwise it gives Kripke models invalidating the formula A. Just read those heavy answers as "not a theorem". But if you want to read the Kripke models just note that "F\#" represente the node of the tree of the accessibility relation on worlds, and that the worlds are represented by lists with the relevant sentences. >This is your end-of-school-year final exam. No cheating allowed. There is >no time limit and it is open book. Take your time. Thanks for the open book. The program below is indeed just a translation (I made in the eighties) in LISP, of the chapter 8 of Boolos 1979. If I don't succed my end-of-school-year final exam, I hope there is an another chance in september! In any case thanks for your persevering attention, Mister G. Levy (my mother's name BTW). Bruno The following is a cut & paste from my IRIDIA Technical Report 1994. =================================================================== [The rest of the post has been deleted.]