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