Re: Constructive Math query.

Bill Taylor says...

>*IF* one's brand of constructivism is of the hard-nosed type
>that conflates truth with provability, (which seems to have
>been widespread in the past, recall my excerpt from Bishop),
>then I would have said it must be so.

I didn't think that constructivism conflates truth and provability.
I missed your quote from Bishop, but Bishop's constructivism
is *conservative* over classical logic; anything that's constructively
provable is also classically provable. The claim that

A is provable <-> A

is certainly not true classically. Of course, you can
take a faith-based approach to believe that if something
is true *eventually* a proof will be found...

>> Take an example in which A is neither provable nor refutable.
>> The interpretation "If we can prove A, then B" becomes vacuously
>> true, in that case, but "If A then B" isn't vacuously true.
>
>Well I would have thought that to a constructivist
>(of this hard-nosed type) it WAS vacuously true.

As I said, I don't think that's true. Constructive logic
doesn't prove anything that isn't also true classically.

I have another objection to the equivalence: If A and B
are statements in the language of arithmetic, then

"If A then B"

is a statement about *natural numbers*. In contrast,

"If we have a proof of A, then B"

is a statement about *proofs*. They certainly don't *mean* the
same thing, even if they are both provably equivalent.

>Such a type would surely regard the "If A" part of your conditional
>as equivalent to "If we can prove A" which he would deem false,
>by noting the undecidability of A. So he would take your
>conditional as vacuously true also. I see now that he would
>also be required to admit that both A was false and ~A was false.
>This would presumably not trouble him as asserting ~~A would
>not require him to assert A.

If ~A and ~~A are both provable, that's as much of a contradiction
as A and ~A.

>Obviously I'm missing something trivial, but I doubt I'll ever
>get it, I just can't seem to cotton to this phislosophical
>constructivism, (as opposed to the strictly formal approach
>of Bridges for example).

Well, the way that makes the most sense to me is to
think of propositions as corresponding to types (in the
sense of computer science), and to think of a proof
of a proposition as elements of that type. So for instance,
the type of "A or B" is the disjoint union of the type
of A and the type of B. The type of "A implies B" is the
type of functions from the type of A to the type of B.
The type of a falsehood is the empty type.

The philosophical issue, then, is this: Do there
exist elements of a type *other* than those that are
constructively proved to exist?

On this question, I think of constructivists as *agnostic*
rather than *atheist*. To take the atheistic position that
nothing exists other than things that are constructively
proved to exist seems contradictory in a way: There is
no *proof* that only constructive objects exist, and
a constructivist should never assume the truth of something
without proof.

Taking the agnostic position allows constructive logic
to be applied even in a nonconstructive domain such as
set theory. You can work out what are the constructive
*consequences* of nonconstructive *axioms*. In the
type-theoretic interpretation, axioms correspond to
types containing elements that are not necessarily
constructively definable.

--
Daryl McCullough
Ithaca, NY



.