https://lawrencecpaulson.github.io/2022/04/20/Why-constructive.html

[utterances-bot]

Why are you being constructive?

https://lawrencecpaulson.github.io/2022/04/20/Why-constructive.html

[Kakadu]

Goldbach’s conjecture, ¬(∃n∈ℕ.n>2∧ n is not the sum of two primes)

In Goldbach conjecture you wrote that n is greater than 2, but it should be n is even.

[lawrencecpaulson]

Well spotted, thanks! Now fixed.

[jdhamkins]

Despite what you suggest, the standard Cantor proof of the existence of transcendental numbers is constructive. Cantor provided an enumeration of the algebraic numbers, and his diagonalization method provides a construction of a real number not on that list. Thus, we construct a specific transcendental number. This aspect of his proof was historically important in regard to his dispute with Kronecker.

[jdhamkins]

But basically I am well on your side in this dispute, and wanted only to point out that minor issue. Meanwhile, there are many other examples of non-constructive existence proofs in mathematics. One example concerns Turing's account of computable real numbers as those for which we have a computable algorithm to enumerate the digits. (This is not quite the same as the usual notion in computable analysis, where a computable number is one for which we can compute rational aproximations within any desired precision.) With Turing's definition, it is nonconstructive to prove that the sum of two computable numbers is computable (since you need to split on cases depending on whether there are infinitely many carries or not). But in classical logic, it is provable.

[lawrencecpaulson]

You're right. In this case I won't try to correct the post, however. There are still several genuine non-constructive proofs mentioned there (König's lemma, above all).

[UlrikBuchholtz]

It's in Brouwerian mathematics that all total functions on the reals are continuous. Bishop was very careful to make his work compatible with classical mathematics, so there you instead assume a modulus of uniform continuity (or whatever) whenever it's needed.

I agree with you that the main benefits of constructive mathematics are that it can be internalized in different settings, such as synthetic computability theory (which you mentioned), synthetic measure theory, synthetic topology, synthetic differential geometry, etc., by interpretations in various toposes.

From a proof-assistant standpoint, this means that to get the full benefit, we need to be able to perform these proof interpretations within the system, which is not well-supported at the moment. (The way constructive mathematicians currently use proof assistants is in a more limited way, by checking the constructive mathematics itself, but then we don't reap the full rewards.)

[lawrencecpaulson]

How about a link? Andrej Bauer mentioned CoRN, a Coq library of constructive analysis:

https://github.com/coq-community/corn https://corn.cs.ru.nl/