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
