Re: Does provability matter?

2001-12-19 Thread Juergen Schmidhuber


Wei Dai wrote:
> I don't understand how you can believe that the probability of more
> dominant priors is zero. That implies if I offered you a bet of $1
> versus your entire net worth that large scale quantum computation will
> in fact work, you'd take that bet. Would you really?

Your dollar against my 2 cents worth? I don't want to rip you off!

Ok, let me adopt a more careful Bayesian's fallback position: I just
assume certain things, then derive consequences, given the assumptions,
without precisely quantifying the plausibility of the assumptions 
themselves, letting the reader decide whether they are plausible or not.

Juergen




Re: Does provability matter?

2001-12-11 Thread Wei Dai

I don't understand how you can believe that the probability of more
dominant priors is zero. That implies if I offered you a bet of $1
versus your entire net worth that large scale quantum computation will
in fact work, you'd take that bet. Would you really?

On Tue, Dec 11, 2001 at 04:24:46PM +0100, Juergen Schmidhuber wrote:
> Wei Dai wrote:
> > I'm not sure I understand this. Can you give an example of how our
> > universe might make use of an entire continuum of real numbers? How might
> > someone show this if it were true?
> 
> I have no idea. In fact, I guess it is impossible.
> 
> > But if there is a formally describable prior that dominates the speed
> > prior, and you agree that the more dominant prior doesn't have a prior
> > probability of zero, then isn't the speed prior redundant? Wouldn't you
> > get equal posterior probabilities (up to a constant multiple) by
> > dropping the speed prior from your prior on priors, no matter what it
> > assigns to priors that are not formally describable?
> 
> In the Bayesian framework we derive consequences of assumptions
> represented as priors. The stronger the assumptions, the more specific
> the
> predictions. The Speed Prior assumption is stronger than the assumption
> of a formally describable prior. It is not redundant because it yields
> stronger
> predictions such as: The computer computing our universe won't compute
> much more of it; large scale quantum computation won't work; etc.
> 
> In fact, I do believe the Speed Prior dominates the true prior from
> which our universe is sampled (which is all I need to make good
> computable predictions), and that the probability of even more
> dominant priors is zero indeed. But as a Bayesian I sometimes ignore
> my beliefs and also derive consequences of more dominant priors.
> I do find them quite interesting, and others who do not share my
> belief in the Speed Prior might do so too.
> 
> Juergen Schmidhuber
> 
> http://www.idsia.ch/~juergen/
> http://www.idsia.ch/~juergen/everything/html.html
> http://www.idsia.ch/~juergen/toesv2/




Re: Does provability matter?

2001-12-11 Thread Juergen Schmidhuber

Wei Dai wrote:
> I'm not sure I understand this. Can you give an example of how our
> universe might make use of an entire continuum of real numbers? How might
> someone show this if it were true?

I have no idea. In fact, I guess it is impossible.

> But if there is a formally describable prior that dominates the speed
> prior, and you agree that the more dominant prior doesn't have a prior
> probability of zero, then isn't the speed prior redundant? Wouldn't you
> get equal posterior probabilities (up to a constant multiple) by
> dropping the speed prior from your prior on priors, no matter what it
> assigns to priors that are not formally describable?

In the Bayesian framework we derive consequences of assumptions
represented as priors. The stronger the assumptions, the more specific
the
predictions. The Speed Prior assumption is stronger than the assumption
of a formally describable prior. It is not redundant because it yields
stronger
predictions such as: The computer computing our universe won't compute
much more of it; large scale quantum computation won't work; etc.

In fact, I do believe the Speed Prior dominates the true prior from
which our universe is sampled (which is all I need to make good
computable predictions), and that the probability of even more
dominant priors is zero indeed. But as a Bayesian I sometimes ignore
my beliefs and also derive consequences of more dominant priors.
I do find them quite interesting, and others who do not share my
belief in the Speed Prior might do so too.

Juergen Schmidhuber

http://www.idsia.ch/~juergen/
http://www.idsia.ch/~juergen/everything/html.html
http://www.idsia.ch/~juergen/toesv2/




Re: Does provability matter?

