Measuring the strength of a theory (Was Re: Raatikainen's critique of Chaitin)

From: Eray Ozkural exa (erayo_at_bilkent.edu.tr)
Date: 09/06/04 

Date: 6 Sep 2004 07:51:16 -0700

[First: I am not changing the target. We have been discussing the
plausibility of using Kolmogorov complexity to measure theorem proving
power a la Chaitin.]

jesse@phiwumbda.org (Jesse F. Hughes) wrote in message news:<877jr8rb3e.fsf@phiwumbda.org>...
> erayo@bilkent.edu.tr (Eray Ozkural exa) writes:
>
> > For instance, if the inference rule which you have picked is classical
> > logic, then the case about theorem proving power explained in
> > Raatikainen's paper does occur. But it does not hold in general!
> > That's why Raatikanen's argument is flawed I believe. (That is: I can
> > invent an inference rule that simply discards "forall x, x=x"....)
>
> So the new theorem is: There is a set of inference rules such that
> complexity of the axioms is a measure of the strength of the theory.
>
> Is that it?
>
> That hardly sounds so exciting as the other version, which applies to
> the logics that folks actually care about.

Not exactly I think. But please do not blame me if my following ideas
do not work for you, I will be pointing at new stuff.

I am not saying that "there is a set of inference rules such that
complexity of the axioms is a measure of the strength of the theory",
since we give no proof, either, that there is always such an FAS that
obtains a mathematical truth from complex axioms. Consider my example
in a previous post:

Let's have this infinitesimal pin and pick a random number between 0
and 1. The probability that the random real we picked is Omega is
almost 0! (But not 0!) That is, if we wanted to solve the halting
problem, having a truly truly random, very real number would be of
absolutely no use! Although the complexity of a random real is just as
much as the number Omega, it normally contains no information about
the halting problem. Unfortunately!

It is obvious that a random string can have large complexity, but for
relevance to theorem proving we would also like it to be meaningful.
We can formalize this meaning as the following (like in computability
in the limit). Consider

H(a / r)

ie. entropy of (the coding of) an answer a to a mathematical problem,
with respect to a real number r. The meaningfulness of r for a is then
mutual information among two strings H(x:y) = H(a) - H(a/r), how much
information gained by looking at r.

For instance a0 could be this: ith bit of a0 is 1 if program i halts
(wrt a universal computer U), 1 if it does not.

It is obvious that
  H( a0 / Omega) = O(1)
since there is a nonhalting program which can solve the halting
problem using omega. (the program's size is constant.) That is why, I
am saying that Omega is maximally informative wrt halting problem
since any conditional program could be shorter *only by a constant
factor*. (and hence H(a0/Omega)=infinite, what bettter maximal than
the infinite?!)

Another example involving Omega.

Let a1 be encoded as follows, it is a sequence of numbers such that
ith number is the value of BB_LISP(k) [the maximum output size of any
k-bit long LISP program]. Since H(a1/a0) = O(1), H(a1/Omega) = O(1) as
well.

Let's now come to Torkel's hypothetical number a3, a number encoding
the truth of arithmetic sentences in first-order language of
arithmetic as an exercise. ith bit of a3 is 1 if ith sentence is true,
otherwise 0. What is H(a3/Omega)?

Nevertheless, the probability that a random real r gives any
information on the halting problem is pretty low because in an
uncountably infinite number of cases H(a0 / r) = infinite, knowing r
doesn't help us at all. We still need an infinite amount of
information to solve it. :(

How do we then incorporate truth into the theory? I suspect something
like formalizing model theory in algorithmic terms will be necessary.
Semantic strings as the above is a way, surely, why not, but these are
our constructs, they are toys. The entropy in a semantic space must be
calculated, but do not ask me how that is done. I do not know yet.

Regards, 

--
Eray Ozkural
PS: My gut feeling is that the results will be Wittgensteinean, we
will find that empirical trials are painfully necessary to do
mathematics!

Relevant Pages

  • Measuring the strength of a theory (Was Re: Raatikainens critique of Chaitin)
    ... plausibility of using Kolmogorov complexity to measure theorem proving ... > complexity of the axioms is a measure of the strength of the theory. ... The probability that the random real we picked is Omega is ... am saying that Omega is maximally informative wrt halting problem ...
    (sci.math)
  • Re: Raatikainens critique of Chaitin
    ... in this case infinite complexity. ... Omega can be said to represent halting problem's structure ... Here is a definition of randomness in Kolmogorov complexity: ... A real r is Chaitin random if the information content of the initial ...
    (comp.theory)
  • Re: Raatikainens critique of Chaitin
    ... in this case infinite complexity. ... Omega can be said to represent halting problem's structure ... Here is a definition of randomness in Kolmogorov complexity: ... A real r is Chaitin random if the information content of the initial ...
    (sci.math)
  • Re: Yet another Attempt at Disproving the Halting Problem
    ... nothing to do with physical computers. ... Since the only change multiple tapes provide ... is to the order of computational complexity, ... contribute to the solution of The Halting Problem. ...
    (comp.theory)
  • Re: Yet another Attempt at Disproving the Halting Problem
    ... nothing to do with physical computers. ... Since the only change multiple tapes provide ... is to the order of computational complexity, ... contribute to the solution of The Halting Problem. ...
    (sci.logic)