Newsgroups: sci.math
From: hoey@ai.etl.army.mil (Dan Hoey)
Date: 11 Aug 89 18:30:40 GMT
Subject: Re: proof by contradiction

Avoidance of proof by contradiction is one of the hallmarks of
Constructivist mathematics, a logical discipline associated with
L. E. J. Brouwer.  This school accepts only those mathematical objects
that can be constructed in some finite way from primitive objects.
The school is not widely accepted in its strict form, as an
epistemological gauge of what is proven and what isn't.  However, I
have heard of some work that attempts to convert a constructive proof
into a computer program for calculating the constructed object.  If
nothing else, a proof that uses contradiction bars the use of such
tools.

I'm sorry to be so vague on the subject, but all I know comes from a
talk I heard eight years ago.  I think the research was going on at
Cornell or Princeton, in case that helps.

Dan Hoey