The Limits of Reason

Uncomputabiliblity and Unprovability

Berry's paradox

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.

Describe describe

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.

One of these must fail!

Strict descriptions

  • 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.

General descriptions

  • 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.

Refining using proofs

  • 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.

Chaitin's theorem

  • 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.

Consistency and Contradictions

  • 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)$.

Surprise Examination Paradox

  • 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.

Godel's second incompleteness theorem

  • 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.