The Limits of Reason

The smallest number that cannot be described in less than a 1000 words.

Let us call this Berry's number.

Paradox: The above is a description of Berry's number in less than 1000 words.

For Berry's paradox to give a contradiction, we need

A notion of descriptions, say as terms of a fixed type.
To know which descriptions are well-defined (e.g. terminate), so correspond to terms.
To know which term is represented by a given description.
Berry's statement must give a well-defined description.

Suppose we have a strict language, where all descriptions are total and terminating.
Suppose also that our language is rich enough so that descriptions are terms, as is the function evaluating a (valid) description.
For example, we can consider only primitive recursive definitions, while allowing dependent functions and inductive types.
In this case Berry's statement will not be considered to be a valid description.

Suppose we allow all recursive descriptions, as well as dependent types etc.
In general descriptions may not terminate.
Can be described should be interpreted as having a terminating description.
Berry's statement will be a valid description, if we can determine which descriptions terminate.
Thus the Boolean function saying which descriptions terminate is not computable.

We consider below only descriptions of numbers.
We can exclude descriptions which we can prove do not terminate.
With propositions as types, we can enumerate proofs and filter out descriptions that we can prove do not terminate.

By a diagonal ordering, for short descriptions we can
- enumerate terminating short descriptions of numbers, and give the numbers to which they correspond.
- enumerate descriptions that we can prove do not terminate.
We can thus describe Berry's number unless there is some description which does not terminate, but we cannot prove that it does not terminate.

For $M$ large enough, we cannot prove a statement $P_M(n)$ saying we cannot describe $n$ in less than $M$ tokens.
Otherwise we list proofs till we find one of the form $P_M(n)$.
For the first such proof of $P_M(n)$ we return $n$.
This gives a description of length bounded by $C + log(M)$; the description has $M$ as part of it but not $n$.
By a counting argument, some statement of the form $P_M(n)$ must be true, in fact at least one of a finite collection of such statements must be true.

We consider axiom systems given by a dependently typed language and a finite collection of postulates.
Such a system is inconsistent if there is a term of type $\mathbb{0}$.
In an inconsistent theorem, we can prove everything.
Chaitin's theorem actually says that if we can prove a statement $P_M(n)$ (with $M$ large) then our system is inconsistent.
Note that if a system is inconsistent, we can prove $P_M(n)$.

We have a finite collection of statements such that:
- At least one of the statements is true.
- Any false statement can be proved to be false.
Suppose only one of the statements was true.
Then, Chaitin's theorem, together with proving false statements are false gives a proof that this statement is true.
Thus, if we could prove our axiom system to be consistent, we can prove that there are at least two true statements.

Suppose we had a consistent axiom system.
If we can prove this is consistent, then we can prove that at least two of the statements $P_M(n)$ are true.
If exactly two were true, then using this and proving the false statements to be false, we can prove that these statements are true.
Iterating this argument gives an impossible situation.
We conclude that if a given axiom system is consistent, we cannot prove that it is consistent.