We'll be exploring proof via elementary number theory, which is the study of the integers. In particular, we will be discussing divisibility. Division on integers is an interesting operation even though we've likely been dividing numbers since childhood without thinking about it too much. However, where it does come back to trip us up again is when we start to learn how to program. This usually comes in the form of trying to divide two numbers and then remembering that dividing two integers doesn't always give you an integer.
Let $a$ and $b$ be integers. We say that $a$ divides $b$, written $a \mid b$, if and only if there exists an integer $n$ such that $a \cdot n = b$. We also say that $b$ is a multiple of $a$.
We can try to express this formally. Our domain is the integers and we assume that we know basic properties or axioms about integers, like how we know they're equal and how we can multiply them.
We have two integers, $a$ and $b$. Notice that $a \mid b$ is really a predicate: it's a statement about $a$ and $b$. We would like to relate this predicate to more basic operations—in particular, that there's an integer $n$ for which we have $a \cdot n = b$. Equality is also a predicate, which is comparing two things, $a \cdot n$ and $b$. Since this is an existential statement, we can write this as \[\exists n (a \cdot n = b).\]
Now, we want to define the predicate $a \mid b$ so that it is true if and only if there is an integer $n$ for which $a \cdot n = b$.
The connective "if and only if" is not one of the connectives we introduced, but we can construct it using what we've already seen. We say that $p$ if and only if $q$ whenever $p \rightarrow q \wedge q \rightarrow p$. Sometimes this is also written $p \leftrightarrow q$. This means our definition can be rendered formally in the following way: \[a \mid b \leftrightarrow \exists n (a\cdot n = b).\]
A proof is a proof. What kind of a proof? It's a proof. A proof is a proof, and when you have a good proof, it's because it's proven.
So far, we have covered how to say things, but ultimately, what we want to do is verify whether a statement is true or not. This is done by means of proof. Informally, a proof is really just an argument that a statement is valid based on some premises.
In mathematics, the premises are a set of facts, like "For all natural numbers $m$ and $n$, $m+n = n+m$" (that is, addition on the natural numbers is commutative). In very formal settings, we are extra careful to specify exactly which facts we "know" already—these are called axioms. Then, if we apply those facts in certain ways which are described by some rules, we can arrive at some statement, which we know must be true because we followed the rules.
For example, consider the following proposition.
For all integers $a$, $b$, and $c$, if $a \mid b$, then $a \mid bc$.
Within this statement, there are some facts that we need to know already in order to work with if we want to "prove" this statement. We must know facts about integers and the predicate for divisibility, $\mid$.
Here is a list of facts that we take to be true about integers.
| Name | Property |
|---|---|
| Closure under addition | For all integers $a,b$, $a+b$ is an integer. |
| Associativity of addition | For all integers $a,b,c$, $(a+b)+c = a+(b+c)$. |
| Commutativity of addition | For all integers $a,b$, $a+b = b+a$. |
| Additive identity | There exists an integer 0 such that for all integers $a$, $a+0 = a$. |
| Additive inverse | For all integers $a$, there exists an integer $-a$ such that $a+(-a) = 0$. |
| Closure under multiplication | For all integers $a,b$, $a \times b$ is an integer. |
| Associativity of multiplication | For all integers $a,b,c$, $(a \times b) \times c = a \times (b \times c)$. |
| Commutativity of multiplication | For all integers $a,b$, $a \times b = b \times a$. |
| Multiplicative identity | There exists an integer 1 such that for all integers $a$, $a \times 1 = a$. |
| Distributivity of multiplication over addition | For all integers $a,b,c$, $a \times (b+c) = (a \times b) + (a \times c)$. |
You don't need to memorize these—all these facts really say is that addition and multiplication on integers works the way that you've known all along. But it is interesting to note and useful to be aware that we can list these facts and that we rely on them, even if we weren't aware of it. As an aside, these rules together with the set of integers forms the algebraic structure known as a ring.
What then is a formal proof in this context? This is something that the mathematcians of the late 19th century tried to nail down using logic. We might render the above statement as something like \[\forall a,b,c(a \mid b \rightarrow a \mid bc).\] What constitutes a proof of this? Well, we need a way to "prove" a statement that's universally quantified and how to deal with an implication. In other words, the form of the statement determines the rules that we apply to come up with our argument, or proof.
Notice that if we have everything set up, we don't actually need to "know" what our predicates "mean", since the validity of the proof is determined totally by the form of the sentence. What this means is that in the most formal versions of this process, we get to the level of manipulation of symbols, akin to string rewriting. It's not hard to see that when we get to this level, a proof really becomes something like a program, with strict rules that can be checked and validated.
We want to approach less formally, so what we are trying to do is begin with a set of statements that represent facts that we already know and try to apply rules to these facts so that we can construct a "true" statement by the end of the process. Any statement that we can arrive at by following these rules is considered "valid" and the steps that we take constitute the proof.
Let's consider the proposition $p \wedge q$. Earlier, we were given the truth table for this statement, but what would a proof of such a proposition look like? Well we know that in order for $p \wedge q$ to be true, it has to be the case that $p$ is true and that $q$ is true. But how do we know that $p$ and $q$ are both true? Well, if we had a proof for $p$, we would know that it's true and if we had a proof for $q$, we would know it's true. That is, if we have a proof of $p$ and we have a proof of $q$, then we are able to construct a proof of $p \wedge q$. We can express this idea as a rule, written \[\frac{p \quad q}{p \wedge q} \wedge\!i.\]
This is an example of an inference rule. The rule we discussed above is called $\wedge$-introduction, since it creates a conjunction.
Inference rules are rules that govern how we can construct proofs for our statements based on what we have already proved. We can define a whole bunch of these inference rules and by using these rules, we can manipulate formulas to acquire other formulas. Inference rules are often specified in the following way: \[\frac{\alpha_1 \quad \alpha_2 \quad \cdots \quad \alpha_n}{\beta}.\]
This rule says that if I know that statements $\alpha_1, \alpha_2, \dots, \alpha_n$ are valid, then I can conclude that $\beta$ is also valid. A statement $\alpha_i$ is valid if we already know it beforehand (i.e. it is a known, given fact) or if it shows up at some earlier point in the proof. The reason for this is that since we were able to get to $\alpha_i$ at some point earlier in the proof, we must have obtained it by following our proof rules. Therefore, if we stopped at the point that we got $\alpha_i$, we would have a proof if $\alpha_i$.
Inference rules define a proof system. The proof system that we'll be referring to is natural deduction, which was defined by Gerhard Gentzen in the 1930s, and contains rules that correspond to common patterns of proof used by human mathematicians. There are other proof systems which are geared for other purposes, such as use with computers or the study of proof systems.
We won't actually be learning or using natural deduction to prove things. Instead, we'll be walking through basic proof techniques and noting how and where they correspond to rules that are defined in natural deduction.
Here's a particularly important inference rule (dating back to antiquity): $$\frac{p \rightarrow q \quad p}{q} \rightarrow\!e.$$
This inference rule is called $\rightarrow$-elimination. What does it mean? It's an argument of the form
This is classical logic. But let's consider it from the perspective of proof. What this says is that if we have a proof of the proposition $p \rightarrow q$ and we have a proof of $p$, we are able to construct a proof for $q$.
For instance, the following argument follows the same structure:
We can rewrite this so that it's even more abstract.
Notice that this is just a linear form of our inference rule from above. There's nothing that says that $p \rightarrow q$ and $p$ have to appear in this order. Also note that in very formal proofs, we cite the rule we're applying along with which lines we're applying the rule to.
One thing to notice that the content of the argument has no bearing on whether it's valid or not. The only thing that matters is whether we have followed the rules to get from one statement to the next. This is not unlike how many people try to argue on the internet.
Let's start trying to parse the sentence that describes our induction axiom and come up with a proof for it. Recall that we have the following sentence given to us \[P(z) \wedge \forall k (P(k) \rightarrow P(\operatorname{succ}(k))) \rightarrow \forall n P(n).\]
Our goal is to prove $\forall n P(n)$. Notice that this is a sentence of the form $p \rightarrow q$ and we want to prove $q$. This means that using the second of the rules we saw, we know that what we need to do is prove $p$, which is \[P(z) \wedge \forall k (P(k) \rightarrow P(\operatorname{succ}(k))).\]
Now, observe that this is a conjunction: it is a sentence of the form $p \wedge q$. So this means we need a proof for $p$, which in our case is $P(z)$ and a proof for $q$, which is $\forall k (P(k) \rightarrow P(\operatorname{succ}(k)))$.
This is exactly the template for induction:
We end up with a proof tree that looks like \begin{prooftree} \AxiomC{$P(z) \wedge \forall k (P(k) \rightarrow P(\operatorname{succ}(k))) \rightarrow \forall n P(n)$} \AxiomC{$P(z)$} \AxiomC{$\forall k (P(k) \rightarrow P(\operatorname{succ}(k)))$} \BIC{$P(z) \wedge \forall k (P(k) \rightarrow P(\operatorname{succ}(k)))$} \BIC{$\forall n P(n)$} \end{prooftree}
The base case, $P(z)$, is fairly straightforward to prove—it's a single predicate, so we can prove this directly. However, in order to prove the inductive case, $\forall k (P(k) \rightarrow P(\operatorname{succ}(k)))$, we need to continue to peel back pieces, starting with how to prove universally quantified statements.
A universally quantified statement is one of the form $\forall x P(x)$. At first glance, it seems like we have a lot of work to do, because we have to show that this statement holds for every $x$ in our domain. One way we can attempt this is to go through every element in our domain and see if we have a proof for each one. This is bad because our domain may be infinitely large (as is the case with natural numbers.
Instead, what we do is "pick" a generic representative and continue our argument with that representative. Since we just choose an arbitrary element with nothing special about it, we can conclude that our statement must hold for any element from the domain we've chosen, because we could've picked any of them.
Recall the statement that begins the inductive case for the proof of Proposition 1.9 from last class:
If $n = \operatorname{succ}(k)$ for some natural number $k$ $\dots$
The phrasing is a bit different, but the idea is that we are picking a generic natural number $k$, from which we discuss the rest of the inductive case. Since we don't know anything about $k$, we can conclude that whatever we say will hold for any natural number.
What does the inference rule for this look like? We call this rule $\forall$-introduction: \[\frac{\boxed{\begin{matrix} u \qquad \\ \vdots \\ P(u) \end{matrix}}}{\forall x P(x)} \forall i\] Why is there a box? This notational style is due to Jaśkowski in 1934 and is a way to show that $u$ exists only inside the box. You can think of the box as the "scope" of $u$ and that $u$ can't be used outside of the box. (Notice how "scope" is a concept that has its origins in mathematical logic)
This rule looks complicated (and the notation admittedly is), but it actually tells us exactly what a proof for $\forall x \in S, P(x)$ looks like.
Once we apply this rule, we are cleared to consider the sentence that has been quantified. In our case, this is $P(k) \rightarrow P(\operatorname{succ}(k)$, which is an implication.
Let's see an example of universal quantification by starting a proof of Proposition 2.13, which was
For all integers $a$, $b$, and $c$, if $a \mid b$, then $a \mid bc$.
This had the formula $\forall a,b,c (a \mid b \rightarrow a \mid bc)$.
Let $a$, $b$, and $c$ be arbitrary integers. \[\cdots\]
Now, we would proceed with our proof by using the $a,b,c$ we chose. This means constructing a proof for the sentence $a \mid b \rightarrow a \mid bc$. To do that, we need to know how to prove an implication.
As stated earlier, most theorems are implications. This corresponds to the inference rule $\rightarrow$-introduction: \[\frac{\boxed{\begin{matrix}p \\ \vdots \\ q\end{matrix}}}{p \rightarrow q} \rightarrow\!i\] What this rule means is that in order to prove such statements, we assume $p$ and then use that assumption to show that the conclusion $q$ is true. Again, we use a box to show that $p$ exists as an assumption inside the box, since it's not one of our given facts.
Let's continue our proof from above. Since we dealt with the universal quantification, we are left with the statement $a \mid b \rightarrow a \mid bc$. This means we need to assume $a \mid b$ is true and we can use this assumption to complete our proof.
Let $a$, $b$, and $c$ be arbitrary integers. We assume that $a \mid b$. So there exists an integer $n$ such that $a \cdot n = b$. Then \begin{align*} bc &= (a \cdot n) \cdot c &\text{substitution} \\ &= a \cdot (n \cdot c) &\text{associativity} \end{align*} We note that $n \cdot c$ is an integer, since the integers are closed under multiplication. Therefore, there exists an integer $n'$ (which is our new name for $n \cdot c$) such that $a \cdot n' = bc$. Therefore, $a \mid bc$.
From this, we can see that a proof of $p \rightarrow q$ involves
Here, step (2) is a bit thin on details, but this is where the clever combining of mathematical facts and knowledge happens, so there's not much we can say regarding the structure of the proof.
You may have noticed we did something sneaky in the above proof. When we applied the definitions for divisibility, in a sense, we substituted $a \mid b$ for the statement $\exists n (a\cdot n = b)$. This means that we were working with an existentially quantified statement. Here's what happened
The inference rule for using an existentially quantiifed statement is \[\frac{\begin{matrix} \quad \\ \quad \\ \exists x P(x) \end{matrix} \quad \boxed{\begin{matrix} P(u), \text{sub $u$ for $x$} \\ \vdots \\ Q \end{matrix}}}{Q} \exists e\] In other words, if we want to use an existentially quantified statement $\exists x P(x)$, we simply choose a specific element $u$ and work with the statement $P(u)$. Notice that
Like the other rules we saw earlier, the chosen $u$ exists only within a specific scope. But we can use this fact to arrive at a proof of some other statement $Q$.
However, this is only half the story, because we end up having to arrive at a proof for an existentially quantified statement:
That is, we showed that there exists an appropriate integer and we use this to construct an existentially quantified statement. This is the inference rule \[\frac{P(t)}{\exists x P(x)} \exists i\] In essence, this is a proof that looks like this: