Re: Consistency? + Programs for G, G*, ...

From: Wei Dai <weidai.domain.name.hidden>
Date: Sun, 3 Jun 2001 16:22:09 -0700

I've changed the max submission size to 60 KB.

----- Forwarded message from George Levy -----

Date: Sat, 2 Jun 2001 22:24:23 -0700
From: George Levy
To: everything-list.domain.name.hidden
Subject: Re: Consistency? + Programs for G, G*, ...
X-Diagnostic: Diverted & unprocessed
X-Diagnostic: Submission size exceeds 40000 bytes

Hi Bruno,

Your effort to clarify your position is admirable and I hope other everythingers are
following your explanation. You are still too technical for my taste, and I may
simply have to give up on understanding your position at a critical and constructive
level rather than just at a spectator level.

>
> A version of the UDA can be found in the archive at
> http://www.escribe.com/science/theory/m1726.html
>

I agree fully with your UDA. To summarixe: Basically the perception of consciousness
as seen from the first person is continuous, independently of interruptions in time,
separation in space, (virtual) implementation level, and number of branchings (and
number of fusings or mergings... my addition).

> The UDA illustrates also the incompleteness of Schmidhuberian-like TOE approach,

Yes. Because of UDA, consciousness doesn't seems to be tied down to one particular
"Schmidhuberian universe." In fact the environment where consciousness operates seems
to be the whole plenitude and I agree with you when you expressed reluctance in
talking about a "universe." We are in the plenitude but our senses can only perceive
a thin slice of it. More precisely, for each one of us, "I-plural" am in the
plenitude, but "I-plural" can perceive only a thin slice of it. Each "I" has a
different perspective.

> 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).

Yes. consistency in the (virtual) linkage that connects the present state with all
immediate future states (consistent extensions) is the filter that defines
consciousness from non consciousness. A corollary is that non-consistent extentions
are not conscious. The measure problem is how to quantify the relative number of
(future) extensions having different attributes.

> 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.

Ok. Physics is pattern of laws perceived by the consciousness observing the
plenitude. The consistency filter that restricts consciousness is the same filter
that restrict the world that consciousness observes. This is why the world is
understandable and this is why there are no white rabbits. White rabbits are not
consistent.


>
> 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.
>

I am not very familiar with the concept of G*.


>
> For understanding the UDA (and the reversal psycho/physico),
> people need only a passive amount of computer science and
> elementary comp philosophy. I like also to mention Daniel Galouye Sc Fi book
> "Simulacron 3", and the
> more recent "permutation city" by Greg Egan.

The movies "The Matrix" and "Tron" also deserve a mention


> >
> >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.

>From what you have taught us, modal logic provides the relativistic vehicle needed
that allows each consciousness to exist on its own terms. Consistency and consistent
extentions are only defined in term of the consciousnes that they themselves define.

> >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 am sorry to say you failed that question. You did mention names. But is was a trick
question. Clearly, a precisely defined set of axioms and rules of inference would
have turned consciouness and the world into a Schmidhuber type of mechanistic desert
incapable of supporting consciousness. My intuition is that it is precisely
indeterminacy that is responsible for consciousness.

>
> 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.
>

Great answer!

> 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.
>

Bad answer. Lobian??? I don't know what you mean by asking the machine. Is G the
(relativistic or modal) set of axioms that the machine has. Asking the machine then
means using those axioms? I don't know what G* is. Some Godelian construct?


>
> 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).
>

Now you attempt to explain G* but you call it "*all* machine psychology". Can we
restrict ourselves to the words axioms/rules of inference? Is G* the set of all
axiomatic systems?


> 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.).

We don't have to be specific. Can we just say the machine is governed by a consistent
axiomatic system?

>
> 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).

I don't understand

> 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"].
>

I don't understand. G appears to be a first person statement, and G* a third person
one. G is defined by a set of axioms and by itself leads to complete determinacy.
Intuitively speaking it is not sufficient to produce consciousness. So we need G*
which is, I guess, is non-G. Yet, how can G* be emulated by a machine?

>
> >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*.
>

OK. G* is true on the machine but not provable. So how does G* come about? How is G*
implemented to generate consciousness? Is G* virtual and G actual? What is the
meaning of virtual versus actual in the context of the plenitude?


>
> 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!

How do I do that? Is G* really implemented or implementable?


> 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.

I hardly understood the above paragraph.... Maybe we should give up on being
formal...There is too much background which seems to be required to understand this
stuff.

>
>
> >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).

Let's use English. []<>t: prove not consistent?

>
> 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).

I don't see it your way. I would rather take the relativistic point of view and say
that third person point of view arises when several consciousness share the same view
of the plenitude because their axiomatic systems (frames of reference) are similar.



>
>
> >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?

Yes UDA is very powerful. In fact UDA can certainly illustrate uncertainty. However,
I don't see how UDA can show how particles can be in superposition and interfere with
each other as in the double slit experiment. It requires the attribute of "phase"
associated to a particle. I don't know how to build "phase" into the UDA.

An extention of the UDA can also illustrate the EPR experiment - the apparent faster
than light communication between two particles - but I don't see how it can model
Bell's inequality theorem. To model the EPR experiment in the Brussel to
Washington/Moscow teleprotation, one would have to teleport not just one person, but
also some object with a particular attribute hidden from the person until he decides
to observe it after he has reached destination. Obviously, if the subjective elapsed
time is zero from before the teleportation, to after the telelportation, the
attribute of the object will appear to travel infinitely fast between Washington and
Moscow.

>
> >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 :-)

hmmmm... I thought that was a trick question. An axiomatic system cannot be both
complete and consistent. Therefore there can't be a program for it. We go back on how
you implement both G and G*.....


>
> 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.
>

I did not understand a word of the above. Sorry. I program Forth, Fortran, C and
Visual Basic.


>
> >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!

You'll certainly get many, many, many more chances. The more your consiousness
splits, the more chances you'll get!! This has been a huge effort on your part....
Thanks.

> In any case thanks for your persevering attention, Mister G.
> Levy (my mother's name BTW).
>

Interesting. We may be cousins - going back far enough it is a certainty! I do have
some cousins in France. In fact I do have a second cousin called Bruno, but his
father not his mother is a Levy. This Bruno is probably in his late forties. I have
lived in Casablanca and Montreal, and now reside in San Diego, California.

George(s)


----- End forwarded message -----
Received on Sun Jun 03 2001 - 16:29:51 PDT

This archive was generated by hypermail 2.3.0 : Fri Feb 16 2018 - 13:20:07 PST