2001-11-29 Thread Wei Dai

On Wed, Nov 28, 2001 at 05:27:43PM +0100, Juergen Schmidhuber wrote:
> Which one? Hm. Let me extend your question and ask: what's the
> probability
> that the Great Programmer is more than a mere programmer in the sense
> that he is not bound by the limits of computability?  For instance,
> if someone were able to show that our universe somehow makes use of an
> entire continuum of real numbers we'd be forced to accept some even more
> dominant prior that is not even computable in the limit.  We could not
> even formally specify it.

I'm not sure I understand this. Can you give an example of how our
universe might make use of an entire continuum of real numbers? How might
someone show this if it were true?

> So what's my prior on all priors? Since the attempt to answer such a
> question might lead outside what's formally describable, I'll remain 
> silent for now.

But if there is a formally describable prior that dominates the speed
prior, and you agree that the more dominant prior doesn't have a prior
probability of zero, then isn't the speed prior redundant? Wouldn't you
get equal posterior probabilities (up to a constant multiple) by
dropping the speed prior from your prior on priors, no matter what it
assigns to priors that are not formally describable?




Re: Does provability matter?

2001-11-28 Thread Juergen Schmidhuber

Wei Dai wrote:
>
> On Thu, Nov 15, 2001 at 10:35:58AM +0100, Juergen Schmidhuber wrote:
> > > Why do you prefer the Speed Prior? Under the Speed Prior, oracle universes
> > > are not just very unlikely, they have probability 0, right? Suppose one
> > > day we actually find an oracle for the halting problem, or even just find
> > > out that there is more computing power in our universe than is needed to
> > > explain our intelligence. Would you then (1) give up the Speed Prior and
> > > adopt a more dominant prior, or (2) would you say that you've encountered
> > > an extremely unlikely event (i.e. more likely you're hallucinating)?
> > >
> > > If you answer (1) then why not adopt the more dominant prior now?
> >
> > Why not adopt a more dominant prior now? I just go for the simplest
> > explanation consistent with available data, where my simplicity measure
> > reflects what computer scientists find simple: things that are easy
> > to compute.
>
> You didn't explicitly answer my question about what you would do if you
> saw something that is very unlikely under the Speed Prior but likely under
> more dominant priors, but it seems that your implicit answer is (1). In
> that case you must have some kind of prior (in the Baysian sense) for the
> Speed Prior vs. more dominant priors. So where does that prior come from?
>
> Or let me put it this way. What do you think is the probability that the
> Great Programmer has no computational resource constraints? If you don't
> say the probability is zero, then what you should adopt is a weighted
> average of the Speed Prior and a more dominant prior, but that average
> itself is a more dominant prior. Do you agree?

If someone can use large scale quantum computing to solve a problem
whose
solution requires much more computation time than necessary to compute
the history of our own particular universe, then one could take this
as evidence against the Speed Prior.  You are right: to quantify this
evidence in a Bayesian framework we need a prior on priors.

Which one? Hm. Let me extend your question and ask: what's the
probability
that the Great Programmer is more than a mere programmer in the sense
that he is not bound by the limits of computability?  For instance,
if someone were able to show that our universe somehow makes use of an
entire continuum of real numbers we'd be forced to accept some even more
dominant prior that is not even computable in the limit.  We could not
even formally specify it.

So what's my prior on all priors? Since the attempt to answer such a
question might lead outside what's formally describable, I'll remain 
silent for now.

Juergen Schmidhuber

http://www.idsia.ch/~juergen/
http://www.idsia.ch/~juergen/everything/html.html
http://www.idsia.ch/~juergen/toesv2/




Re: Does provability matter?

2001-11-16 Thread Marchal

Quick, but not so quick, comment on Wei Dai, Juergen Schmidhuber 
and Charles Goodwin. (I'm busy). 
Apologises in advance for some length, though, I
guess you are busy too.
Apology also to those EverythingFOR-listers who get this
message twice. That's the effect of interference
of parallel lists, it doubles the intensity at some point :)


Wei Dai wrote (in the everything-list):

> On Wed, Oct 31, 2001 at 10:49:41AM +0100, Juergen Schmidhuber wrote:
> > Which are the logically possible universes?  Tegmark mentioned a
> > somewhat
> > vaguely defined set of ``self-consistent mathematical structures,''
> > implying provability of some sort. The postings of Marchal also focus
> > on what's provable and what's not.
>
> Do you understand Marchal's postings? I really have trouble making sense
> of them. If you do, would you mind rephrasing his main ideas for me?



And Juergen Schmidhuber answered:


>No, unfortunately I do not understand him. But provability does seem
>important to him.  Maybe someone else could post a brief and concise
>summary?


What about telling me if it is the UDA or the Arithmetical UDA (AUDA) you
have problem with.

In case it is the UDA (that is the proof that comp entails a necessary
reversal between physics and machine/psychologycomputer-science/number
theory) it would be helpful if you tell me which step you don't understand
in the UDA in 11 steps. 
(cf   http://www.escribe.com/science/theory/m3044.html  ). Frankly.

In case it is the AUDA, (the translation of UDA in arithmetic or in any
language of a sound UM) the difficulty of understanding is more normal,
because the AUDA needs some familiarity with Logic (Goedel Loeb ...).
The importance of provability comes from the fact that like Judson
Webb or John Myhill (ref in my thesis) I consider Godel's 2th theorem as 
(the first) theorem in exact psychology, in particular machine 
psychology: 
a consistent machine cannot prove its own consistency, or a machine 
cannot prove she has (even just one) consistent extension(s). 
Hume is right, and provable with comp, indeed.
Now the UDA proves that our "physics" is defined by a measure
on those consistent extensions. So the concept of consistency is very
important, and it is defined from the concept of provability: p is
consistent iff -p is not provable (-[]-p, = <>p).

Modal logic makes works on self-referential machine "easy", at least
with some familiarity in logic. Have you follow my "little course" to 
George Levy on modal logic?

But in case you have not understand UDA, perhaps AUDA is premature, I
don't know, logicians understand more easily AUDA, at least formally.


I know a lot of people here developpe similar ideas. I bet a lot of
children, especially the dreamer one, brush against the idea.
And indeed many ScFi writers, like Daniel Galouye in SIMULACRON III, makes
quasi rigorously the point. Still I'm sorry/happy for what
is perhaps some advance from my part :-) I )-: 
Simplifying a little bit I made
public the "UDA" including "amoeba-immortality" the ancestor
of "comp-immortality" in 1963. (ok I was young!). I was interested in
amoeba life-time. After that my brain became a battle field between
biology (which will give comp) and chemistry (making me doubt about
comp and becoming eventually the very shape of the comp-doubt).
James Watson says "cells obeys to the laws of chemistry". 
To obvious to be true. 

