Re: Constructive Math query.


Bill Taylor wrote:
|It is a trivial theorem of orthodox math that
| "any sequence which is a permutation of the harmonic sequence,
| tends to zero".
|
|Is this still provable in constructive math? The proof seems
|to require looking at unbounded distances down the sequence,
|so I'm not sure.

It might be a useful exercise to look at a classical proof and
try to figure out which step it is that seems like it might be
nonconstructive.

The index set is N^{+} = {n : n>0}.

A function f:N^{+}->N^{+} is a permutation if it's a one-to-one
correspondence, meaning that for each n>0, there exists a unique
m>0 such that f(m)=n. The permuted series is 1/f(n).

Suppose we have an epsilon>0. By Eudoxus' principle, which is
constructive, epsilon>1/k for some integer k>0. If n>k, then
1/n<epsilon. What does it take to guarantee that 1/f(n)<epsilon?
At least it suffices that f(n)>k.

So, is there an M sufficiently large that if n>M, then f(n)>k?
How do you usually prove that there is? Consider what the
exceptions are, namely those n for which f(n)=1,...,k. Since
f is one-to-one, these are just n = f^{-1}(1),f^{-1}(2),...,
f^{-1}(k). There are finitely many, so there's an upper bound
M, and if n>M then f(n) is a positive integer other than
1,...,k, hence f(n)>k and 1/f(n)<epsilon.

What seems like it might be nonconstructive? It is all
constructive, but you still might want to try to figure out
what seemed like it might not be.

Keith Ramsay

.

Relevant Pages