Re: Provable vs Computable

From: Marchal <marchal.domain.name.hidden>
Date: Sat May 5 07:08:22 2001

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
Received on Sat May 05 2001 - 07:08:22 PDT