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.
Received on Wed Aug 21 2002 - 09:52:53 PDT