I hope this is our last *too long* post, Juergen.
At the end of it, I propose we come back to the initial
discussion, if you agree.
Juergen wrote:
>> Normally a constructive philosopher should abandon comp right here,
>> because it follows from that theorem that we cannot be machine in
>> any constructive sense.
>
>Which theorem? Send pointer to its proof. Not to its informal
>description, but to its proof.
Sorry but for reason of place I will remain a little bit informal.
The theorem concerns sound (or just consistent) machines proving
enough elementary theorems of arithmetic.
There exists multiple versions of the theorem.
Theorem : no sound (or just consistent) machine can build
a copy of itself in a provable way.
Theorem : No sound machine can know its own description.
(where knowing is formalised by S4 modal logic (or S4Grz)
and description by arithmetisation).
Theorem: the mechanist knower cannot know itself.
Theorem: No sound machine can build a machine which
proves the same theorems as itself and at the same time proves
that fact.
The theorem is sometimes called "the correct reconstruction of Lucas
argument". Unlike the traditional Lucas/Penrose argument this
theorem is not controversial, although the first reconstructions of it
were not very rigorous.
The first one to realise that truth, and to propose a rigorous argument
is Emil Post in his 1922 anticipation (see the book of Davis 1965).
Note there is still a slight error in Post's formulation.
It (re) originates in the delightful paper by Benacerraf "God, the Devil
and Godel". Unfortunately, although all the interesting ideas are in
Benacerraf's paper, the paper is wrong from the beginning to the end
(as Benacerraf aknowledges himself in an appendice). Chihara, Wang,
Reinhaerdt have propose, with growing level of rigor, reconstructions of
Benacerraf's reconstruction of Lucas.
Penrose (re)proposes Lucas's use of Godel theorem against mechanism in
his first book, but correct it in his second book. So you can find a
proof in the second book of Penrose too (rather involved proof).
In the second book Penrose argue that mechanist philosophy is
meaningfull only in the sense of "being a machine and knowing which
one". Then indeed *that* mechanist philosophy is refuted.
Just look at my thesis page 40 -> 44. With G and G* it is almost
an easy exercice to formalise it completely and to prove it.
You will find all formal details, + the references in my thesis.
(It would just be indecent to give here a formal description
of that theorem, because that would be long (as you can guess),
and, until now, it would be without most distracting.
>(One reason why I doubt this: isn't the lowest possible level - embodied
>by what's computable in the limit - sufficient? Why not run all universes
>GTM-computable in the limit? If one of them is ours, then the set-up
>is constructive.)
How do you know there is a lowest possible level?
What do you mean by "one of them is ours"?
Once you distinguish first and third person, you will understand
(well it is a consequence of the invariance lemma) that
it is at least consistent with comp that there is no lowest
possible level, and you can understand that the expression
"our universe" has necessarily no obvious meaning.
We will come back to the invariance lemma later, (if you agree).
Your problem is that you are attached to a very naive (and vague!)
theory of mind where the first person is attached to
a particular "physical" instantiation of a computation.
In 1988 I have build the movie-graph thought experiment (platonic
destructive in the James Brown's nomenclature) which shows that
this view is incompatible with comp. Maudlin has proved in 1989
an equivalent result. Unlike UDA the graph movie argument *is*
difficult (we discuss it at lenght in the list). For pedagogical
reason I don't use it here. I use some form of Occam instead.
If you want really be rigorous here you should solve first the
very serious Putnam-Chalmers-Mallah's physical implementation problem.
(see the thread on that implementation problem in the archive).
I have not the Mallah's problem, because I have no universes at all.
Just many computational histories, which together makes first person
discourse possible.
I have *other* problems, like the white rabbits, which force us to
derive the physical law from the psychological laws of
machine's dreams. But then, that's the result of the first part.
>Not uncomputable. Any past is finite.
I was talking about the immediate next futur.
>So it is at worst random or
>"Martin-Loef-random" or incompressible. None of those you cite is
>careless when it comes to the difference between countable and uncountable
>sets. None claims one can compute a continuum by dovetailing. Dovetailing
>will be forever limited to the countable realm.
I have never said that we can "compute a continuum" by dovetailing.
Sometimes, in some context, I talk about dovetailing *on* the continuum
because I have explain precisely what I mean by that.
I do that whith people who have a precise idea on the 1/3 person
difference. From the 1-person point of view that continuum is relevant.
(see below).
>The various Dempster-Shafer (DS) approaches are no alternatives
>to probability theory. They are extensions designed to facilitate
>handling of uncertainty in contexts where lack of belief does not imply
>disbelief. But DS is essentially about hulls confining sets of
>traditional distributions, and thus compatible with the traditional
>framework of Bayesian statistics. (Variants of DS that are not yield
>paradoxical results.)
Hulls confining sets of traditional distributions? You can see it
that way, but that does not entails compatibility with the framework of
Bayesian statistics.
>It is this recurring type of claim I find so irritating: "rigorous
>proof" without formal framework.
Let us remember that this is an important point where we *completely*
disagree.
It is possible to be 100% formally correct and still be 100% lacking
philosophical rigor. My favorite exemple is perhaps your first paper :-)
And it is also possible to be 100% rigorous although being 100% informal.
The first part of my thesis is hopefully an exemple. Others are
provide by some thought experiment by Galileo, Simon Stevin, etc.
Note that mathematicians *never* prove things formally. For exemple
Fermat theorem has been proved, but it is still an open problem
if the proof can be formalised in Peano arithmetic, or in which
precise extension of Peano arithmetic can it be proved, ...
>> A weakness is that I am lead toward hard mathematics.
>
>What a strange remark. The weakness of your texts is that they are
>so informal.
This is what *I* do find irritating: the fact that you say this
although you have admitted not having read my thesis. What kind of
scientist are you? Where does your certainty come from?
The second part belongs to mathematics (of course, there is always the
possibility of systematic error, but it has been verified by
independant mathematicians, for the thesis, for the price, etc.)
I am lead to difficult open mathematical problems.
(The most important is to axiomatise Z1*).
To make things clear, the work contains two parts:
-1) A rigorous thought experiment showing that if we accept comp
then physics is a branch of machine's psychology.
It is informal but rigorous, despite your irritation with
respect to this point. It leads also toward a many-things,
observer-moment-like, ontology (thats why I am here).
-2) A mathematical part where I "interview" the machine and its
"guardian angel". It is there that a "quantum logic" appears naturaly
as a kind of border of the first person. It is also there that
I am lead to difficult question of mathematical logics.
I say a little more on that second part in the archive at
http://www.escribe.com/science/theory/m1417.html
The guardian angel is Solovay G' modal logic. (I call it G*,
nowadays provability logician call it GLS).
G has a long story and got many names:
K4W (segerberg), PRL (smorinsky), G (Solovay), L (the Deutsch),
GL (recent american name). L is for Lob).
Do you know these provability logics ?
I recall to everybody that Smullyan has written a popular book on
G and G* : Forever undecided. (Precise ref in my thesis, or paper).
This little book is a nice introduction to provability logic.
It certainly gives a feeling of what G and G* are.
The second part is difficult. It needs familiarity with quantum
logic, quantum mechanics, mathematical logic, philosophical logic,
and philosophy of mind. No doubt it is difficult. But in fundamental
matter nothing is urgent.
>Your thesis is in French.
I am very nervous about that. The day I have been accepted for
doing a thesis in France, The minister TOUBON decides ALL french
thesis, even those by foreigners, must be done in french.
>Your papers are informal.
I agree for the first part (of both my paper, and thesis).
But: please, don't confuse "vague" and "informal". Don't confuse also
"mathematical" and "formal".
Formalisation is useful only for metamathematics, computer science,
and computationalist philosophy. Not for doing the proof but for
proving things (informaly) *on* the proof.
Your confusion has a taste of pregodelian formalist philosophy (I tell
you that before). That has nothing to do with constructivisme.
Most important constructivist (Brouwer, Bridge) are anti-formalist.
>Then there is your "invariance lemma: the way you quantify 1-indeterminacy
>is independent of (3-)time, (3-)place, and (3-)real/virtual nature of the
>reconstitution." This does not make sense, because if the (3-) probability
>distribution on the possible futures and reconstitutions does depend on
>time or place or other things (why not?) then 1-indeterminacy does so,
>too. Under most distributions, some futures are less likely than others.
>Hence there are nontrivial, distribution-dependent, probabilistic
>1-predictions as well as "quantifications of 1-indeterminacy" that depend on
>time/space/other things.
I see you genuily fail to understand the invariance lemma.
No problem. We will come back to this until you get the
TILT, (if you agree).
>I am prejudiced against claims of rigorous proof when even the
>assumptions are unclear; and against statements that are plain
>wrong, such as "the UD generates all real numbers".
I am not claiming I am rigorous, except when you say I am vague
and when you ask me precisions which are not relevant.
The sentence "the UD generates all real numbers" is ambiguous.
Either you interpret it as
"The UD generates (enumerates) the set of all real numbers"
This does indeed contradict Cantor's theorem.
Or you interpret it as
"All real number are (individually) generated by the UD".
In which case, with the usual definition of "generating a
real (generating all its prefixes)" it is just correct. Isn't it?
Of course this is make possible because each prefixe is the
prefixe of 2^aleph_0 reals.
Perhaps the confusion comes from this ambiguity.
* * *
Look, Juergen, don't make yourself member of the club of those
who criticizes my work without studying it, as you confess.
You are not the first one.
I agree the basic result is so counter-intuitive that it is easy
to dismiss it without further consideration. But that is not how
science progress.
Let us go back to the first major point of the philosophical
(informal but rigorous) argument.
(Note that it would be useless to make a discussion on the
possibility of rigorous philosophical argument. Once you are
convinced by just one such proof you will know that that exists).
Now, with all our disgressions, I don't remember if you have
accept the first informal, but precise, point. So I ask
you again: do you agree that comp entails the existence of
first person indeterminacy, as it is shown by the
self-duplication thought experience?
You can ask me to make things more precise. Don't ask me to be
formal, because I ask you a personal question and I cannot
formalise *you*. (Later you will discover that comp entails
in a provable way that the first person cannot never
be formalised, but that this very fact (the unformalisability
of the "I") can be proved formally!).
Later. Let us go step by step.
And let us going back to short post without speculating
vaguely on the whole work. OK?
Bruno
Received on Wed Feb 21 2001 - 08:08:42 PST