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

From: Bruno Marchal <marchal.domain.name.hidden>

Date: Wed, 21 Aug 2002 18:46:11 +0200

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

Date: Wed, 21 Aug 2002 18:46:11 +0200

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

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