# The Limits of Reason

#### Uncomputabiliblity and Unprovability

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

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

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

### Unprovability

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

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

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