Reading proofs

Introduction

In software, one of the most reliable ways to improve your own coding ability is to read code written by others.

If the author’s coding ability surpasses your own, it’s likely you’ll recontextualize ideas you take for granted, absorb new paradigms that shape how you think, and learn the idioms of your peers and the broader community.

Alternatively, if you are further along in your journey than the author, particularly when offering feedback, you will be pushed to develop a strong command of the ideas you wish to share. Your understanding must be deep enough that you can explain your thoughts simply and clearly. In either case, iron sharpens iron.

I believe the same can be said about writing mathematical proofs. In this post, we’ll take a look at two different proofs. One is from a fellow learner in an online group. The other is from the mathematician Bert Mendelson, whose topology book I have frequently cited in previous posts.

A peer’s proof

The problem

Suppose $A \setminus B \subseteq C \cap D$ and $x \in A$. Prove that if $x \notin D$, then $x \in B$.

Peer’s solution

Suppose $x \notin D$. Because $A \setminus B \subseteq C \cap D$, if $y \in A \setminus B$, then $y \in C \cap D$. Then if $y \notin C \cap D$, $y \notin A \setminus B$. Since $x \notin D$, $x \notin C \cap D$, therefore $x \notin A \setminus B$. We know $A = (A \setminus B) \cup (A \cap B)$, $x \in A$, and $x \notin A \setminus B$, therefore $x \in A \cap B$ and $x \in B$.

Commentary

First, we note that the proof is logically sound. Additionally, it makes good use of the contrapositive of a known statement: the core of the proof is exactly right. However, I believe there are small adjustments we can make to cut away what is extraneous and better showcase the logic that drives the proof.

Notice that two variables are introduced where one would do. $x \notin D$ appears, and then there’s very general reasoning about an arbitrary $y \in A \setminus B$, where that reasoning is then later applied to $x$. However, we’re free to simply reason about $x$ the whole time. Doing so unburdens the mind, even if slightly. It saves one from having to map information about $y$ back over to $x$.

Next, “We know $A = (A \setminus B) \cup (A \cap B)$ …” is more verbose and indirect than what’s needed. The rest of the sentence aggregates together already established chunks of reasoning to justify the conclusion. Since those justifications are already “in scope,” they need not be repeated. Cutting them streamlines the proof and makes it easier to understand.

An alternative

To address some of the above critiques, we could structure the proof as follows.

Suppose $x \notin D$. Then $x \notin C \cap D$, hence $x \notin A \setminus B$. Since $x \in A$, it follows that $x \in B$.

Instead of ”hence $x \notin A \setminus B$,” we could explicitly call out that we’re making use of the contrapositive. Or perhaps we’re comfortable with the proof as-is and feel it’s clear enough.

The issues of when to apply logical compression and how much compression to apply are subjective matters. However, subjective does not translate to “there are no preferred patterns.” This harks back to ”… learning the idioms of your peers and the broader community.”

Idioms represent convergence toward ideas that are not necessarily formalized. But that convergence is meaningful because it reduces cognitive load. Moreover, an idea that’s used everywhere is familiar. When something registers as unfamiliar, it’s a clue that there may be a problem afoot. In this way, idiomatic writing helps facilitate correctness.

Mendelson’s proof

The problem

Prove the following:

Let $b$ be a greatest lower bound of the non-empty subset $A$ of real numbers. Then there is a sequence $a_1, a_2, \dots$ of real numbers such that $a_n \in A$ for each $n$ and $\lim_{n}a_n = b$.

Preliminaries

We need a bit of scaffolding before we can unpack Mendelson’s proof.

Definition 1.1 - Let $a_1, a_2, \dots$ be a sequence of real numbers. A real number $a$ is said to be the limit of the sequence $a_1, a_2, \dots$, if, given $\epsilon \gt 0$, there is a positive integer $N$ such that, whenever $n \gt N$, $|a - a_n| \lt \epsilon$. In this event we shall also say that the sequence $a_1, a_2, \dots$ converges to $a$ and write $\lim_{n}a_n = a$.