I got and proposed the idea of translating such UDA-like
question, in the Godel way, in arithmetic, in 1971, including the 
conjecture 
that QM or chemistry should be justified in that way, and (admittedly a
subtil point) that chemistry was a product of the necessity of the
doubt about comp so that matter is defined by a measure on our
ignorance about our possible extensions. 

That has given
a project of a thesis I made precise in 1976. The project (and other 
projects more "serious" in pure math) have been 
rejected, and things of life slowed me down a little bit, let us
say, untill I will publish, under the pression of sympathic belgium
logicians but also engineers, the whole thing in the Toulouse 
(France) 1988 paper, and  more concisely in 1991.

I will get the proof of LASE (Little Schroedinger Abstract
Equation) only in 1994. This is the first confirmation that not only
comp and its reversal are consistent, but that it is going in the
quantum/chemistry direction as I expected (it is empirically consistent).

You can see that, although I believe the empiry should be explain
by the logical and arithmetical, I really come from the empirical
science. My childhood was contemplation of amoeba, planaria, hydra,
all the animals, vegetals and minerals.

Until 1995 I was sure that someone would find a fatal error either
in UDA or in the arithmetical UDA. In the beginning nineties Brussels
University encourages me to make a Phd Thesis which (for administrative 
reason!) I have been asked to propose first as project (again) in 1995.
The project-thesis has been judge non receivable

Re: Does provability matter?

