Are there still mathematicians who don't accept proof by contradiction?

Solution 1:

Constructive mathematics is alive and well, including at MSE; see e.g., tags constructive-mathematics and intuitionistic-logic. 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.

Solution 2:

"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.