Module 3: Overview
This module contains resources for learning about proofs of correctness as well as runtime proofs. The module contains multiple sections beginning with a discussion of proof styles and mathematical notation, then working through each proof type with examples and resources. It is best to start with Section 1.
Section 1: Proof Types
In this section we will discuss the three main forms of proofs most commonly used in computer science and mathematics, as well as why proofs are so useful. These are:
- 1Direct Proofs
- 2Proof by Contradiction
- 3Proof by Mathematical Induction
Of these styles, the third is perhaps the most difficult to learn and is discussed in Section 5. Direct proofs are perhaps the most straightforward — they involve making a series of logical statements that, taken in order, arrive at a logical proof of how something is correct. Covered in Section 3.
Proof by contradiction is our second form of proof. It involves finding an example that proves a statement does not hold true. This is particularly useful when proving an algorithm is incorrect for all inputs, though it is not typically useful for proving an algorithm correct. Covered in Section 4.
Proof by induction represents our third and most commonly accepted form of mathematical proof. It involves proving an algorithm holds true for three cases: a base case, an arbitrary n case, and an n+1 case. This allows us to prove an algorithm correct for arbitrary inputs. Covered in Section 5.
Proofs serve a range of purposes in computer science. One of the most common uses is proving the correctness of an algorithm. Where conventional code is often verified using test cases, algorithms typically require a rigorous proof showing the solution is sound for all possible inputs. For example, there exists an inductive proof that Depth First Search will work correctly for any graph — meaning we can trust it for any graph we need to traverse.
Section 2: Syntax and Set Theory
Proofs are less complex than they seem. What often confuses people is simply the language most commonly used when writing them. The main thing to keep in mind is that the goal is to make our language very clear and precise — proofs must be written so their meaning is objective and cannot be misinterpreted.
First, we need to define our proof system S. The first component is our language L, which can be in one of two styles. The first is propositional, wherein the language is composed of logical statements that have a truth value (true or false). The second is predicate-based, wherein the language is composed of informative statements that qualify or provide more information about the element being proved. Our proof is then composed of a set of formulas F described in L, extended to include a set of expressions E built out of L, and governed by a set of rules R.
Below are the mathematical symbols most commonly encountered in proofs. More can be found in the links at the end of this section.
- =
- Is the same as
- <
- Is strictly less than
- >
- Is strictly greater than
- ≤
- Is less than or equal to
- ≥
- Is greater than or equal to
- ≔
- Is equal by definition to
- ∴
- Therefore
- ∋
- Such that — under the condition that
- ⇒
- Implies — logically implies that
- ⇔
- If and only if (iff)
- ∀
- For all (universal quantifier)
- ∃
- There exists (existential quantifier)
- ∄
- There does not exist
- ∎
- QED — end of proof
- ⊂
- Subset of
- ∈
- Is included in (element of)
- ∪
- Union — combination of two sets
- ∩
- Intersection — elements common to two sets
- ∅
- The empty set (null set)
- ∞
- Infinity
Section 3: Direct Proofs
In Section 2 we discussed the symbolism and basics of how we set up proofs. Now we will begin discussing proof types, starting with direct proofs — generally considered the simplest form.
Direct proofs rely on a sequence of logical statements. Starting from accepted facts or axioms, each statement follows logically from the last, until we arrive at the conclusion we set out to prove. One of the best ways to learn how to write direct proofs is by working through a number of examples — the links and videos below provide a thorough collection.
Section 4: Proof by Contradiction
In this section we will discuss the second common form of mathematical proof used in computer science: proof by contradiction. The goal of proof by contradiction is generally to prove a statement as being false.
For example, take the statement: "All sorting algorithms have a runtime no lower than O(n²)." We can set up a proof by contradiction to disprove this relatively trivially. Let us first restate this in mathematical terms:
This statement is the subject of what we are trying to disprove. Our goal is simple: find a sorting algorithm whose runtime is better than O(n²). One example should come to mind quickly: Merge Sort, which has a runtime of O(n log n). We can use existing well-formed proofs of Merge Sort's runtime as a lemma in our proof by contradiction. The full proof can be structured as follows:
It is worth noting that this is a relatively simple example. For this proof to be fully complete, we would also need an inductive portion to formally show that n log n grows more slowly than n², which leads us into the next section.
Section 5: Proof by Induction
In the two previous sections we discussed two of the simpler forms of proofs used in computer science. Proof by induction is the third, and the most common form of proof used in computer science — and the subject of this section.
Proof by induction can be thought of as very similar to recursion. In recursion, we have a base case and a recursive case. In induction, we similarly have three components:
- 1Base case — prove the claim holds when the input is 1 (or the smallest valid value).
- 2Inductive hypothesis — assume the claim holds for some arbitrary n > 1.
- 3Inductive step — using the hypothesis, prove the claim holds for n+1, showing the pattern continues indefinitely.
For example, when proving an algorithm's runtime is correct, we would first prove that the claimed runtime holds for an input of size 1. Next, we assume it holds for an arbitrary input of size n. Finally, the inductive step proves it holds for n+1, establishing the result for all inputs.
As with the other proof sections, there are many different examples of inductive proofs. The links and videos below provide a thorough set of resources.
