Juergen Schmidhuber wrote >Which are the logically possible universes? Max Tegmark mentioned >a somewhat vaguely defined set of ``self-consistent mathematical >structures,'' implying provability of some sort. The postings of Bruno >Marchal and George Levy and Hal Ruhl also focus on what's provable and >what's not.

You know that Hal Ruhl doesn't distinguish computability and provability, so it is open for me if his approach is nearer your's or mine. The difference relies more between averaging on the (local) set of consistent extensions defined in the whole UD*, or finding a priori defining universes probabilities, or Universal prior. I communicate with the sound lobian machine because I agree (in arithmetic) with the laws of exclude middle, and all classical logic. Provable plays the role of thoroughly verifiable "scientific" communication. (BTW *you* were the guy asking for formalisation!). Now we are working at the metalevel (as George aptly remarks) and we will interview the machine on its self-reference abilities. Recall the goal consists in translating UDA in a language interpretable by a sound UTM. And UDA is a self-referential thought experiment. It will happen that the incompleteness phenomenon will force us to take into account the nuance between []p and ([]p & p) and ([]p & <>p) in the discourse of the machine. They will correspond to provable p, knowable p, probability(p)=1. Knowable will give rise to intuitionist logic and probability 1 will give quantum logic. Probability(p) 1 will really be no more that 1) there is consistent extension, 2) p is true in all those consistent extension. (Only in an ideal frame we have []p -> <>p, remember that in the cul-de-sac world []p is always true). >Is provability really relevant? Philosophers and physicists find >it sexy for its Goedelian limits. But what does this have to do with >the set of possible universes? Wait and see. Remember I told George we have not yet really beging the proof. The hard and tiedous thing is to arithmetise the provability predicate. I will define knowledge and "observable" (in the UDA sense) *in* the language of the machine and I will show that the observable propositions obeys some quantum logic. I will only consider the case observable with a probability one. This will give a concrete purely arithmetical interpretation of a quantum logic. The probabilities are taken on the set of relative consistent (UD accessible) extensions, and by consistent I just mean "-[]-" with [] Goedel's provability predicate. (so you can guess the role of provability). The UD will be translated in the form of the set of all (true) \Sigma_1 sentences. >Is provability really relevant? Philosophers and physicists find >it sexy for its Goedelian limits. But what does this have to do with >the set of possible universes? It has to do with the origin of the belief in universe(s) once we bet we do survive digital substitution. >I believe the provability discussion distracts a bit from the >real issue. If we limit ourselves to universes corresponding to >traditionally provable theorems then we will miss out on many formally >and constructively describable universes that are computable in the >limit yet in a certain sense soaked with unprovable aspects. Actually, provability is just a step in my derivation (and we have still not begin to discusse it! nor to define it). We have just seen some modal logic which have a priori nothing to do with provability. You are still anticipating. It is a good thing you are open to unprovable aspects, and it makes weirder you are not open to uncomputable aspects. (Although I know provability is relative and computability is absolute (Church's Thesis) Do you really believe than one of us limit "universes" to sets of provable theorems. I am myself just defining the local *discourse* of a machine-scientist. >Such a virtual reality or universe is perfectly well-defined. At some >point each history prefix will remain stable forever. Even if we know p >and q, however, in general we will never know for sure whether some q(n) >that is still zero won't flip to 1 at some point, because of Goedel etc. >So this universe features lots of unprovable aspects. I have no problem with that. As you should know from our earlier discussion. Remember that the big role in my work comes from (G* minus G), which is a logic of the *unprovable* statements. G ang G* will be defined formally soon, but you can also consult Solovay 1976 or Boolos ... By logic here I mean a well defined set (of formulas) logically closed for modus ponens. >Note also that observers evolving within the universe ... The UDA shows that such an expression has no meaning. The movie graph (or Maudlin's Olympia) illustrates how non trivial the "mind-body" problem is with comp. I am aware there is something very hard to swallow here. But it is a consequence of comp. > ...may write >books about all kinds of unprovable things; they may also write down >inconsistent axioms; etc. All of this is computable though, since the >entire universe history is. So again, why should provability matter? It matters for the same reason which makes you proving theorems in your papers. Proving is just a polite way to communicate third person propositions. You believe that we are modelising universes with proofs, when we are just interviewing sound machines on their possible extension in UD*. If we are sound machines, it is natural to be interested in what those sound machines can prove about themselves, what they can know about themselves, what part of themselves they can observe, and on which computational consistent extensions they can bet, etc. All the term in the preceding sentence will be formally defined and tranlated in arithmetic (the language of a sound UTM I will use). The conclusion will be independent of the language chosen. Bruno