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.
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 a whole, as well as why proofs are so useful.
These include the following:
1: Direct Proofs
2: Proof by Contradiction
3: Proof by Mathematical Induction
Of these styles of proofs, the third is perhaps the most difficult proof style to learn.
This proof style is discussed in section 5.
Direct proofs are perhaps the most straight forward.
A direct proof involves making a series of logical statements that taken in order arrive on a logical proof of how something is correct.
We will discuss direct proofs more in section 3.
Proof by contradiction is our second form of proof.
Proof by contradiction involves finding an example that proves that a statement does not hold true.
This is particularly useful when proving an algorithm is incorrect for all inputs.
Proof by contradiction is not typically useful for proving an algorithm correct, however.
We will discuss proof by contradiction in section 4.
Finally proof by induction represents our third and typically most commonly accepted form of mathematical proof.
Proof by induction involves proving an algorithm holds true for three cases: a base case, an arbitrary n case, and an n+1 case.
This style of proof allows us to prove an algorithm correct for arbitrary inputs.
We will discuss this style of proof more in section 5.
Proofs serve a range of purposes in computer science.
One of the most common uses for proofs is proving the correctness of an algorithm.
When one develops an algorithm or a solution to a problem, it is generally important to prove that the solution is sound.
Where with conventional code we often simply test the code using a range of test cases, with algorithms, we often need to go a step further.
Algorithms development typically requires the development of a rigerous proof for why the algorithm is sound for all possible range of values that it needs to work with.
Consider the Depth First Search algorithm.
There exists an inductive proof that this algorithm will work correctly for any graph.
This means that we can trust depth first search for any graph that we need to traverse and find an element on.
Section 2: Syntax and Set Theory
Proofs are less complex than they seem.
What often confuses people when learning proofs is simply the language that is most commonly used when writing proofs.
The main thing to keep in mind when reading or writing a proof of any of the three types we'll discuss is that the goal is the make sure that our language is very clear and precise.
The goal of proofs is to ensure that the language used cannot be misinterpreted and the meaning is objective.
Firstly, we need to define what our proof system or language will be.
Lets call this proof system S.
The first component of our proof system is our language.
This language L can be in one of two different styles.
The first is propositional, wherein the language is composed of logical statements that have some sort of 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 we are trying to prove.
We also accept that we will make our proof out of a set of formulas F that are described in the language L.
We also accept that this will be extended to include a set of expressions E that will be built out of our language L.
What does all of this mean?
The goal of a proof is to define with logical statements a sequence of statements that will prove something with certainty.
Our goal with the above logic is to carefully spell out what goes into a proof.
Our proofs have a specific system of logic, a set of logical statements that will compose the proof, and a set of rules R that will govern how we define the proof.
This is just a brief introduction to our proof systems and how we specify and define them.
Linked at the end of this section are a number of examples for these systems and how we express them.
Let us now consider some basic symbols commonly used in proofs.
= (the equals sign) means “is the same as”
< (the less than sign) means “is strictly less than”
> (the greater than sign) means "is strictly greater than"
≤ (the less than or equal sign) means "is less than or equal to"
≥ (“greater than or equals”)
≔ means "is equal by definition to"
∴ means "therefore"
∋ (the such that sign) means "under the condition that"
⇒ (the implies sign) means "logically implies that"
⇐⇒ (the iff sign) means "if and only if"
∀ means "for all" (universal quantifier)
∃ means "there exists" (the existential quantifier)
∄ means "there does not exist"
∎ means "QED or end of proof"
⊂ means "subset of"
∈ means "is included in"
∪ means "union" or combination of two sets
∩ means "intersection" or difference of two sets
∅ means "the empty set" somtimes referred to as the null set.
∞ means infinity
More symbols can be found discussed in the links included at the end of this section, though this represents many of the common ones you will work with.
In section 2, we discussed much of the symbolism and the basics of how we set up proofs.
Now, in section 3, we will begin discussing types of proofs.
Our first proof type is commonly considered the simplest proof type.
This is known as a direct proof.
Direct proofs rely on a sequence of logical statements.
For proofs, one of the best ways to learn how to write proofs is by considering a number of examples.
Thus for this section, please consider the linked videos and examples compiled below.
In this section, we will discuss the second common form of mathematical proof that is used in computer science.
This is what is known as proof by contradiction.
The goal behind proof by contradiction is generally to prove a statement as being false.
For example, lets take the statement: "All sorting algorithms have a runtime no lower than O(n squared)".
We can set up a proof by contradiction to disprove this statement relatively trivially.
Lets first restate this in mathematical terms:
There exists the set of all well-defined known sorting algorithms,
where ∀ algorithms in this set, the runtime is never lower asymptotically than O(n squared).
This statement, we take to be the subject of what we are trying to disprove.
Our goal with this proof is simple: we need to find a sorting algorithm that has a runtime that is not O(n squared).
One example should come to mind relatively quickly: Merge sort.
We know that merge sort has a runtime of O(n log(n)).
We also know that there exists well-formed proofs that we can refer to as justification for this runtime.
We can use these existing proofs for the runtime of merge sort as a lemma in our proof by contradiction.
Thus, we can say that there exists a sorting algorithm that has a runtime of O (n log(n)).
We now need to show that O(n log(n)) is less than O (n squared).
Once we have accomplished this, we have shown that there exists a sorting algorithm that disproves our original statement.
Thus the statement we are trying to disprove is indeed incorrect and has been disproven.
We can set up the full proof as follows:
- There exists the set of all known well-defined sorting algorithms, where ∀ algorithms in this set, the runtime is never lower asymptotically than O(n squared).
- We accept that there exists a range of known and defined sorting algorithms, and that Merge Sort ∈ the set of all sorting algorithms.
- We accept that Merge Sort has been proven as a correct sorting algorithm.
- We also accept that Merge Sort has been proven as having a runtime of O(n log(n)).
-O (n log(n)) is asymptotically faster than O (n squared).
-Therefore we see that our statement that ∀ algorithms in the set of sorting algorithms the runtime is never lower than O (n squared) is false by proof by contradiction.
It is worth noting that this is a relatively simple example.
It is also worth noting that for this proof to be complete, we would need an inductive portion to this proof for it to be fully complete, as we need to show that n logn grows more slowly than n squared.
If you would like more examples, consider the videos and articles linked below.
In the two previous sections we discussed two of the simpler forms of proofs utilized in computer science.
Proof by induction is the third and the most common of the forms of proofs used in computer science, and is what we will be discussing in this section.
Proof by induction can be thought of as being very similar to recursion.
In recursion, we accept that we have an base case and a recursive case.
In induction, we have a base case, or a case we want to prove where our input is 1.
For example, lets say we are proving an algorithm's runtime is correct.
We would first prove that what we claim our algorithm's runtime is holds true for a case where our input value is 1.
Next, we want to prove that our algorithm is correct for the n case.
In the n case, n represents an arbitrary input value.
For example, if we are looking to prove the runtime of an algorithm, n would be our arbitrary n case where n is some value >1.
Once we have proven that it holds true for any arbitrary n value, the inductive step aims to prove that this pattern will continue indefinitely.
This is known as the inductive step or n+1 step.
As with our other proof sections, there are a lot of different examples of inductive proofs.
Thus, consider the links and videos that have been provided below.