4.6 Proofs and Programming I: Divisibility

In the previous section, we introduced the concept of using mathematical ideas to create alternate implementations of a function. However, that example might not have been totally satisfying, because we just took for granted the mathematical theorem that gave us the formula \(\sum_{i=1}^n i = \frac{n(n+1)}{2}\). Rather than ask why our code is correct, shouldn’t we now ask why this theorem is correct instead?

So in the last two sections of this chapter, we’ll take a step back and review the basic principles of mathematical definitions and proofs. We say “review” here because you are currently learning about proofs in greater detail in your first-year calculus courses. However, we know that proofs can be challenging when first starting out, and so are taking some time to introduce and cover proofs in these notes as well. We’ll then use these principles in two ways: to practice writing some simple proofs, and to see how the statements we’re proving can translate directly into the code we write.

In Chapter 3, we studied how to express statements precisely using the language of predicate logic. But just as English enables us to make both true and false claims, the language of predicate logic allows for the expression of both true and false sentences. In this section, we will turn our attention to analyzing and communicating the truth or falsehood of these statements. You will develop the skills required to answer the following questions:

• How can you figure out if a given statement is True or False?
• If you know a statement is True, how can you convince others that it is True? How can you do the same if you know the statement is False instead?
• If someone gives you an explanation of why a statement is True, how do you know whether to believe them or not?

These questions draw a distinction between the internal and external components of mathematical reasoning. When given a new statement, you’ll first need to figure out for yourself whether it is true (internal), and then be able to express your thought process to others (external). But even though we make a separation, these two processes are certainly connected: it is only after convincing yourself that a statement is true that you should then try to convince others. And often in the process of formalizing your intuition for others, you notice an error or gap in your reasoning that causes you to revisit your intuition—or make you question whether the statement is actually true!

A mathematical proof is how we communicate ideas about the truth or falsehood of a statement to others. There are many different philosophical ideas about what constitutes a proof, but what they all have in common is that a proof is a mode of communication, from the person creating the proof to the person digesting it. In this course, we will focus on reading and creating our own written mathematical proofs, which is the standard proof medium in computer science.

As with all forms of communication, the style and content of a proof varies depending on the audience. In this course, the audience for all of our proofs will be an average first-year computer science student (and not your TA or instructor). As we will discuss, your audience determines how formal a proof should be (here, quite formal), and what background knowledge you can assume is understood without explanation (here, not much).

However, there is even variation in the typical computer science student with experience in this area, so as much as possible in this course, we will introduce new mathematical domains to serve as the objects of study in our proofs.

This approach has three very nice benefits: first, by building domains from the ground up, we can specify absolutely the common definitions and properties that everyone may assume and use freely in proofs; second, these domains are the theoretical foundation of many areas of computer science, and learning about them here will serve you well in many future courses; and third, learning about new domains will help develop the skill of reading about a new mathematical context and understanding it.In other words, you won’t just learn about new domains; you’ll learn how to learn about new domains! The definitions and axioms of a new domain communicate the foundation upon which we build new proofs—in order to prove things, we need to understand the objects that we’re talking about first.

It turns out that proving formulas like the one from the previous section is a bit tricky, and is done most easily using a proof technique that we’ll cover later this year in CSC111. So instead, in this section we’ll use the domain of number theory, which is a branch of mathematics that studies properties of the natural numbers and integers. We’ve chosen this domain because it doesn’t require much prior mathematical knowledge, is complex enough to give us plenty of practice writing proofs, and prepares us for some really cool computer science applications in cryptography that we’ll get to later this term!

Defining divisibility

Throughout this course, we will study various mathematical objects that play key roles in computer science. As these objects become more complex, so too will our statements about them, to the point where if we try to write out everything using just basic set and arithmetic operations, our formulas won’t fit on a single line! To avoid this problem, we create definitions, which we can use to express a long idea using a single term.This is analogous to using local variables or helper functions in programming to express part of an overall value or computation.

We start out here by taking a common concept (divisibility) and providing a formal definition in predicate logic.

Comment: This definition of divisibility also permits \(d = 0\), which may be a bit surprising! We’ll revisit this case down below.

Proofs using divisibility

We’re going to start out our exploration of proofs by studying a few simple statements. You may find our first few examples a bit on the easy side, which is fine. We are using them not so much for their ability to generate mathematical insight, but rather to model both the thinking and the writing that would go into approaching a problem.

Each example in this section is divided into three or four parts:

