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: <everything-list.domain.name.hidden>
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.]
Received on Mon May 28 2001 - 12:56:57 PDT