[TYPES] non-constuctive proofs

[oleg@okmij.org]

Thorsten Altenkirch posed a problem of rationality of log_2 9. There
are actually two problems: proving that log_2 9 is not rational, and
proving that log_2 9 is irrational. They are different problem in
intuitionistic logic, and the second is much harder. Incidentally, the
high-school proofs about sqrt(2) only proved that sqrt(2) is not
rational. If we use classical logic (as most theorem provers did in
Freek's benchmark), we may conclude the number is irrational. We may
not intuitionistically conclude so.

Let us first solve the first problem, the negation of rationality of
log_2 9. Let us use weak reductio, which is intuitionistically
justified. Let us assume log_2 9 is rational, that is, p/q, where p
and q are two positive integers. 
    log_2 9 = p/q
    q*log_2 9 = p
    log_2 (9^q) = p
    9^q = 2^p
which can only happen if both p and q are 0. Otherwise, the two sides
have no common factor other than 1. QED.

To prove irrationality of log_2 9 intuitionistically, we should prove
that we can construct a sequence of intervals over Q (rational
numbers) whose length is decreasing and which contain log_2 9. In other
words, we should be able to bracket log_2 9 by two rational numbers
given any rational eps. We appeal, as in the case for sqrt(2), to the
Newton method (or golden ration method or any other suitable method of
root finding).