[FOM] Queries for a constructivist

[Eray Ozkural]

Greetings,

On 10/22/05, Bill Taylor <W.Taylor at math.canterbury.ac.nz> wrote:
> A: It is meaningful to say of a mathematical proposition:
>
>    "There is a (constructive) proof of this statement but no-one has
>     yet found one."
> B: Every mathematical statement is in exactly one of these 3 states:
>
>    (c) It has been (constructively) proved;
>    (d) It has been (constructively) refuted;
>    (e) It is in neither of states (c) or (d).

I would ordinarily think that both A and B are true. First, If A is
true, I would
think that B follows from A. Leaving aside this difficulty, for A, I imagine
that there are always proofs that haven't been carried out in any
formal axiomatic system (with infinitely many theorems). Including
of course those with the inference rules of intuitionistic logic.

> Would the answers to either be different, if we had specified
> a non-intuitionist constructivist?

On the other hand, it seems that the differences in opinion among
these branches of constructivism does not make much of a
difference regarding your question. At any rate, the law of
non-contradiction is valid in intuitionistic logic. Furthermore,
A holds for reasons explained above.

This is a good site with links to web resources on constructivism:

http://www.sakharov.net/foundation_rt.html

I especially recommend having a look at the stanford entry, which
may clear up the questions about kinds of constructivism, and this
one:
Constructivism and Proof Theory - by A.S. Troelstra
http://staff.science.uva.nl/~anne/eolss.pdf

Regards,

--
Eray Ozkural (exa), PhD candidate.  Comp. Sci. Dept., Bilkent University, Ankara
http://www.cs.bilkent.edu.tr/~erayo  Malfunction: http://www.malfunct.com
Uludag Project: www.uludag.org.tr   KDE Project: http://www.kde.org