# Are there explicit examples of "absolutely" unprovable mathematical statements?

This is a question which has been asked and answered a number of different ways online, however, in my own research, most answers have been unsatisfying and occasionally conflicting. Due to that, I hope to clarify my question as much as possible.

Typically, we discuss "provability" in terms of a particular formal system. i.e. Goodstean's theorem can not be proven in Peano arithmetic, and Gödel's incompleteness theorem says that no sufficiently powerful formal system can prove its own consistency. However, such theorems are not "absolutely" unprovable since it is typically possible to construct more powerful formal systems in which these statements can be proven.

A common response to this question is to say that no statement can be "absolutely" unprovable, since it is always possible to construct a system which treats any given statement as an axiom. However, I don't think this is an adequate notion of "proof", since, for example, if I constructed a theory which treated the twin prime conjecture as an axiom, no one would consider this to be an acceptable proof of the twin prime conjecture. Perhaps the key here is to clarify that we are working within a fixed model, and we are concerned about human-verifiable proofs within a (presumably) consistent formal system.

My first thought about this question was to define "absolutely unprovable" in terms of computability. This arxiv paper by Toby Ord (who I should say is not a mathematician or computer scientist) states that

With the help of Turing’s work on computability, formal systems can be specified as Turing machines that semi-compute a set of formulae, which are considered proven. This can be considered in the terms of classical proof procedures as a recursively enumerable set of axioms with recursively enumerable rules of inference [...]

Turing’s proof of the uncomputability of the halting function by his machines also extended Gödel’s Incompleteness Theorem. Turing (and Church) had shown an ‘absolutely’ undecidable function whose values could be proven by no consistent formal system. (ch 1.3, pg 6)

Which seems to suggest that, assuming the truth of the Church-Turing thesis, there are "absolutely unprovable" theorems. In fact, trivially, since there are an uncountable number of subsets of the integers, and, for every subset $$S\subset\mathbb{Z}$$ there are a countable number of statements expressible in Peano arithmetic about $$S$$, each of which must be true or false, there must be uncountably many theorems about the subsets of the integers, but, since there are only countably many Turing machines, there must be theorems whose proof can't be generated by any Turing machine. But, this argument doesn't really give me a way of finding any specific example of an unprovable theorem.

Ord defines a function which maps from Turing machines to the set $$\{0,1\}$$ depending on whether or not they halt. While this function has been proven to be uncomputable, meaning, there is no Turing machine which can compute this function for all inputs, I don't see how it necessarily provides an example of an absolutely unprovable theorem, since it does not imply this function can't be computed on any individual input. It could be the case that for every Turing machine $$M$$ there exists another Turing machine $$M'$$ that can be used to compute a proof that $$M$$ does/doesn't halt. If this were the case, the halting problem would still be undecidable since no program could find M' for any given M, but it would not provide an example of any unprovable theorem.

Another example of an often discussed uncomputable function is the Busy-Beaver function. I've often heard it mentioned that $$\Sigma(n)$$ is uncomputable for sufficently large values of $$n$$. If this is the case, it would seem to imply the existence of an absolutely unprovable theorem which states something like "$$\Sigma(\omega) = \sigma$$" (for some $$\omega,\sigma\in\mathbb{Z}^+$$). However, while there is no Turing machine that can compute $$\Sigma(n)$$ for all inputs, I see no reason to believe that for any given $$n$$ there isn't some Turing machine that can compute (and verify) $$\Sigma(n)$$. There is a theorem which has been mischaracterized (by some people online) as stating that values of $$\Sigma(n)$$ are uncomputable for $$n\geq 7910$$, however, this proof only shows that values of $$\Sigma(n)$$ can't be proven using ZFC for $$n\geq 7910$$. In general, all of the "unprovability" results I've seen about the Busy-Beaver function seem to be relative to some particular formal system.

What I'm interested in knowing is if there are any explicit examples of absolutely unprovable statements, that is, statements (expressible in some computable formal system) which, if they are true, no proof can be computed (i.e. generated by a Turing machine). In particular "natural" examples of such theorems would be very interesting.

• What does it mean for a proof to be generated by a Turing machine? A proof is a finite object - no more complicated than (and indeed codeable by, per Godel) a single natural number. Also, keep in mind that there are only countably many sentences in the language of arithmetic - most sets of natural numbers aren't definable in the language of arithmetic, and so we can't even talk about them. (And the language of arithmetic isn't special here - any at-most-countable language has the same deal.) Finally, remember that every sentence is a theorem of the system with only it as an axiom. Aug 1, 2019 at 2:45
• Do you assume a particular logic theory (PA or ZFC or ZFC+twin prime) is consistent ? If PA is consistent (for a fixed n) iff buserbeaver(n) > N then PA + buserbeaver(n) > N is consistent, if it is not consistent there is an algorithm proving it in a finite amount of time, when assuming PA is consistent you are assuming the program searching for a contradiction will never halt. Aug 1, 2019 at 2:46
• @Noah When I talk about generating a proof, I'm referring to the paper by Toby Ord, in which he claims that a deductive formal proof can be thought of as a type of computation.
– ZKG
Aug 1, 2019 at 2:51
• @reuns You make a very good point about consistency that I had not considered, consider posting that as an answer.
– ZKG
Aug 1, 2019 at 2:54

In general, all of the "unprovability" results I've seen about the Busy-Beaver function seem to be relative to some particular formal system.

All unprovability results whatsoever are relative to some particular formal system: every sentence $$\varphi$$ is a theorem of the axiom system $$\{\varphi\}$$, after all! So if we interpret the term as strongly as you do per

such theorems are not "absolutely" unprovable since it is typically possible to construct more powerful formal systems in which these statements can be proven,

then there are simply no absolutely undecidable sentences at all. The best results we can hope for are principles of the form "For every theory of such-and-such type, only a small number of the sentences in this particularly simple set of sentences $$\Gamma$$ is decidable" - the Busy Beaver function provides such an example (every consistent recursively axiomatizable theory extending PA decides only finitely many of its values).

Incidentally, here's a bit of very annoying context: the phrase "absolutely undecidable" is used by some logicians, but in a more complicated (and highly informal) way. An absolutely undecidable sentence is one which, in some sense, we'll never find "intuitively compelling" - on par with those for the ZFC axioms, say - arguments for or against. (Personally I have a strong distaste for this term.)