10
$\begingroup$

When I was a kid, I read popular scientific texts about the different philosophies of mathematics; formalism, intuitionism, constructivism and many others.

I learned that there existed mathematicians who did not accept proofs by contradiction and some others who did not consider proof of existence of solutions important, but required proof of how to actually construct solutions. Are such stances still common among mathematicians?

$\endgroup$
12
  • 1
    $\begingroup$ Someone once made the (specious?) point to me that every proof can be made into a proof by contradiction by starting it off with the phrase "Suppose not." $\endgroup$ – peter a g May 23 '18 at 18:51
  • 4
    $\begingroup$ @Jean-ClaudeArbaut I agree with you, but it should be mentioned that this often doesn't come from an aversion to proof by contradiction, but rather from the fact that constructive proofs often yield more information $\endgroup$ – leibnewtz May 23 '18 at 18:57
  • 1
    $\begingroup$ In discussing intuitionistic logic, a useful distinction is between $\lnot P, \Gamma \vdash Q \wedge \lnot Q$ implies $\Gamma \vdash P$ on the one hand, and $P, \Gamma \vdash Q \wedge \lnot Q$ implies $\Gamma \vdash \lnot P$ on the other hand. In intuitionistic logic, the first is rejected, whereas the second is accepted as valid. I think I've seen the distinction be stated as: the first is referred to as "proof by contradiction" and the second is referred to as "reductio ad absurdum". $\endgroup$ – Daniel Schepler May 23 '18 at 18:59
  • 1
    $\begingroup$ It can also be practically useful to determine what can be proven using intuitionistic logic only, since the internal logic of a topos (and hence the internal logic of a category of sheaves, extensively used in modern algebraic geometry) often does not satisfy the excluded middle, but does still satisfy all the axioms of intuitionistic logic, and therefore also all the theorems of IL. $\endgroup$ – Daniel Schepler May 23 '18 at 19:03
  • 1
    $\begingroup$ In fact I prefer non-constructive proof as they usually teach me more (as a mathematician). Non-constructive proofs usually require some new ideas or tricks while constructive proof usually present one idea. $\endgroup$ – Yanko May 23 '18 at 19:04
6
$\begingroup$

Constructive mathematics is alive and well, including at MSE; see e.g., tags and . Some of the most active authors in this area are Douglas Bridges and Fred Richman, who authored a combined total of over 300 publications between them. One should also mention Michael Beeson and others.

One of the most recent articles in this area is

Beeson, Michael. Brouwer and Euclid. Indag. Math. (N.S.) 29 (2018), no. 1, 483–533.

I believe this is supposed to be a constructive re-writing of Euclid.

$\endgroup$
2
3
$\begingroup$

"Proof by contradiction" is just one of several differences between constructive mathematics and ordinary "classical" mathematics - for example intuitionistic mathematics is a constructive mathematics that includes proof by contradiction, but not the law of the excluded middle. Reading generously, I think the question is about constructive mathematics more generally, not really about proof by contradiction.

While there may be a small number of active mathematicians who actively "reject" nonconstructive proofs, it would be a small number indeed. Part of the trouble, of course, is to decide what "reject" means - does it mean they simply prefer not to use it, or that they refuse to read any mathematics that does use it? It seems to me that many mathematicians have a preference for constructive proofs when they can be found, but are willing to believe nonconstructive proofs as an alternative.

However, there is a great deal of contemporary interest in constructive mathematics by mathematicians who do accept nonconstructive proofs.

  • One motivation is that systems of constructive logic are closely related to computability, through a phenomenon known as the Curry-Howard correspondence.

  • Another motivation is that some foundational systems of current interest, such as topos theory within category theory, have internal logics that are usually constructive rather than classical.

  • A third motivation comes from the program of proof mining, in which explicit bounds can sometimes be extracted from seemingly nonconstructive proofs by recasting those proofs in systems of formal logic and then applying methods of proof theory.

These sorts of applications seem to be the most common application of constructive mathematics today - not as a belief system, but as a tool that naturally arises in particular contexts and yields interesting mathematical results.

$\endgroup$
1
  • 1
    $\begingroup$ An example for your second bullet point would be Synthetic Differential Geometry, which works with a model of the real line including nilsquare infinitesimals. The whole theory completely collapses under classical logic. Bell's A Primer of Infinitesimal Analysis describes this in (IIRC) the first few pages. $\endgroup$ – helveticat Jul 10 '18 at 14:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.