Proof by Contradiction

So far, we have looked exclusively at proofs by construction where our goal is to construct an object, e.g., an evaluation trace that provides evidence that a proposition holds. However, in some cases, it is not feasible to construct such evidence directly. This is particularly true when we to prove that an object does not obey some property of interest. Indeed, as we’ve seen from our study of mathematical logic, reasoning about the negation of a property can be subtly tricky!

In these situations, we can employ a different proof technique, proof by contradiction, to show the proposition of interest. Proving a proposition \(P\) by contradiction proceeds as follows:

• For the sake of contradiction, assume that \(\neg P\), i.e., the negation of the goal proposition, is true.
• From this assumption, derive additional facts until we can exhibit a contradiction.
• If we are able to derive a contradiction, we know that it must be because we assumed \(\neg P\) holds. Thus, it must be the case that \(\neg P\) holds and therefore \(P\) holds instead.

Note that in terms of our natural deduction rules, this final step invokes the law of the excluded middle: either \(P\) or \(\neg P\) holds. We should that \(\neg P\) leads to a contradiction and thus does not hold. Therefore, it must be the case that \(P\) holds instead.

We saw this briefly when we reasoned about set inclusion proofs involving the empty set. However, reasoning via contradiction is pervasive throughout mathematics. A classical example of contradiction proof is showing that \(\sqrt{2}\) is irrational. Recall that the definition of a rational number.

In other words, a number is rational if it can be expressed as a fraction.

In contrast, an irrational number is precisely a number that is not rational! By “negating” the definition of rational number, we see that we must show that there is no way to decompose the number into a fraction. But that means that we have to show that every possible fractional decomposition does not work, a much harder task than exhibiting a single fractional decomposition!

Instead of this route, we can use a proof by contradiction. We will assume that \(\sqrt{2}\) is irrational and then follow our nose until we arrive at a contradiction.

The Spectrum of Formal Proof

As we end our discussion of mathematical logic, let us reflect on the nature of formality in mathematical arguments. We brought up at the beginning of the course that a hallmark of mathematical prose was its attention to mathematical rigor. We’ve seen varying degrees of mathematical rigor so far:

• In program correctness, we justified equivalences between programs by using a formal model of computation.
• In mathematical logic, we justified equivalences between propositions by the rules of natural deduction.

While our program correctness proofs appealed to a formal model of computation, we didn’t explicate and justify every step of reasoning. For example, when our programs became more interesting, we took shortcuts in evaluation such as (length l) -->* (+ 1 (length l)) and did not justify our derivation. However, implicit in our model is a collection of formal rules that we did not explicate. For example, the following rule:

----------------------------- [app]
((lambda (x) e) v) --> [v/x]e

Precisely describes function application: an applied lambda takes a step to its body e but with every occurrence of its parameter x substituted for value v. While we could have introduced and required you to cite these rules on every derivation step, it would have been too onerous to do so. But does this mean our program correctness proofs were not formal enough?

To answer this question, we need to be more clear about what we mean by “formal” and “rigorous” in mathematics. Recall that mathematical prose is composed of a collection of interrelated formal definitions and propositions. All mathematical arguments, therefore, must be based on these objects:

When that argument is meant to show that a proposition is correct, we call it a proof.

For example, consider the append-length property from our program correctness unit (finally written using appropriate first-order logic symbols!):

A non-mathematical argument might be the following:

This property is correct because I ran append on multiple test cases and observed that the property held.

While not an unreasonable argument, it is not mathematical in nature. The argument does not appeal to any particular model of how programs operate; it is a direct observation of the object “in the wild.”

A mathematical argument would be one that draws on some model of how Racket programs operate. We introduced one such model, substitutive evaluation, although there are others we could consider. In this sense, a mathematical argument is simply one that we make based off of a predictive model of the phenomena that we are studying. That model itself is, by definition, mathematical in nature since mathematics is the study of modeling. So, remember when formulating mathematical arguments to always go to definition to determine what to prove and how to proceed in your reasoning.

What ultimately varies between mathematical arguments is the amount of formality or rigor found in them.

It is tempting to think that a formal mathematical argument is one that uses a significant amount of symbols, for example, the natural deductions we have been writing. However, because the symbols are backed by formal definitions, the symbols are simply a concise way of writing out prose that immediately appeals to formal definition. For example, I can invoke the idea of universal quantification in a variety of ways in prose:

• For every animal \(x\) … .
• For all animals \(x\) … .
• For each animal \(x\) … .
• \(x\) … . (Note: implicitly universally quantified!)

But there is only one unambiguous way to write universal quantification in symbols:

• \(\forall x \ldotp \ldots\)

Since our arguments must appeal to definition, we favor using symbols to keep our prose concise, yet on-target. However, it isn’t a requirement.

So what is the difference between a formal and informal proof in practice? A completely formal proof of our append-length property would not just use our formal model of computation and a citation of every rule in our model, but also explicate every step of logical reasoning using our rules of natural deduction! In contrast, a completely informal proof of append-length would be:

Here, we’ve skipped virtually all the steps of formal reasoning, just citing that the proof proceeds by induction. Note that this proof is correct: we can prove this claim by induction on l1. It is less formal because it has left out most of the details of the argument!

What is the right level of formality in a mathematical argument? It depends on context. For example:

• If you are explaining why a code snippet you wrote is correct to a co-worker, you may appeal to how the program evaluates “on paper” (thus, invoking a model of computation implicitly) but only explain the cases that are most complex or of most concern, e.g., due to performance or security. In your description, you might talk about how “this function evaluates to this value and therefore …” without appealing to any formal rules.
• If you are trying to debug a very subtle issue in your code, you might start writing out how the program takes successive steps of evaluation in addition to your assumptions about the state of variables and how they change over time.
• If you are in a mathematics class, you might be expected to write out every step of evaluation along with every rule justifying that step as evidence that you understand the low-level mechanics behind your argument.

In all of these cases, you are making arguments, but the level of formality changes depending on need. It is imperative as a computer scientist that you learn how to navigate this spectrum of informality and formality in making mathematical arguments so that you can provide the right amount of details at the right time. In practice, you will likely be making more informal arguments both to yourself and your collaborators and coworkers. However, when things get tricky or difficult, you should be capable of making more detailed formal arguments to better convince everyone involved that you are doing the right thing.