Logic Journal of IGPL

Logic Journal of IGPL Advance Access originally published online on June 7, 2009
Logic Journal of IGPL 2009 17(4):351-374; doi:10.1093/jigpal/jzp015

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by Calude, C. S. Articles by Hay, N. J. Social Bookmarking          What's this?

© The Author 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Every computably enumerable random real is provably computably enumerable random

Cristian S. Calude and Nicholas J. Hay

Department of Computer Science, University of Auckland, Private Bag 92019, Auckland, New Zealand
E-mail: cristian{at}cs.auckland.ac.nz,nickhay{at}cs.auckland.ac.nz

We prove that every computably enumerable (c.e.) random real is provable in Peano Arithmetic (PA) to be c.e. random. A major step in the proof is to show that the theorem stating that "a real is c.e. and random iff it is the halting probability of a universal prefix-free Turing machine" can be proven in PA. Our proof, which is simpler than the standard one, can also be used for the original theorem.

Our positive result can be contrasted with the case of computable functions, where not every computable function is provably computable in PA, or even more interestingly, with the fact that almost all random finite strings are not provably random in PA.

We also prove two negative results: a) there exists a universal machine whose universality cannot be proved in PA, b) there exists a universal machine U such that, based on U, PA cannot prove the randomness of its halting probability.

The paper also includes a sharper form of the Kraft-Chaitin Theorem, as well as a formal proof of this theorem written with the proof assistant Isabelle.

References

[1]  Brainerd WS, Landweber LH. Theory of Computation (1974) New York: Wiley.

[2]  Calude C. Chaitin numbers, Solovay machines and incompleteness, Theoret. Comput. Sci (2002) 284:269–277.[CrossRef]

[3]  Calude C. A characterization of c.e. random reals, Theoret. Comput. Sci (2002) 271:3–14.[CrossRef]

[4]  Calude CS. Information and Randomness. An Algorithmic Perspective (2002) 2nd Edition. Berlin: Springer Verlag. Revised and Extended.

[5]  Calude CS, Calude E, Marcus S. Proving and Programming. In: Randomness & Complexity, from Leibniz to Chaitin—Calude CS, ed. (2007) Singapore: World Scientific. 310–321.

[6]  Calude CS, Hertling P, Khoussainov B, Wang Y. Recursively enumerable reals and Chaitin numbers. Morvan M, Meinel C, Krob D, eds. (1998) Berlin: Springer–Verlag. 596–606. Proceedings of the 15th Symposium on Theoretical Aspects of Computer Science (Paris), Full paper in Theoret. Comput. Sci. 255 (2001), 125–149.

[7]  Chaitin G. A theory of program size formally identical to information theory, J. Assoc. Comput. Mach (1975) 22:329–340.

[8]  Chaitin GJ. Algorithmic Information Theory (1987) Cambridge: Cambridge University Press. (3rd printing 1990).

[9]  Chaitin GJ. The Limits of Mathematics (1998) Singapore: Springer.

[10]  Hales TC. Formal proof. Notices of the AMS (2008) 11:1370–1380.

[11]  Downey R, Hirschfeldt D. Algorithmic Randomness and Complexity. Heidelberg: Springer. to appear.

[12]  Fischer PC. Theory of provable recursive functions, Trans. Amer. Math. Soc (1965) 117:494–520.[CrossRef]

[13]  Hay NJ. Formal proof of the Kraft-Chaitin theorem in Isabelle. Available online at http://www.cs.auckland.ac.nz/~nickjhay/KraftChaitin.thy.

[14]  Hoyrup M, Rojas C. Personal communication to C. Calude, 11 September 2008.

[15]  Kaye R. Models of Peano Arithmetic (1991) Oxford: Oxford Press.

[16]  Kuera A, Slaman TA. Randomness and recursive enumerability, SIAM J. Comput (2001) 31(1):199–211.[CrossRef]

[17]  Nipkow T, Paulson LC, Wenzel M. Isabelle/HOL — A Proof Assistant for Higher-Order Logic (2002) Springer. LLNCS 2283.

[18]  Solovay RM. Personal communication to C. Calude, 23 March 2007.

[19]  Solovay RM. A version of for which ZFC can not predict a single bit. In: Finite Versus Infinite. Contributions to an Eternal Dilemma—Calude CS, Pun G, eds. (2000) London: Springer-Verlag. 323–334.

[20]  Solovay RM. Draft of a paper (or series of papers) on Chaitin's work ... done for the most part during the period of Sept.–Dec. 1974 (1975) May. New York: IBM Thomas J. Watson Research Center, Yorktown Heights. 215. unpublished manuscript.

CiteULike    Connotea    Del.icio.us    What's this?

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by Calude, C. S. Articles by Hay, N. J. Social Bookmarking          What's this?