# Chaitin's constant and coding undecidable propositions in a number

Chaitin's constant $\Omega$ is a constant whose digits are defined to encode the solution to the halting problem which is undecidable and hence $\Omega$ is uncomputable. I am not particularly familiar with the field of algorithmic information theory, and I have a question about a statement which I once read (by a physicist) in a paper by David Deutsch:

If the dynamics of some physical system did depend on a function not in $C(T)$ [the set of computable functions], then that system could in principle be used to compute the function. Chaitin (1977) has shown how the truth values of all ‘interesting’ non-Turing decidable propositions of a given formal system might be tabulated very efficiently in the first few significant digits of a single physical constant [Emphasis mine].

I have read the paper referenced, and I think I understand (a fair bit of) it, but I still do not understand exactly where the italicized statement comes from; I could not seem to find relevant results in the paper. Would anybody be able to explain exactly where the statement that all of a formal system's ‘interesting’ undecidable propositions can be efficiently tabulated in a real number's first few significant digits comes from, how such tabulation would proceed, and what (if any) is the relation of this to $\Omega$ and Chaitin's work?

• Haven't followed your links so I don't know if they are taking the same approach, but I think the idea is to follow Chaitin's construction but instead of a prefix-free coding of Turing machines use a prefix-free coding of a first-order theory, and instead of counting halting programs, count provable formulas, weighting them with the same $2^{-\vert x \vert}$. Then the resulting real number can be interpreted as a "provability probability" and the first $n$ bits of it can be used to decide the provability of the first $2^n$ formulas (assuming language is binary). – Dan Brumleve Jan 26 '17 at 0:12
• @DanBrumleve I see, so Deutsch's statement would then be taken to mean that we simply take a small (why?) number of undecidable propositions to be 'interesting' and require $\log(n)$ bits to encode the result? – Anon Jan 26 '17 at 0:16
• @DanBrumleve Wait, but would the first $n$ bits really give us the first $2^n$ formulae? Each digit has $1$ bit of information which should (?) only let us decide one formula? I thought the bijection between formulae (or Turing machines in the case of $\Omega$) and digits was no better than one-to-one? Have I misunderstood what's going on with $\Omega$ the whole time? – Anon Jan 26 '17 at 0:20
• A time-space trade-off is a way to look at it maybe? We start by knowing how many n-bit programs halt (formulas can be proved), this information uses about $\log{n}$ bits. Then we run them all in parallel (start proving every theorem starting from the axioms) until exactly that many of them halt (exactly that many formulas shorter than $n$ have been proven). Now we know exactly which ones that are shorter than $n$ are halting programs (are provable) and which ones aren't. – Dan Brumleve Jan 26 '17 at 3:17
• ... should have said "this information uses about $n$ bits" not $\log n$ – Dan Brumleve Jan 26 '17 at 3:29

In a prefix-free coding of first-order arithmetic, instead of writing $\exists\ y\ .\ y*y=x$, we would write something like $\exists\ y\ .\ = * \ y \ y \ x$. It's also convenient to think about a prefix-free binary language, so assign a binary word to every symbol, for example $\exists \rightarrow 0000$, $x \rightarrow 0001$, etc. in either a fixed-width or prefix-free way so that the symbol boundaries can be decoded.

Now let $L$ be such a binary prefix-free language encoding the formulas of arithmetic and define $\Omega = \sum_{x \in L : \text{Pr}(x)}{2^{-\vert x \vert}}$ where $\text{Pr}$ is the provability predicate for $L$. $\Omega$ is the probability that an infinite random bit string starts with a theorem.

Given the first $n$ bits of $\Omega$, $\Omega_n = \lfloor \Omega \cdot 2^n \rfloor \cdot 2^{-n}$, we can decide $\text{Pr}(x)$ for any formula $x$ with $\vert x \vert \le n$. What we do is begin a process of proving all theorems of arithmetic starting with the axioms, keeping track of the total contribution to $\Omega$ from every theorem proved so far. When that value becomes greater than or equal to $\Omega_n$, which it must eventually, all theorems not longer than $n$ bits have been proved. At that point we can determine $\text{Pr}(x)$ for any formula $n$ bits or shorter.

It's fun to imagine $\Omega$ appearing as a dimensionless physical constant measurable to thousands of digits, or perhaps engraved on a monolith buried on the moon alongside the axioms of ZFC. I think it is certainly a paradox that mathematical truth is so "compressible". One way out is to say that there's no way we can really know that the $n$-bit string written on the monolith really is $\Omega_n$ (supposing even that there is other writing that claims it is equal to $\Omega$, that it was created by the gods, etc.). There is also the point that it's probably computationally infeasible to wait until all short theorems are proved, so it would be useless. One thing we might get out of it is a situation like where there are $5$ open problems (formulas that are not known to be theorems and not known not to be) expressible in $n$ bits; after choosing to believe in a particular $\Omega_n$, we might then "know" that exactly $3$ of them are provable, and $2$ are not, but that by itself might get us no closer to discovering which are which.

• Fantastic answer! I would +2 if I could, but I've hit the daily vote limit (MSE does that to you...) so I'll upvote later. – Anon Jan 26 '17 at 5:20
• This is exactly what I was asking; I guess by 'interesting' Deutsch meant the theorems that have short statements. The fact that he specifically mentioned them being Turing-undecidable propositions makes me wonder though: in a particular $L$ all of the short theorems might be Turing decidable mightn't they, since Turing decidability and $L$-provability aren't the same thing? Would it be possible to have an $L$ in which all of the short theorems were Turing undecidable, thus bearing out Deutsch's statement, or have I misunderstood something? – Anon Jan 26 '17 at 5:20
• He is abusing the term "decidable" a bit since it is not a formula itself that is decidable or not, rather it applies to a proposition with an argument like our provability predicate. – Dan Brumleve Jan 26 '17 at 5:25
• By the way, I love the idea of the monolith. Deutsch's response in the paper to what you have said about being unable to know that it is $\Omega_n$ is interesting: "Nor, conversely, is it obvious a priori that any of the familiar recursive functions is in physical reality computable. The reason why we find it possible to construct, say, electronic calculators, and indeed why we can perform mental arithmetic, cannot be found in mathematics or logic. ... – Anon Jan 26 '17 at 5:29
• Despite what I said "decideable" can refer to a formula, meaning that it or its negation is provable. But I don't think that's what he means here, because if a short formula is undecidable (has no proof or disproof), the construction will tell us that fact, but it won't tell us its "truth value". What I think he means is something like "truth values of all 'interesting' propositions of a given formal system (a non-Turing decidable problem)". – Dan Brumleve Jan 26 '17 at 5:44