- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Wei Dai <weidai.domain.name.hidden>

Date: Mon, 28 May 2001 12:41:52 -0700

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

Date: Mon, 28 May 2001 12:41:52 -0700

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.

Post grad ? Well, perhaps ..., these days ... :-)

Damned! (but I appreciate the honesty).

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.

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.

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

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.

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.

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

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?

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.

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

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