Abstract:
We prove that every computably enumerable (c.e.) random real is provable in
Peano Arithmetic (PA) to be c.e. random, a statement communicated to one author
by B. Solovay. 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.
The result that every c.e. random real is provably c.e. random is in contrast with
the case of computable functions, where not every computable function is provably
computable. It is even more interesting to compare this result with the fact that – in general – random finite strings are not provably random.
The paper also includes a sharper form of the Kraft-Chaitin Theorem, as well as an
automatic proof of this theorem written with the interactive theorem prover Isabelle.
