Re: Constructive Math query.


Keith Ramsay wrote:
> david petry wrote:
> |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.

> |Of course, you must be talking about permutations which can
> |be constructively proven to be permutations. Then, the answer
> |is "yes".

> There's no need to add an assumption that the permutation has
> been proven to be a permutation. Just the fact that it is one
> is sufficient.

Yes, but "the fact that it is one" can only be established by proof.

> This may seem like a picky point, [...]

I would be surprised if Bill Taylor thinks your point clarifies
anything.
But I could be wrong.

.

Relevant Pages