1. The statement that we want to prove or disprove. Sometimes, we’ll specify whether to prove or disprove it, and other times deciding whether the statement is true or false is part of the exercise.
2. A translation of the statement into predicate logic. This step often provides insight into the logical structure of the statement that we are considering, which in turn informs the structure and techniques that we will use in our proofs.
3. A discussion to try to gain some intuition about why the statement is true. You’ll tend to see that these are written very informally, as if we are talking to a friend on a whiteboard. The discussion usually will reveal the mathematical insight that forms the content of a proof. This is often the hardest part of developing a proof, so please don’t skip these sections!
4. A formal proof. This is meant to be a standalone piece of writing, the “final product” of our earlier work. Depending on the depth of the discussion, the formal proof might end up being almost mechanical – a matter of formalizing our intuition.

With this in mind, let’s dive right in!

We can draw from this example a more general technique for structuring our existence proofs. A statement of the form \(\exists x \in S,~P(x)\) is True when at least one element of \(S\) satisfies \(P\). The easiest way to convince someone that this is True is to actually find the concrete element that satisfies \(P\), and then show that it does. This is not the only proof technique used for existence proofs. You’ll study more sophisticated ways of doing such proofs in future courses. This is so natural a strategy that it should not be surprising that there is a standard “proof structure” for proving existential statements.

Note that the two blanks represent the same element of \(S\), which you get to choose as a prover. Thus existence proofs usually come down to finding a correct element of the domain which satisfy the required properties.

Here is another example which uses the same idea, but with two existentially-quantified variables.

The previous example is the first one that had multiple quantifiers. In our proof, we had to give explicit values for both \(a\) and \(k\) to show that the statement held. Just as how a sentence in predicate logic must have all its variables quantified, a mathematical proof must introduce all variables contained in the sentence being proven.

Alternating quantifiers, revisited

In 3.7 Logical Statements with Multiple Quantifiers, we saw how changing the order of an existential and universal quantifier changed the meaning of a statement. Now, we’ll study how the order of quantifiers changes how we can introduce variables in a proof.

This proof is quite short, but introduces a few new elements. First, it introduced a variable \(n\) that could represent any real number. Unlike the previous existence proofs, when we introduced this variable \(n\) we did not specify a concrete value like \(10\), but rather said that \(n\) was an arbitrary real number by writing ``Let \(n \in \Z\).You might notice that we use the same word “let” to introduce both existentially- and universally-quantified variables. However, you should always be able to tell how the variable is quantified based on whether it is given a concrete value or an “arbitrary” value in the proof.

The other interesting element of this proof was that it contained an existentially-quantified variable \(k\) after the \(\forall n \in \Z\). We used an extremely important tool at our disposal when it comes to proofs with multiple quantifiers: any existentially-quantified variable can be assigned a value that depends on the variables defined before it.

In our proof, we first defined \(n\) to be an arbitrary integer. Immediately after this, we wanted to show that for this \(n\), \(\exists k \in \Z,~ n = 1 \cdot k\). And to prove this, we needed a value for \(k\)—a “let” statement. Because we define \(k\) after having defined \(n\), we can use \(n\) in the definition of \(k\) and say “Let \(k = n\).” It may be helpful to think about the analogous process in programming. We first initialize a variable \(n\), and then define a new variable \(k\) that is assigned the value of \(n\).

Even though this may seem obvious, one important thing to note is that the order of variables in the statement determines the order in which the variables must be introduced in the proof, and hence which variables can depend on which other variables. For example, consider the following erroneous “proof.”

This proof may look very similar to the previous one, but it contains one crucial difference. The very first sentence, “Let \(k = n\),” is invalid: at that point, \(n\) has not yet been defined! This is analogous to a NameError in Python. This is the result of having switched around the order of the quantifiers, which forces \(k\) to be defined independently of whatever \(n\) is chosen.

Note: don’t assume that just because one proof is invalid, that all proofs of this statement are invalid! We cannot conclude that this statement is False just because we found one proof that didn’t work.A meta way of looking at this: a statement is True when there exists a correct proof of it. That said, this statement is indeed False, and we’ll see later on how to prove that a statement is False instead of True.

Proving statements with implications

Let’s look at one new example.

Whew, that was a bit longer than the proofs we’ve already done. There were a lot of new elements that we introduced here, so let’s break them down:

• After introducing \(n\) and \(d\), we wanted to prove the implication \(d \mid n \Rightarrow d \leq n\). To prove an implication, we need to assume that the hypothesis was True, and then prove that the conclusion is also True. In our proof, we wrote “Assume \(d \mid n\).”

  This is not a claim that \(d \mid n\) is True; rather, it is a way to consider what would happen if \(d \mid n\) were True. The goal for the rest of the proof was to prove that \(d \leq n\).

  This proof structure is common when proving an implication:

  A typical proof of an implication (direct).

  Given statement to prove: \(p \Rightarrow q\).

  Assume \(p\).

  [Proof that \(q\) is True.]

• When we assumed that \(d \mid n\), what this really did was introduce a new variable \(k \in \Z\) from the definition of divisibility. This might seem a little odd, but take a moment to think about what this means in English. We assumed that \(d\) divides \(n\), which (by definition) is the same as assuming that there exists an integer \(k\) such that \(n = kd\). Given that such a number exists, we can give it a name and refer to it in the rest of our proof.

  In general, assuming an existential statement (“assume there exists…”) is the second way to introduce a variable into a proof, and something to look out for and use in your own proofs.

Expressing divisibility in Python

So far, we have worked with the divisibility predicate \(\mid\) as a purely theoretical tool. But because predicates are just functions, we can express these in programming languages as well. Here is the start of a function design in Python:

def divides(d: int, n: int) -> bool:
    """Return whether d divides n."""

While we can use the modulo operator % to implement this function (more on this later), we’ll remain faithful to the mathematical definition as much as possible:

\[ d \mid n ~:~ ''\exists k \in \Z,~ n = dk'' \quad \text{where $n, d \in \Z$} \]

Unfortunately, there is one challenge with translating the mathematical definition of divisibility precisely into a Python function. In mathematics we have no trouble at all representing an infinite set of numbers with the symbol \(\Z\); but in a computer program, we cannot represent infinite sets in the same way. Instead, we’ll use the following theorem to restrict the set of numbers to quantify over. This theorem can be proved using the same approach as the previous example we looked at, except dividing the proof into cases based on whether \(n\) and \(d\) are positive or negative.

This theorem tells us that for a given integer \(n\), its set of possible divisors is \(\{-|n|, -|n| + 1, \dots, |n| - 1, |n|\}\) How do we represent such a set in Python? We can use the range data type: Remember the asymmetry here: the start argument for range is inclusive, but the end argument is exclusive. So we need abs(n) + 1, not abs(n), as the second argument.

possible_divisors = range(-abs(n), abs(n) + 1)

And then we can replace \(\Z\) by this variable in the definition of divisibility to obtain \(\exists k \in possible\_divisors,~ n = kd\). We can now translate this directly into Python code using what we learned earlier this chapter:

def divides(d: int, n: int) -> bool:
    """Return whether d divides n."""
    possible_divisors = range(- abs(n), abs(n) + 1)
    return any({n == k * d for k in possible_divisors})

Divisibility and the remainder operation

You might have noticed that our definition of divides, though faithful to the mathematical definition, is not the same as how we’ve previously determined whether a number is divisible by 2 (i.e., is even).

def is_even(n: int) -> bool:
    """Return whether n is even."""
    return n % 2 == 0

In this case, we check whether n is divisible by 2 by checking whether the remainder when n is divided by 2 is 0 or not. So what we have now is a repeat of sum_to_n_v1 and sum_to_n_v2 from the previous section: two potential implementations of the same definition, with one implementation being a literal translation of the definition and the other implementation looking faster but using additional mathematical properties.

It turns out that for non-zero \(d \in Z\), checking remainders is equivalent to the original definition of divisibility. We can state this precisely using the following theorem.

Again this seems “obvious”, but how would we actually prove it? To do so, we need to learn about the formal definition of remainders, which comes from the following theorem.

So now using the formal definition of remainder, we can give a proof of our Divisibility and Remainders Theorem:

def divides_v2(d: int, n: int) -> bool:
    """Return whether d divides n."""
    if d == 0:
        # This is the original definition.
        possible_divisors = range(-abs(n), abs(n) + 1)
        return any({n == k * d for k in possible_divisors})
    else:
        # This is a new but equivalent check.
        return n % d == 0

def divides_v3(d: int, n: int) -> bool:
    """Return whether d divides n."""
    if d == 0:
        # This is another new, equivalent check.
        return n == 0
    else:
        # This is a new but equivalent check.
        return n % d == 0