2001-11-15 Thread Wei Dai

On Thu, Nov 15, 2001 at 10:35:58AM +0100, Juergen Schmidhuber wrote:
> > Why do you prefer the Speed Prior? Under the Speed Prior, oracle universes
> > are not just very unlikely, they have probability 0, right? Suppose one
> > day we actually find an oracle for the halting problem, or even just find
> > out that there is more computing power in our universe than is needed to
> > explain our intelligence. Would you then (1) give up the Speed Prior and
> > adopt a more dominant prior, or (2) would you say that you've encountered
> > an extremely unlikely event (i.e. more likely you're hallucinating)?
> >
> > If you answer (1) then why not adopt the more dominant prior now?
>
> Why not adopt a more dominant prior now? I just go for the simplest
> explanation consistent with available data, where my simplicity measure
> reflects what computer scientists find simple: things that are easy
> to compute.

You didn't explicitly answer my question about what you would do if you
saw something that is very unlikely under the Speed Prior but likely under
more dominant priors, but it seems that your implicit answer is (1). In
that case you must have some kind of prior (in the Baysian sense) for the
Speed Prior vs. more dominant priors. So where does that prior come from? 

Or let me put it this way. What do you think is the probability that the
Great Programmer has no computational resource constraints? If you don't
say the probability is zero, then what you should adopt is a weighted
average of the Speed Prior and a more dominant prior, but that average
itself is a more dominant prior. Do you agree?




Re: Does provability matter?

2001-11-15 Thread Juergen Schmidhuber

Wei Dai wrote:
>
> Thanks for clarifying the provability issue. I think I understand and
> agree with you.
>
> On Tue, Nov 13, 2001 at 12:05:22PM +0100, Juergen Schmidhuber wrote:
> > What about exploitation? Once you suspect you found the PRG you can use
> > it
> > to predict the future. Unfortunately the prediction will take enormous
> > time to stabilize, and you never can be sure it's finished.
> > So it's not very practical.
>
> By exploiting the fact that we're in an oracle universe I didn't mean
> using TMs to predict the oracle outputs. That is certainly impractical.
>
> There are a couple of things you could do though. One is to use some
> oracle outputs to predict other oracle outputs when the relationship
> between them is computable. The other, much more important, is to quickly
> solve arbitrarily hard computational problem using the oracles.
>
> > I prefer the additional resource assumptions reflected
> > by the Speed Prior.  They make the oracle universes very unlikely, and
> > yield computable predictions.
>
> Why do you prefer the Speed Prior? Under the Speed Prior, oracle universes
> are not just very unlikely, they have probability 0, right? Suppose one
> day we actually find an oracle for the halting problem, or even just find
> out that there is more computing power in our universe than is needed to
> explain our intelligence. Would you then (1) give up the Speed Prior and
> adopt a more dominant prior, or (2) would you say that you've encountered
> an extremely unlikely event (i.e. more likely you're hallucinating)?
>
> If you answer (1) then why not adopt the more dominant prior now?

You are right in the sense that under the Speed Prior any complete
_infinite_ oracle universe has probability 0. On the other hand,
any _finite_ beginning of an oracle universe has nonvanishing
probability. Why? The fastest algorithm for computing all universes
computes _all_ finite beginnings of all universes. Now oracle universes
occasionally require effectively random bits.  History beginnings that
require n such bits come out very slowly: the computation of the n-th
oracle bit requires more than O(2^n) steps, even by the fastest
algorithm.
Therefore, under the Speed Prior the probabilities of oracle-based
prefixes quickly converge towards zero with growing prefix size. But in
the finite case there always will remain some tiny epsilon.

Why not adopt a more dominant prior now? I just go for the simplest
explanation consistent with available data, where my simplicity measure
reflects what computer scientists find simple: things that are easy
to compute.


Juergen Schmidhuber

http://www.idsia.ch/~juergen/
http://www.idsia.ch/~juergen/everything/html.html
http://www.idsia.ch/~juergen/toesv2/




Re: Does provability matter?

2001-11-14 Thread Wei Dai

Thanks for clarifying the provability issue. I think I understand and
agree with you.

On Tue, Nov 13, 2001 at 12:05:22PM +0100, Juergen Schmidhuber wrote:
> What about exploitation? Once you suspect you found the PRG you can use
> it
> to predict the future. Unfortunately the prediction will take enormous
> time to stabilize, and you never can be sure it's finished.  
> So it's not very practical. 

By exploiting the fact that we're in an oracle universe I didn't mean
using TMs to predict the oracle outputs. That is certainly impractical.

There are a couple of things you could do though. One is to use some
oracle outputs to predict other oracle outputs when the relationship
between them is computable. The other, much more important, is to quickly
solve arbitrarily hard computational problem using the oracles.

> I prefer the additional resource assumptions reflected
> by the Speed Prior.  They make the oracle universes very unlikely, and
> yield computable predictions.

Why do you prefer the Speed Prior? Under the Speed Prior, oracle universes
are not just very unlikely, they have probability 0, right? Suppose one
day we actually find an oracle for the halting problem, or even just find
out that there is more computing power in our universe than is needed to
explain our intelligence. Would you then (1) give up the Speed Prior and
adopt a more dominant prior, or (2) would you say that you've encountered
an extremely unlikely event (i.e. more likely you're hallucinating)?

If you answer (1) then why not adopt the more dominant prior now?




Re: Does provability matter?

2001-11-13 Thread Juergen Schmidhuber


Wei Dai wrote:
>
> On Wed, Oct 31, 2001 at 10:49:41AM +0100, Juergen Schmidhuber wrote:
> > Which are the logically possible universes?  Tegmark mentioned a
> > somewhat
> > vaguely defined set of ``self-consistent mathematical structures,''
> > implying provability of some sort. The postings of Marchal also focus
> > on what's provable and what's not.
>
> Do you understand Marchal's postings? I really have trouble making sense
> of them. If you do, would you mind rephrasing his main ideas for me?

No, unfortunately I do not understand him. But provability does seem
important to him.  Maybe someone else could post a brief and concise
summary?

> > 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?
>
> What does it mean for a universe to be "provable"? One interpretation is
> that there exists an algorithm to compute any finite time-space region of
> the universe that always halts. Is that what you mean?

Well, any finite object x has a halting algorithm that computes it.
So which are the unprovable things? They are formal statements such as
"algorithm x will eventually compute object y." If it does then you can
prove it, otherwise in general you can never be sure. But why identify
universes with true or false statements? When I'm asking "Is provability
really relevant?" I am not really referring to "provable universes" -
I don't even know what that is supposed to be. I just mean: why should
it be important to show that a particular algorithm computes a
particular
universe? Or that a particular universe has a particular property (there
are many generally unprovable properties)?  Let's compute them all -
why worry about provability?

> > The provability discussion seems to distract 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 unprovability.
> >
> > Example: a never ending universe history h is computed by a finite
> > nonhalting program p. To simulate randomness and noise etc, p invokes
> > a short pseudorandom generator subroutine q which also never halts. The
> > n-th pseudorandom event of history h is based on q's  n-th output bit
> > q(n)
> > which is initialized by 0 and set to 1 as soon as the n-th statement in
> > an ordered list of all possible statements of a formal axiomatic system
> > is proven by a theorem prover that systematically computes all provable
> > theorems.  Whenever q modifies some q(n) that was already used in the
> > previous computation of h, p appropriately recomputes h since the n-th
> > pseudorandom event.
>
> Living in this universe is like living in a universe with a
> halting-problem oracle, right? If you want to know whether program x
> halts, you just measure the n-th pseudorandom event, where n is such that
> the n-th theorem is "x halts." Yes?

Yes. Once the history has stabilized this will give you the correct
answer.

> The problem with universes with halting-problem oracles (which I'll just
> call oracle universes) is that either the oracle is not exploitable
> (for example if no one in the universe figures out that the pseudorandom
> events actually correspond to theorems) in which case the universe just
> looks like an ordinary "provable" universe, or the oracle is
> exploitable, in which case the outcome becomes completely unimaginable for
> us. (Or is that not true? Can we imagine what would happen if an
> intelligent species came across an exploitable halting-problem oracle?)
>
> > But why should this lack of provability matter?  Ignoring this universe
> > just implies loss of generality.  Provability is not the issue.
>
> If oracle universes could exist, how significant are they? What's
> the probability that we live in such a universe, and how could we try to
> determine and/or exploit this fact?

If the computer on which the history of our universe is calculated is a
general Turing machine (as opposed to a monotone machine which cannot
edit
previous outputs), and if we make no resource assumptions such as those
embodied by the Speed Prior, then the oracle universes indeed represent
a large fraction of the probability mass of all universes. Why? Because
there are many oracle universes with very short algorithms.

How to determine whether we are in an oracle universe? In principle it
is possible, at least to the extent inductive inference is possible at
all! Just search through all oracle pseudo-random generators (PRGs) and
try to match their outputs with the apparently noisy observations. If
the observations are not really random, eventually you'll stumble across
the right PRG. It's just that you cannot prove that it is the right one,
or that its outputs have already stabilized.

What about exploitation? Once you suspec

Re: Does provability matter?

2001-11-02 Thread Wei Dai

On Fri, Nov 02, 2001 at 04:29:26PM -0800, [EMAIL PROTECTED] wrote:
> What about the instantiations of people who measure the event the other
> way before the universe gets restarted and re-run from that point?  They
> would see the wrong answer to the halting question, but they are just
> as conscious as the people who later see the right answer.

The people who see the wrong answer have zero measure because they exist
for only a finite amount of time on the output tape whereas the people who
see the right answer exist for an infinite amount of time on the output
tape.




Re: Does provability matter?

2001-11-02 Thread hal

Wei Dai writes:
> Living in this universe is like living in a universe with a
> halting-problem oracle, right? If you want to know whether program x
> halts, you just measure the n-th pseudorandom event, where n is such that
> the n-th theorem is "x halts." Yes? 

What about the instantiations of people who measure the event the other
way before the universe gets restarted and re-run from that point?  They
would see the wrong answer to the halting question, but they are just
as conscious as the people who later see the right answer.

Hal




Re: Does provability matter?

2001-11-02 Thread Wei Dai

On Wed, Oct 31, 2001 at 10:49:41AM +0100, Juergen Schmidhuber wrote:
> Which are the logically possible universes?  Tegmark mentioned a
> somewhat
> vaguely defined set of ``self-consistent mathematical structures,''
> implying provability of some sort. The postings of Marchal also focus
> on what's provable and what's not.

Do you understand Marchal's postings? I really have trouble making sense
of them. If you do, would you mind rephrasing his main ideas for me?

> 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?

What does it mean for a universe to be "provable"? One interpretation is
that there exists an algorithm to compute any finite time-space region of
the universe that always halts. Is that what you mean? 

> The provability discussion seems to distract 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 unprovability.
> 
> Example: a never ending universe history h is computed by a finite
> nonhalting program p. To simulate randomness and noise etc, p invokes
> a short pseudorandom generator subroutine q which also never halts. The
> n-th pseudorandom event of history h is based on q's  n-th output bit
> q(n)
> which is initialized by 0 and set to 1 as soon as the n-th statement in
> an ordered list of all possible statements of a formal axiomatic system
> is proven by a theorem prover that systematically computes all provable
> theorems.  Whenever q modifies some q(n) that was already used in the
> previous computation of h, p appropriately recomputes h since the n-th
> pseudorandom event.

Living in this universe is like living in a universe with a
halting-problem oracle, right? If you want to know whether program x
halts, you just measure the n-th pseudorandom event, where n is such that
the n-th theorem is "x halts." Yes? 

The problem with universes with halting-problem oracles (which I'll just
call oracle universes) is that either the oracle is not exploitable
(for example if no one in the universe figures out that the pseudorandom
events actually correspond to theorems) in which case the universe just
looks like an ordinary "provable" universe, or the oracle is
exploitable, in which case the outcome becomes completely unimaginable for
us. (Or is that not true? Can we imagine what would happen if an
intelligent species came across an exploitable halting-problem oracle?)

> But why should this lack of provability matter?  Ignoring this universe
> just implies loss of generality.  Provability is not the issue.

If oracle universes could exist, how significant are they? What's
the probability that we live in such a universe, and how could we try to
determine and/or exploit this fact?




Re: Does provability matter?

2001-11-01 Thread Marchal

Juergen Schmidhuber wrote:


>Which are the logically possible universes?  Tegmark mentioned a
>somewhat
>vaguely defined set of ``self-consistent mathematical structures,''
>implying provability of some sort. The postings of Marchal also focus
>on what's provable and what's not.
>
>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?


Because I interpret "possible universe" or "possible model of p" by "p
belongs to a model" or "p belongs to a consistent extension", which I
translate in arithmetic by "p is consistent" that is by "-p is not 
provable" (-[]-p). (By Godel's *completeness* theorem it is extensionnaly
equivalent).


>The provability discussion seems to distract 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 unprovability.


But *all* our consistent extensions are soaked with unprovability.
And the UDA shows *all* of them must be taken into account.
'Probability one of p' will be when 1) and 2)