Theorem 1.2 - Let $b$ be a greatest lower bound of the non-empty subset $A$ of real numbers. Then, for each $\epsilon \gt 0$, there is an element $x \in A$ such that $x -b \lt \epsilon$.

The proof

For each $\epsilon = \frac{1}{n}$ we obtain $a_n \in A$ such that $a_n - b \lt \frac{1}{n}$. Since $b$ is a lower bound of $A$, $0 \leq a_n - b$. Therefore $\lim_{n}a_n = b$.

A more verbose alternative

Prior to reading Mendelson’s proof, I probably would have written something like this.

By Theorem 1.2, choose $a_n \in A$ such that $a_n -b \lt \frac{1}{n}$. Doing so for each positive integer $n$ defines the sequence $(a_{n})$. Let $\epsilon \gt 0$. Then there exists a positive integer $N$ such that $\frac{1}{n} \lt \epsilon$ whenever $n \gt N$. Since $b$ is a lower bound of $A$, it follows that $0 \leq a_n -b \lt \frac{1}{n} \lt \epsilon$ when $n \gt N$. Therefore by Definition 1.1, we have $\lim_{n}a_n = b$.

Commentary

Comparing the two proofs, the first sentence in each proof is similar.

For each $\epsilon = \frac{1}{n}$ we obtain $a_n \in A$ such that $a_n - b \lt \frac{1}{n}$.

By Theorem 1.2, choose $a_n \in A$ such that $a_n -b \lt \frac{1}{n}$.

I did not explicitly make mention of an $\epsilon$, at least not as part of my invocation of Theorem 1.2. Mendelson doesn’t explicitly state what theorem he is invoking, but he explicitly chooses a family of $\epsilon$.

Initially, this tripped me up; it took me longer than I’d like to admit to realize that his $\epsilon$ was a direct invocation of Theorem 1.2 and not something he was trying to carry forward to help demonstrate that Definition 1.1 was satisfied.

Next, there’s a large chunk of quantifier unpacking and checkbox ticking that I include which Mendelson does not.

Doing so for each positive integer $n$ defines the sequence $(a_{n})$. Let $\epsilon \gt 0$. Then there exists a positive integer $N$ such that $\frac{1}{n} \lt \epsilon$ whenever $n \gt N$.

I explicitly define the sequence and invoke the Archimedean Property. This is done largely as a beginner’s force of habit. The statement has a logical form. I see the quantifiers and satisfy each of them.

Mendelson expects the reader to supply both the sequence and the Archimedean Property. The sequence is ambient, and the Archimedean Property is a given just by how often it appears in proofs.

In this way, Mendelson respects his reader, and that respect protects the core of the proof from being smothered by the re-litigation of ideas that are used so often as to be taken for granted.

Finally, we look at the ending of each proof.

Since $b$ is a lower bound of $A$, $0 \leq a_n - b$. Therefore $\lim_{n}a_n = b$.

Since $b$ is a lower bound of $A$, it follows that $0 \leq a_n -b \lt \frac{1}{n} \lt \epsilon$ when $n \gt N$. Therefore by Definition 1.1, we have $\lim_{n}a_n = b$.

Again, the ending of my proof is more verbose. I handle 1.1’s $\epsilon$ and produce an $N$. Mendelson does not, confirming his $\epsilon$ belongs solely to the invocation of 1.2. I also explicitly invoke Definition 1.1. Mendelson does not.

The lessons are the same

When I reviewed my fellow learner’s proof, we found that simplification came by reasoning about fewer variables, removing indirection and redundancy, and allowing the proof to pull from some amount of ambient context.

These very same lessons were relayed back to me when I compared Mendelson’s proof to my own!

Ideas that I had grasped well enough to be able to convey to another learner took on a new life in a deeper context, and thoughts that I’ve held about explicitly unpacking quantifiers have been challenged.

I’m left to consider how my proof writing might be impacted by extending enough respect to my readers to let them infer the mundane.