Why are direct proofs often considered better than indirect proofs?

I just did a quick lookup and it suggested that the two flavors of indirect proof was contraposition and contradiction. What I'm about to say is criticizing contradiction, because contraposition seems fine to me.

Imagine you have a 1000 statement direct proof. Then every step along that way is provable. Maybe somebody reads your proof and realizes that an observation you made halfway through is exactly the idea they need to solve a problem they have. Mathematical history has many examples of lemmas that are more famous than the theorems they originally supported.

By contrast, a 1000 statement proof by contradiction starts out with two hypotheses that are inconsistent. Everything you're building is a logical house of cards that is intended to collapse at the end. Nothing you wrote can be counted on outside that framework without a separate analysis.

If it truly takes both hypotheses to get you to the result, then so be it. But I was rightfully dinged by my professors when I wrote a proof by contradiction that could easily be modified into a direct proof by contraposition.


A direct proof often provides more information: if, for example, you want to show that there exists a number with some property, then a direct proof is much more likely than an indirect proof to tell you what that number actually is. This is also true for more complicated statements: if you want to prove "For all $x$ there is some $y$ such that [stuff]," you probably also want to know a particular function spitting out such a $y$ for each given $x$. Again, a direct proof is much more likely to provide that information to you.


This idea really shines when we take it further, and look at logical systems which don't even allow indirect proof; I'm thinking in particular of intuitionism, but there are others.

Most obviously, the above point yields an "applied" motivation for such logics, since it turns out that we can often prove that a proof in such a system (of an appropriate statement) immediately gives us explicit bounds/functions/etc. for that statement. Relevant terms here include "proof mining" (or "unwinding") and "term extraction."

At a vastly higher level of abstraction and technicality, arguments in weaker logics are applicable in broader contexts. Now if you're not interested in nonclassical logic a priori, that doesn't seem like much of a motivation at first, but it turns out that nonclassical logics show up in classical mathematics - via the internal logic of categories. This logic is generally intuitionistic. For an example of how this can translate to a result in the "real world" with classical logic, see this old MSE post. This is quite technical, but here's the gist:

  • We want to prove a fact about modules over sheaves.

  • If we work within an appropriate topos, these look like bog-standard modules over a ring, and the fact we want is classically true for actual modules over actual rings.

  • So all we need is to show that that fact translates to the internal logic: the topos in question will then also think the same thing about its "modules," which are actually the more general objects we care about.

  • This ultimately means that we can produce a classical proof about a generalization of a certain object by finding an intuitionistically-valid proof about the more specific kind of object.


This is rooted in the fact that "true" and "provable from a certain set of axioms with a legit sequence of deductions" can be different things, and in most cases a direct proof can be easier to generalize than an indirect proof. A couple of examples might be useful in explaining this.


Theorem. If the elements of $\mathbb{N}$ are colored with $c$ colors, there are infinite monochromatic 3-APs (arithmetic progressions with $3$ terms).

Sketch of indirect proof: we may invoke the https://en.wikipedia.org/wiki/Poincaré_recurrence_theorem and the principle of combinatorial compactness, by putting a tolopogy over the space of ultrafilters.

Sketch of direct proof: we may study the discrete Fourier series of the set of integers with some color. It turns out that if a coefficient is large enough, there is no way to avoid monochromatic $3$-APs. If that is not the case, we are able to achieve an increase in density by intersecting our set with an infinite AP. By dichotomy, a finite number of steps (only depending on $c$) is able to locate a monochromatic $3$-AP, and prove it appears before $\exp(\exp(\exp c)))$ or something like that.

The indirect case might be considered more elegant, but the direct proof provides an extra quantitative information.


Theorem. Any continuous map $f$ from the unit disk to itself has a fixed point.

Sketch of indirect proof: the existence of a continuous map from $D^2$ to $D^2$ without fixed points would give a retraction of $D^2$ over $S^1$, which does not exist due to the fact that $\pi_1(D^2)$ is trivial while $\pi_1(S^1)=\mathbb{Z}$.

Sketch of direct proof: $D^2$ can be continuously deformed into a triangle $T$, and we may consider a triangulation of $T$ with mesh $\varepsilon$. We may assign a color to each vertex of the triangulation according to the value of our function at such point, and check that the hypothesis of Sperner's lemma are fulfilled. The full-colored Sperner's triangles associated to the meshes $\frac{\varepsilon}{2},\frac{\varepsilon}{4},\frac{\varepsilon}{8},\frac{\varepsilon}{16},\ldots$ accumulate towards a fixed point for $f$.

The (combinatorial) direct proof not only proves a fixed point exists, it provides an algorithm for locating it.