Hi Tim, hi People
This post is a continuation of
http://www.escribe.com/science/theory/m3908.html
where I try to explain the role of Yetter's book in the
ultimate derivation of physics from machine psychology.
Note that the gain of such derivation would be:
1) The possibility of experimental refutation of comp.
(just by comparing the comp-physics and empiry).
2) Thanks to the difference G* minus G, (that is the
(godelian) difference between machine psychology (G*)
and machine's machine psychology (G)) we have a non
trivial source for *physical sensation* (as true
inferable non communicable (non provable) truth. For
example consciousness can be seen as instinctive
inference of consistency.
I was saying (in m3908) that Yetter's book bears on both
side of the mind-body problem, where roughly speaking MIND
is defined by boolean classical logic and MATTER by
quantum logic.
I will try to be as short and informal as possible, at
the risk of being slightly incorrect.
Recall that the UDA shows that physics, from the point
of view of machine m in state S_m is given by the structure
(hopefully a probability domain structure) on the set of
accessible consistent extensions of S_m.
The AUDA strategy consists in interviewing a consistent
machine (and its guardian angel) about its consistent
extensions. The abstract structure corresponding to such
discourse are given by G and G* (called GL and GLS in
Boolos 1993, or PRL and PRL^omega in Smorynski 1985, ...).
G formalizes what a machine can prove about itself, and
G* formalizes what is true about the machine. The non
empty character of G* minus G reflects the incompleteness
phenomenon: there exists a lot of truth that the machine
cannot prove about itself. The main example is the simple
consistency statement -[]f, or equivalently <>t.
When I say G captures the provable propositions by the
machine about itself, I am really talking about third
person propositions bearing on correct *descriptions* of
itself.
This concerns the computationalist which faces description
of his body and brains for exemple. It is not, and cannot be
the intuitive first person "I".
But we can defined this intuitive first person "I" by the
thaetetus' definition of knowledge linking provability (the
G box) and truth; this by defining a new box, and thus another
modal logic, by []p & p. The counterintuitive aspect of the
Godelian formal provability comes from the fact that
provability is not linked to truth, or, more precisely,
it is not linkable to truth by the machine (but such a link
is easy stuff for its guardian angel who know the truth
about the machine!).
With formula you have
G does not prove []p equivalent with []p & p
but
G* does prove []p equivalent with []p & p
If you define a new box [1]p by []p & p ([] = the G box)
You have obviously that [1]p -> p, because ([]p & p) -> p
(because "((a & b) -> a)" is a tautology.
The logic of that new box is given by the modal system S4Grz
and it permits the association of a canonical intuitionist
logic, and even a topos, to the consistent machine. It plays
the role of the first person associated to the machine.
But the Kripke semantics of S4Grz, [that is fundamentally
the geometry of the possible accessible worlds or accessible
states in which the theorem of S4Grz are invariant (and non
dependant of the valuation of the sentence letter p, q, r ...)]
is given by antisymmetric frame.
It has been shown, through Godel, McKinsey and Tarski,
Grzegorczyk, that the classical modal S4Grz is a classical
version of intuitionist logic. Very genuine for a first person.
In a similar manner Goldblatt 1974 has succeeded to show that
the modal logic, know as B in the literature, is a classical
version of quantum logic (a weaker form of the Birkhoff
von Neumann 1936 quantum logic).
So it would be nice if our interview of the machine (and its
angel) lead us to B, or near B, at least, giving us a quantum
logic for the background of the comp-physics.
But the beginning of the interview, where we defined the
first person in term of G, lead us to the antisymetric S4Grz,
and that's odd because the Kripke semantics of B, that is the
Kripke frames of B are the symmetric one.
There is no need to despair! After all the G frame are
irreflexive (no worlds are accessible from themselves), and
the S4Grz frame are reflexive. But we did succeeded going from
the irreflexive G frame to the reflexive S4Grz.
Still, when I discover the antisymmetry of "my" first person,
and given that the physics should appear in the discourse
of the machine first person, I conclude that quantum logic
was not in the near horizon of the interview, and I try,
without clear success to make appear a weaker (substructural)
logic which has some physical smell too, and which was the
Girard linear logic. So I have first conjecture that the
(re)definition of physics in the G and S4Grz logics should lead
to linear logic. Unfortunately the relation between linear
logic and quantum logic was itself not obvious too. Then,
a curious paper appears making an explicit relation between
linear logic and "certain models for the logic of quantum
mechanics". That paper was "Quantales and (noncommutative)
linear logic", it appears in 'The Journal of Symbolic Logic"
(volume 55, n°1, 1990) and was written by Yetter.
Yetter's paper will enhanced my interest in linear logic,
which will lead me to category theory (the *-autonomous one
which gives models for linear logic) then quickly toward the
monoidal closed category, etc.
>From Yetter's paper I will understand the importance (for
my derivation of physics from machine) of finding
good tensorial products
good topologies
good dualities
and I will search for them ... without success. I'm still
searching!
Still the miracle *will* occur: the translation of UDA in
arithmetic (classical machine language) leads automatically
to the symmetric B.
I explain quickly. (I have explained this in other posts).
To have a probability 1 for a "physical certainty" p, we need
[]p (that is p is true in all accessible worlds, if that
exists) and <>p (there is an accessible world where p is true).
So we must refine the "[]p ===> []p & p" transformation by
"[]p ===> []p & <>p"
Then, just taking into account that the state/world must be
accessible by the universal dovetailer. This is done by
restricting the realisations of the sentence letter to the
\Sigma_1 arithmetical sentences, i.e. those which have the
shape ExP(x) with P decidable (E = "it exists").
This gives a logic for which the logic B, without the
necessitation rule, is sound (but not complete).
Now that loss of the necessitation means we get a weak logic,
hopefully a substructural linear sort of quantum logic.
Actually I got a family of such logics: the Z and X logics.
(Z, Z0, Z1, ..., X, X0, X1, ... then the same with "*").
X1* should give physics, X1* minus X1 should give the
physical sensations, the X_alpha, alpha ordinal gives
room for extremely weak form of computationalism, etc.
This is why I am excited by Yetter's book from the MIND
toward MATTER link motivation.
* * *
But I said that I dig also in the reverse direction, that
is from the MATTER-toward-MIND link. Here Yetter's book is
also interesting. Since I read Kitaev's paper
See
http://xxx.lanl.gov/abs/quant-ph/9707021
I have begun to grasp the deep relation between quantum
topology and quantum information. I have also realised how
to get tensorial products without global tensor structure
as it is explained explicitely in the paper by Freedman
entitled "A magnetic model with a possible Chern Simons phase".
See
http://xxx.lanl.gov/abs/quant-ph/0110060
Modular functor, an abstract form for anyon-type quantum
computer also appeared in the work of "linear-sort"of
logician like Blute, Cockett and Seely with their linear
functor. So we see that the logician themselves begun
to add on the MATTER-toward-MIND path *and* the other
way too.
This is hardly astonishing. Girard build his "system F"
as a reconstruction of Hilbert program after Godel
demoslished Hilbert initial program. And Girard got his
linear logic by making his system F just more symmetric.
My own work can be seen as going directly from Godel
to the needed weaker logic by listening directly to what
a machine can say about its limitations, and its limitation's
border.
I am conjecturing the Z and above all the X (*) logics define
"naturally" some sort of machine-first-person accessible
quantum computing machine. That would close the
mind->matter (BIT->QUBIT) path.
The book by Yetter could help familiarization with
the braided monoidal categories and their possible use
in quantum computing. Alas it is a short book and Yetter
does not make explicit link with his noncommutative
linear logic. Also, the second part of the book is
not self-contained and looks rather hard.
This ends my hopefully not too self-centered, but
certainly quite "self"-centered comment on Yetter's book.
Hoping having been not too short. Er ... or too long :)
Have a nice week-end,
Bruno
(*) With the transformation []p ===> []p & <>p & p, p \Sigma_1
as described by G*. (compare with the Z logic where
[]p is transformed into []p & <>p, this is a re-applica-
tion of the thaetetus's trick).
The precise translation from G to the Z and X logic:
For the Z logic:
D(p) = p
D(A & B) = D(A) & D(B)
D(A v B) = D(A) v D(B)
D(-A) = -D(A)
D([]A) = []D(A) & <>D(A) D is for Deontic Transform
For the X logic:
D(p) = p
D(A & B) = D(A) & D(B)
D(A v B) = D(A) v D(B)
D(-A) = -D(A)
D([]A) = []D(A) & <>D(A) & A (see the added "& A" !)
Received on Fri Aug 23 2002 - 08:21:15 PDT