1) []p, provable('p'), = p is true in all, if any, "possible universe".
2) <>p  consistent('p') = there is a possible universe with p.

(I use Godel *completeness* theorem for first order logic, here, but 
a more sophisticated presentation can be made (G and G* 
works on second order arithmetic as well, but I don't want to be too
technical)).

So I translate probability one of p by "[]p & <>p". The
incompleteness theorems makes that moves no less trivial than
the translation of "knowing p" by "provable(p) & p" which gives
an arithmetical interpretation of intuitionist logic.

The comp restriction to UD*, the trace of the UD, is translated
in arithmetic by a restriction of p by \Sigma_1 sentences p (this
includes universal \Sigma_1 sentences). Universality (with
comp) is \Sigma_1 completeness (+ oracle(s), etc.).

This gives the quasi Brouwersche modal logics Z1*. (I get
interesting quantum smelling logics also with the translation of
"feeling really p" by "[]p & <>p & p", the X1* logic. 
I conjecture Z1* gives an arithmetical quantum logic.
(X1*, Z0*, XO* are interesting variant, the X* minus X
are expected to play the role of a qualia logic, (for the
true mesurable but unprovable atomic propositions).


>Example: a never ending universe history h is computed by a finite
>nonhalting program p. To simulate randomness and noise etc, p invokes
>a short pseudorandom generator subroutine q which also never halts. The
>n-th pseudorandom event of history h is based on q's  n-th output bit
>q(n)
>which is initialized by 0 and set to 1 as soon as the n-th statement in
>an ordered list of all possible statements of a formal axiomatic system
>is proven by a theorem prover that systematically computes all provable
>theorems.  Whenever q modifies some q(n) that was already used in the
>previous computation of h, p appropriately recomputes h since the n-th
>pseudorandom event.
>
>Such a virtual reality or universe is perfectly well-defined.  We can
>program it. 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.


Sure.


>But why should this lack of provability matter?...


Because UDA shows that our future is a sort
of mean on the unprovable things (our consistent extensions,
unprovable by incompleteness). 

The miracle is the sharing and cohering part of those
extensions. I don't pretend having explained that miracle.
But UDA says where you must look for the explanation, and
the translation of the UDA in arithmetic gives an encouraging step
toward quantum logic, and even quale logics. 
(Linking J.S. Bell and J.L. Bell btw, ref in my thesis). 


>...Ignoring this universe
>just implies loss of generality.  Provability is not the issue.


  You are postulating a computable universe. And you believe, like
some physicist that an explanation of that universe is an explanation
for everything (discarding completely the "mind-body" problem).

  I am NOT postulating a computable universe. I am not even 
postulating a universe at all.
I postulate only *physicists*, in a very large sense 
of the word. I postulate that they are (locally) computable. 


I postulate only arithmetical truth and its many consistent
internal interpretations.

Provability is not really the issue indeed. It is the border between 
provability and unprovability which is the issue.
G* \ G gives insightful informations about that, including the
'probability on the uncomputable' issue.

Although I give theorem provers for the Z logic, question like
what is the status of the Arithmetical Bell's Inequality: