Constructive Proofs in Mathematics

Hello! Welcome to your next lesson in our journey through the foundations of mathematics.

In our last lesson, we analyzed the deep philosophical differences between classical and intuitionistic logic. We saw that the intuitionist's rejection of the Law of the Excluded Middle isn't just a technicality; it stems from an anti-realist philosophy that equates truth with constructive provability. This led us to the distinction between non-constructive proofs, which merely show existence, and constructive proofs, which must provide a method for finding the object in question.

Today, we will move from theory to practice. Your learning outcome for this lesson is to apply constructive reasoning to a simple mathematical proof. We'll see how the philosophical principles we discussed translate into a specific style of mathematical argumentation, one that you'll find is closely related to the design of algorithms.

1. What Makes a Proof "Constructive"?

At its core, constructive reasoning demands that proofs of existence be effective.

• To prove a statement of the form "There exists an $x$ such that $P(x)$ is true," a constructive proof must exhibit a specific example of such an $x$ or provide a method for finding one.
• To prove a statement of the form "$A$ or $B$," a constructive proof must either prove $A$ or prove $B$.

This is a direct departure from classical logic, where you can prove existence by contradiction (showing that non-existence is impossible) or prove a disjunction using the Law of the Excluded Middle without committing to either disjunct.

The key idea is that a constructive proof contains more information than a classical one. It doesn't just convince you that something is true; it shows you how it's true by providing a concrete witness. This "witness" is often the result of an algorithm.

The video below explains this "constructive" demand in the context of disjunctions, which follows the same principle as existence claims.

2. An Example: From a Non-Constructive to a Constructive Proof

Let's see this distinction play out in a core result from number theory. You know that for any two positive integers $a$ and $b$, their greatest common divisor (GCD) can be expressed as a linear combination of them, i.e., $d=ax+by$ for some integers $x$ and $y$.

A classical proof can establish the existence of $x$ and $y$ non-constructively. The following paper provides an excellent, rigorous treatment of this topic suitable for your background.

The classical proof you just read is elegant, but from a constructive viewpoint, it's unsatisfying. It defines a set B = {au + bv | u, v ∈ ℤ and au + bv > 0} and then asserts that because B is a non-empty set of positive integers, it must have a smallest element, d. This relies on the Well-Ordering Principle. While classically valid, this step gives us no procedure for finding d, nor the corresponding x and y. It proves that x and y exist without constructing them.

3. The Algorithm as Proof: Euclid's Method

How would we make this proof constructive? We need an explicit procedure—an algorithm—that takes a and b as input and produces d, x, and y as output. As Avigad's paper notes, this procedure is precisely the Euclidean algorithm.

A constructive proof is not just the algorithm itself, but also the arguments that prove the algorithm works as intended. This includes:

1. A proof that the algorithm always terminates.
2. A proof that upon termination, it produces the correct output.

The following lecture explains this beautifully, framing Euclid's algorithm as a paradigm of constructive mathematics.

The proof of termination in the video is constructive because it relies on the property of a strictly decreasing sequence of natural numbers, which must eventually reach zero in a finite number of steps. The proof of correctness is constructive because it demonstrates step-by-step how the property of being the GCD is maintained through each iteration of the algorithm.

4. Your Turn: Applying Constructive Reasoning

Now it's time to apply these concepts yourself. The learning outcome is not just to understand but to apply.

Exercise 1: Re-interpreting a Classical Proof

Euclid's proof of the infinitude of primes is often presented as a proof by contradiction, which can have a non-constructive flavor. However, as Avigad's paper mentions, it contains the kernel of an algorithm.

Your task:
Read the two proofs of Theorem 2.2 ("There are infinitely many prime numbers") in Section 2 of Avigad's paper (LINK).

1. Describe the algorithm implicit in the second, re-worded proof for finding a prime number larger than a given number M.
2. Is this a good algorithm? (Think about computational efficiency).

Exercise 2: A Concrete Application

Let's use the constructive method we studied to solve a concrete problem.

Your task:
Let a = 288 and b = 168 (one of the examples from the Oxford video).

1. Use the Euclidean algorithm to find the greatest common divisor, d.
2. Now, perform the more advanced constructive task: find integers x and y such that 288x + 168y = d. To do this, work backward through the steps of your algorithm, substituting the expression for the remainder from each previous line.

Conclusion

In this lesson, we bridged the gap between the philosophy of intuitionism and the practice of constructive mathematics. You have seen that applying constructive reasoning means thinking algorithmically—insisting that a proof not only demonstrates existence but provides a clear recipe for construction.

Here are the key takeaways:

• A constructive proof of existence must provide a method for finding the object whose existence it asserts.
• This principle is embodied in procedures like the Euclidean algorithm, which serves as a proof that is also a computation.
• A complete constructive proof includes not just the algorithm, but also constructive arguments for its termination and correctness.
• We can often re-read classical proofs to extract their implicit constructive content, turning them into explicit algorithms.

Preview of the Next Lesson:
We have now examined three competing foundational programs: Logicism, Formalism, and Intuitionism, focusing on their logical and philosophical underpinnings. We are now prepared to move into the second module on mathematical foundations, which deals with the framework that ultimately became dominant in modern mathematics. In our next lesson, we will begin this by exploring the world of set theory. The learning outcome will be to describe the iterative conception of the set-theoretic universe underlying ZFC. We will be shifting our focus from the rules of reasoning to the fundamental objects that mathematicians reason about.