Re: Raatikainen's Complexity Complex
From: David Bernier (david250_at_videotron.ca)
Date: 07/26/04
- Next message: Marc Goodman: "Re: Disproof of the Halting Problem's Conclusion"
- Previous message: stephen_at_nomail.com: "Re: Disproof of the Halting Problem's Conclusion"
- In reply to: Eray Ozkural exa: "Re: Raatikainen's Complexity Complex"
- Next in thread: Eray Ozkural exa: "Re: Raatikainen's Complexity Complex"
- Reply: Eray Ozkural exa: "Re: Raatikainen's Complexity Complex"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Date: Mon, 26 Jul 2004 16:30:07 -0400
Eray Ozkural exa wrote:
> Hello David,
>
> David Bernier <david250@videotron.ca> wrote in message news:<t1uJc.6160$Q66.59012@wagner.videotron.net>...
>
>>I believe I understand your point. At best, the complexity of
>>an axiomatic system gives a rough upper bound on its
>>proving-strength ( assuming its aritmetical theorems
>>are all true.)
>>
>>But I think that things are worse than that for the
>>view that complexity of axiom systems (even looking
>>only at those which are "concise") relates well to
>>proving strength.
>>
>>Considering extensions of Peano Arithmetic of the form:
>>
>> PA + "The Turing machine with K
>> states and transition table [ insert table] doesn't
>> halt when starting with a blank tape.",
>>
>>[ K need not be "huge", say K<= 10^6 is conceivable ]
>>
>>which are (a) strict extensions of PA and (b) arithmetically true,
>>
>>I believe one can prove that there exist (say) at least
>>a trillion distinct TMs T1, ... T_{10^12} with K states where
>>PA + "TM_i doesn't halt" is an arithmetically true
>>strict extension of PA for 1<=i<=10^12 (by strict extension I just
>>mean that "TM_i doesn't halt" is undecidable in PA), and
>>where, for any i such that 1<=i <=10^12,
>
>
> Yes, I understand your extension. There will be many programs in that
> range with infinite loops, a fact which cannot be proved in PA. [+]
>
> The axioms PA + "TM_i doesn't halt" substantially enlarges the set of
> true theorems that can be derived with respect to PA. (Infinitely
> more, as discussed elsewhere) (labelled PA1).
>
>
>>the statement "TM_i doesn't halt" *is not* a theorem in the
>>"large" axiomatic system:
>>
>>PA+union_{j : 1<=j<=10^12, j=/= i} { axioms "TM_j doesn't halt"}. [*******]
>
>
> (labelled PA2)
>
> You mean that H(PA2) > H(PA1), but T(PA2) is not a superset of T(PA1)
> (where T(X) is the set of true theorems that can be derived from axiom
> set X to be precise), while we expect it to be such.
Yes, I claim that T(PA2) is not a superset of T(PA1). In particular,
as I said above, the true statement "TM_i does not halt" is not
a theorem of PA2.
You may recall that Chaitin gave an explicit exponential Diophantine
equation with a free variable (say x_0) such that the equation
C(x_0, .....)=0 has either 0 or infinitely many solutions (values for x_0)
with a 1 to 1 correspondence with the value of the x_0'th bit of
Chaitin's Omega_Lisp. Next, we may ask what is the largest n such that
all m in {1,2, ... n} can be written as a numeral with K characters or
fewer in PA? This largest n, say n(K), is >= c*log(K) for some c>0
fixed and assuming that K is sufficiently large [this is quite easy].
Next, if we know the K first bits of Omega_Lisp, what does this tell
us about the values BB(1), BB(2), BB(3), ... of Rado's uncomputable
Busy Beaver function? To give a precise answer, one would
need a Turing machine program to Lisp program translator;
but I strongly believe that with the first K bits of Omega_Lisp,
for sufficiently large K, one can compute BB(floor(c2*K)) for some
fixed positive c2.
Finally, we wish to use the above to get a contradiction somewhere.
First, the hypothesis is that for every positive d, there is
an arithmetically true strict extension of PA, say S_ell, such
that H(S_ell) <= d*ell and such that the value of BB(ell) is
known to S_ell (as a theorem) for every positive ell. Next, we
need a predicate of PA which says: " the TM with Godel number
N is a Busy Beaver Champion" (which means that any TM with
the same number of states as the TM referred to by the
Godel number N will either not halt, or halt no later than
the TM referred to by N does).
Then we construct a predicate MinBB(g) which has the meaning:
" g is the Godel number of a Busy Beaver Champion
for the number of states in the TM referred to by g, and
any Busy Beaver Champion with the same number of
states as the TM referred to by g has a Godel number of
at least g".
I'm afraid I can't complete this argument today.
The result [*******] above may be due to Solovay or Chaitin.
I believe Chaitin said and/or wrote something to the effect that
"to prove a twenty pound theorem, one needs twenty pounds
of axioms."
I agree that twenty pounds of axioms will be enough, but that
in some cases the twenty pound [complexity-wise] theorem
will be so hard that one must choose one's twenty
pounds of axioms very carefully.
David Bernier
> You seem to have a good argument. It seems to be an improved analogue
> of Raatikainen's argument, and in my opinion, more striking. I might
> be losing the debate!
> The interesting part for me is that individual halting problem
> instances are already irreducible (digits of Omega), so we seem to be
> talking at the right level this time instead of meaningless (a=a) kind
> of relations. Therefore, your argument may be stronger.
>
> However, there may be something quite counter-intuitive going on in
> your example. Maybe our expectations are not satisfied. I couldn't
> reach a conclusion, but let's not dismiss the fact that we are dealing
> with the first 10^12 digits of Omega: a remarkable finite random
> string. H(PA2) seems to be something like 10^12 - 1 + H(i) + O(1), not
> a very small entropy. (Please correct me if I'm wrong: I didn't prove
> it, I just thought of it and wrote it down here)
>
> My only concern right now is that your expectation above might not be
> realistic, why should T(PA2) subsume T(PA1) according to Chaitin's
> theory? Does your argument depend on this expectation?
>
> Thanks a lot for your thoughtful post; it has probably been the most
> challenging discussion I have participated in for a long time.
>
> Regards,
>
> --
> Eray Ozkural
>
> PS: Frankly, I've thought about your post quite a bit, and perhaps in
> the end it has been all the more confusing. I hope not :)
>
> [+] Axiom schemata like PA will have finite descriptive complexity,
> naturally, so they can be handled by our formalization.
- Next message: Marc Goodman: "Re: Disproof of the Halting Problem's Conclusion"
- Previous message: stephen_at_nomail.com: "Re: Disproof of the Halting Problem's Conclusion"
- In reply to: Eray Ozkural exa: "Re: Raatikainen's Complexity Complex"
- Next in thread: Eray Ozkural exa: "Re: Raatikainen's Complexity Complex"
- Reply: Eray Ozkural exa: "Re: Raatikainen's Complexity Complex"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Relevant Pages
|