Hi Tim, Hi All So I got indeed the Yetter's book. I promise to you, Tim, some commentaries. Here they are. It is for me an opportunity to write my last long post, before I try to write that english text as Wei gently insists I do. Yetter's book interests me for two related reasons, both linked to my thesis, and even to the most advanced part of it---in some sense you arrive, in the list, a little to early with your toposes! :-).

As you know, I am interested in the mind-body problem, and toes. A toe which would not solve the mind-body problem, or "meta-solve" it by explaining why we cannot solve it, would be a very poor toe, imo. I think it has been a good methodology for the physicists to forget the mind, but such attitude cannot last in a search of a theory of *everything*. About the mind I am a conservative sort of logician, and I am platonist about positive integers, so by mind I take first boolean arithmetical truth. Did not George Boole entitled his book "The Laws of Thought"? Add the digital mechanist, or computationalist, hypothesis, and you get a more *psychological* mind: boolean arithmetical truth, as seen (as anticipated) by consistent boolean universal machine. This is the passage George Boole => George Boolos. No pun intended. The whole idea can be simplified into: MIND = BIT. About the body I am a conservative sort of physicist and I am willing to bet on quantum mechanics. I am not so conservative to keep the wave collapse principle as a *physical principle*, but enough conservative to keep it as a psychological principle. Well, here we have qubits, and, with some simplified Deutsch Kitaev Freedman thesis we could say that MATTER = QUBIT. A simplified translation of the mind-body problem can be made with those conservative views. The MP problem can be seen as a search of a justification of the BIT-QUBIT relation. It is not a too big exaggeration to say that the work by Everett, Graham, Hartle, Zeh Joos, Kiefer (and others) gives an explanation of BITS from QUBITS. That is, how classical observers/worlds emerge from a quantum reality. And it is not at all an exaggeration to say my work is an attempt to explain QUBITS from BITS. Actually I show more and less: -More: because my work provides a proof that, IF we take the comp hyp seriously enough, THEN qubits *must* follow from bits. This is basically done by the Universal Dovetailer Argument UDA (+ the Movie Graph Argument if you don't like explicit reference to OCCAM razor). -Less: because I just paved the beginning of a way from bits to qubits. It is the purpose of the Arithmetical UDA (AUDA). It is at the completion of that road that Yetter's work should help. As you see, I dig on both sides of the mind-body relation, and Yetter's book bears on both side too, as I will try to explain. The UDA is a thought experiment in which "you" are implicated. UDA shows that "your" immediate future is given, relatively to "your" actual state (whatever that is) by some measure on all consistent histories/computations going through that state. The AUDA is a translation of the UDA in the language of any consistent universal machine capable of proving enough arithmetical truth. Since Godel 1931, we know that we can use, as universal language, just elementary arithmetics, with elementary induction. Our goal is to interview a "scientific" machine about its consistent extensions (ce). Those ce are playing the role of the "consistent" histories (not exactly in the sense of Hartle, Isham, ...). By UDA, physics is literally redefined as a "probability" measure on those extensions. The first thing to do is to define the notion of consistent extension in the language of the machine. This is easy, at least after reading Godel! Indeed Godel succeeded in defining the notion of "provable by a machine M" in the language of that machine M. Godel used "principia mathematica" as machine M, and today we prefer to use Peano Arithmetic, but any boolean topos with natural numbers object can play that role. So the intuitive sentence "M proves p" can be translated in arithmetic with Godel's beweisbar arithmetical predicate B. B(`x') means the formula with godel number x is provable by the machine M. You can read "M proves -B(`f')" as M proves that M cannot prove the false. But this is equivalent to: M proves that M is consistent. Actually, Godel's second incompleteness theorem is that this never happens: a consistent machine cannot prove its consistency: -B(`f') -> -B(`-B(`f')) where `x' = godel number of x It happens that consistent machines *can* prove the last formula! The machine M can prove "if M is consistent then M cannot prove its consistency". Let us write Bp as a modal formula []p (p refering to an arithmetical sentence). -[]f means the machine is consistent. In all modal logic -[]A is the same as <>-A. So -[]f is the same as <>-f, i.e. <>t. Godel's second theorem can be written as: <>t -> -[]<>t. You see that a modal logic emerges with the box "[]" being interpreted by the arithmetical provability predicate, and the diamond "<>" by the arithmetical consistency predicate. This last one is, as you guess, useful for interviewing the machine about the consistent extension and about the measure we are searching on those extension. Is the provability box a good candidate for playing the role of the machine's (first person) knowledge? NO. For this we should have the provability of "[]A -> A". In particular we should have []f->f, but A->f is -A, so []f->f is -[]f, that is *consistency*. The consistent machine does not prove []A->A. The consistent machine cannot prove its soundness. Also the consistent machine, being unable to prove its consistency, cannot prove the existence of---even just one---consistent extension. Apparently this takes the hope for a rich interview about the consistent extensions off. But a) the machine can prove sentence like "<>t -> <something>" (like if M is consistent then <something>). Cf the fact that the machine can prove Godel's second theorem, even about itself. b) because physics is redefined as the measure on the consistent extensions, we are primarily interested by the *truth* about those ce, not necessarily what the machine are able to *prove* about them. Here enter Solovay theorems. Let me give you the exact wording of it. See http://www.escribe.com/science/theory/m3889.html for the formal presentations of G and G*. Let L = {p, q, r, ...} = the propositional sentence letters. Let LA be the set of first order arithmetical sentences (like Ex(x=0) AxEy(y>x) Bew(`x'), etc.) (E = it exists, A = For all) A realization R is a function from L to LA assigning to each propositional sentence an arithmetical sentence. Now we can define a translation T of propositional modal sentences in arithmetic: T(p) = R(p) for any propositional sentence letter p T(f) = f T(A -> B) = T(A) -> T(B) and most importantly T([]A) = Bew(`T(A)') with Bew the arithmetical provability predicate (Bew for the German Beweisbar. ("Bew" is less misleading than the "B" above). Solovay first arithmetical completeness theorem is that the modal logic G proves A iff the machine M proves T(A). And this does not depend on the realisation R. So the logic G captures what a machine can prove about its own capacity of proving things. Solovay second arithmetical theorem is that the logic G* proves A iff T(A) is true for the machine M, independently of the fact that M can prove it or not! In some sense G* formalizes completely the incompleteness! G is obviously included in G*, and G is strictly included in G*. The simplest example is given by the consistency proposition <>t: G does not prove it, and indeed the machine cannot prove its consistency, and G* does prove it. That's why sometimes I refer to G as the discourse by the machine itself, and G* as the discourse by the machine's guardian angel. G* knows much more than G. As we have seen above the provability predicate does not obey the typical modal "knowledge" reflexivity formula []p -> p. The provability predicate is not first-person knowledge. It embodies a sort of scientific, third person, form of self reference. G* *can* prove []p -> p, but G* is not closed for the necessitation rule, so that, according to any S4-type formalization of knowledge G* cannot be directly in use. Those bad news are really good news, for it shows a way to handle with care those "intuitive" notion in our counter-intuitive context. In particular, knowing that the machine cannot prove []p -> p (modulo a realisation and a translation, but I will commit the language abuse of not repeating this), although it is true (G* trivially prove []p -> p), we can, thus, define the knowledge of p, by []p & p. This leads to a very interesting notion of first person for consistent machine. It is possible to show that this notion of knowledge cannot be defined in arithmetic! (like the notion of truth with Tarski theorem). This notion of knowledge will entail, for example, that any consistent machine will hardly believe being a (consistent) machine. Independent works by Kuznetsov & Muravitsky, and George Boolos, and Robert Goldblatt, based on the thesis in modal logic by Segerberg show that the logic of [1]p (by definition = []p & p) is completely captured by the modal system S4Grz. That is S4 + the Grzegorczyk formula: []([](p -> []p) -> p) -> p This "horrible formula" gives antisymmetry for the accessibility relation of the S4Grz Kripke semantics. This is a GOOD news because it makes the link between anticipation of consistency, as seen by the "first-person" machine, and irreversibility of the passing from one state of knowledge to another. So S4Grz makes a sort of link between consciousness/ perception (as defined by Helmholtz: anticipation) and subjective time. This is akin to Brouwer's theory of consciousness, from which he based its intuitionist philosophy. This is confirmed through the works of Grzegorczyk and Goldblatt: From S4Grz you can isolate an arithmetical, in term of provability, version of Brouwer's intuitionist logic. And more: It is natural to define S4Grz* (which correspond to G* as S4Grz correspond to G). But surprise: S4Grz = S4Grz*. The first person is his own guardian angel! Even Boolos remarks in his second 1993 book on provability that this phenomenon is "shades of the intuitionists' doctrine that mathematical truth is to be identified with provability. And now that we have an intuitionist first person, we can associate a "free topos" to it, capable of providing rich contextual semantics for the first person in any contextual situation. Now I know you like very much toposes, but at the time I isolate the first person logic, I did not take the antisymmetry of the relation as a good news. Why? Because I hoped for a symmetrical relation, because symmetry is the mark of the physical, and the UDA reasoning shows physics should rely on the first person. At that time I depressed a little bit because I realize that my enterprise was contradictory: how to get physical symmetry from psychological antisymmetry? Oops! I realize I am rather long here. Also I must go now. Don't hesitate to ask question, even about little formal details. I hope you see a little bit more clearly how I proceed. Wait for the next episode if you want see the arithmetical marriage between symmetry and antisymmetry, and more ..., including the importance of Yetter's book, or, more generally, of symmetric and ... non symmetric monoidal categories for eventually extracting the qubits from the dreaming bits. Bruno So it is not exactly my last long post, but it is among them. Perhaps such more detailled explanations will help me in planning a longer paper. Thanks for your patience.