Part 2: Simple Proofs
Introduction
Last chapter, we saw how to translate statements in English to formulas, with a variable for each piece of the sentence. We also saw truth tables and what contradictions/tautologies are.
In this chapter, we will learn how to prove a formula, which means showing that it is a tautology. We could do this by listing all combinations using a truth table, but we saw that these can get enormous, so we need a better method for proving than listing all options. This is why we will use natural deduction to prove formulas.
Assumptions and Proof Goals
Suppose we would like to prove that the following complicatedlooking formula is a tautology:
\( ((a \Rightarrow b) \land a) \Rightarrow b \)
We will write a proof for this in a structured manner. At the bottom of the proof, we write the proof goal, which is what we will try to prove. At the top, we write assumptions, which you do not have to prove, but which are valid only within a certain context. In between, we write intermediate facts that we use to go from the assumptions to the proof goal.
We start by determining the "toplevel" symbol of the formula. In the example, this is \( \Rightarrow \), because we can split up the formula in two subformulas \( (a \Rightarrow b) \land a \) and \( b \), connected with \( \Rightarrow \). The parentheses help to guide us here.
Just like we had a truth table for each symbol, we also have proof rules for each symbol, of the following two types:
 Introduction rules: these are rules that "build" a bigger formula from smaller facts. In practice, you use these rules when you have a proof goal that you need to work toward, but you don't know yet how to prove it (you work backward from the proof goal).
 Elimination rules: these are rules that "deconstruct" a formula into a smaller formula. In practice, you use these rules for reasoning steps (you work forward from assumptions and existing facts).
Rules for \( \Rightarrow \)
The introduction rule for \( \Rightarrow \) says that if you assume the lefthand side \( X \) and manage to prove, using this assumption, that the righthand side \( Y \) is true, then you may conclude that \( X \Rightarrow Y \) is true. It would be written down as follows in your proof:
assume \( X \)  
...  
{ new proof goal }  
\( Y \)  
{ by introduction rule for \( \Rightarrow \) }  
\( X \Rightarrow Y \) 
The extra spacing makes it extra clear where it is allowed to use the assumption, while the lines in {} are comments to explain your steps. You could compare it to writing something like Python code for a program, except this is for a proof.
The elimination rule for \( \Rightarrow \) says that, if you know that an implication \( X \Rightarrow Y \) holds true, and you have proven that the lefthand side \( X \) is true, then you may conclude that the righthand side \( Y \) holds true. It would be written down as follows:
\( X \Rightarrow Y \)  
...  
\( X \)  
...  
{ by elimination rule for \( \Rightarrow \) }  
\( Y \) 
I intentionally wrote uppercase \( X \) and \( Y \), because they do not have to be variables; they can also be more complex subformulas.
Now we can use the introduction rule to prove the example at the start! This is because we were trying to prove something where the toplevel symbol was \( \Rightarrow \). This step would be written as follows:
(1)  assume \( (a \Rightarrow b) \land a \) 
... still left to do ...  
{ ? }  
(?)  \( b \) 
{ by introduction rule for \( \Rightarrow \) on (1) and (?) }  
(?)  \( ( \)\( (a \Rightarrow b) \land a \)\( ) \Rightarrow \) \( b \) 
We also added line numbers to make it easier for a reader to understand what is going on. We have filled in some of the gaps of our proof, but note that it is not complete yet. We need other rules to finish the proof.
Rules for \( \land \)
The introduction rule for \( \land \) is a bit simpler. If you know that \( X \) is true and that \( Y \) is true, then you may conclude that \( X \land Y \) is true:
\( X \)  
...  
\( Y \)  
...  
{ by introduction rule for \( \land \) }  
\( X \land Y \) 
Notice that this introduction rule does not give you an assumption!
The elimination rules for \( \land \) (there are 2) are also quite simple. If you know that \( X \land Y \) holds, then you may conclude \( X \):
\( X \land Y \)  
{ by elimination rule for \( \land \) }  
\( X \) 
In the same way, if you know that \( X \land Y \) holds, then you may conclude \( Y \):
\( X \land Y \)  
{ by elimination rule for \( \land \) }  
\( Y \) 
Finishing the Example Proof
We already had the following part of the proof:
(1)  assume \( (a \Rightarrow b) \land a \) 
... still left to do ...  
{ by what rule? }  
(?)  \( b \) 
{ by introduction rule for \( \Rightarrow \) on (1) and (?) }  
(?)  \( ((a \Rightarrow b) \land a) \Rightarrow b \) 
First of all, we can use the elimination rule for \( \land \) twice to continue the proof for our example:
(1)  assume \( ( \)\( a \Rightarrow b \)\( ) \land \) \( a \) 
{ by elimination rule for \( \land \) on (1) }  
(2)  \( a \Rightarrow b \) 
{ by elimination rule for \( \land \) on (1) }  
(3)  \( a \) 
... still left to do ...  
{ by what rule? }  
(?)  \( b \) 
{ by introduction rule for \( \Rightarrow \) on (1) and (?) }  
(?)  \( ((a \Rightarrow b) \land a) \Rightarrow b \) 
For the last step, we can use the elimination rule for \( \Rightarrow \) to bridge the gap:
(1)  assume \( (a \Rightarrow b) \land a \) 
{ by elimination rule for \( \land \) on (1) }  
(2)  \( a \) \( \Rightarrow \) \( b \) 
{ by elimination rule for \( \land \) on (1) }  
(3)  \( a \) 
{ by elimination rule for \( \Rightarrow \) on (2) and (3) }  
(4)  \( b \) 
{ by introduction rule for \( \Rightarrow \) } on (1) and (4)  
(5)  \( ((a \Rightarrow b) \land a) \Rightarrow b \) 
Another Example
Below you can see another example of a proof with these rules, for the proposition \( ((a \land b) \Rightarrow c) \Rightarrow (a \Rightarrow (b \Rightarrow c)) \). Click the buttons under it to see the process.
...  
(?)  \( ((a \land b) \Rightarrow c) \Rightarrow (a \Rightarrow (b \Rightarrow c)) \) 
(1)  assume \( (a \land b) \Rightarrow c \) 
... still left to do ...  
(?)  \( a \Rightarrow (b \Rightarrow c) \) 
{ by introduction rule for \( \Rightarrow \) on (1) and (?) }  
(?)  \( ( \)\( (a \land b) \Rightarrow c \)\( ) \Rightarrow ( \)\( a \Rightarrow (b \Rightarrow c) \)\( ) \) 
(1)  assume \( (a \land b) \Rightarrow c \) 
(2)  assume \( a \) 
... still left to do ...  
(?)  \( b \Rightarrow c \) 
{ by introduction rule for \( \Rightarrow \) on (2) and (?) }  
(?)  \( a \) \( \Rightarrow ( \)\( b \Rightarrow c \)\( ) \) 
{ by introduction rule for \( \Rightarrow \) on (1) and (?) }  
(?)  \( ((a \land b) \Rightarrow c) \Rightarrow (a \Rightarrow (b \Rightarrow c)) \) 
(1)  assume \( (a \land b) \Rightarrow c \) 
(2)  assume \( a \) 
(3)  assume \( b \) 
... still left to do ...  
(?)  \( c \) 
{ by introduction rule for \( \Rightarrow \) on (3) and (?) }  
(?)  \( b \) \( \Rightarrow \) \( c \) 
{ by introduction rule for \( \Rightarrow \) on (2) and (?) }  
(?)  \( a \Rightarrow (b \Rightarrow c) \) 
{ by introduction rule for \( \Rightarrow \) on (1) and (?) }  
(?)  \( ((a \land b) \Rightarrow c) \Rightarrow (a \Rightarrow (b \Rightarrow c)) \) 
(1)  assume \( (a \land b) \Rightarrow c \) 
(2)  assume \( a \) 
(3)  assume \( b \) 
{ by introduction rule for \( \land \) on (2) and (3) }  
(?)  \( a \) \( \land \) \( b \) 
(?)  \( c \) 
{ by introduction rule for \( \Rightarrow \) on (3) and (?) }  
(?)  \( b \Rightarrow c \) 
{ by introduction rule for \( \Rightarrow \) on (2) and (?) }  
(?)  \( a \Rightarrow (b \Rightarrow c) \) 
{ by introduction rule for \( \Rightarrow \) on (1) and (?) }  
(?)  \( ((a \land b) \Rightarrow c) \Rightarrow (a \Rightarrow (b \Rightarrow c)) \) 
(1)  assume \( ( \)\( a \land b \)\( ) \Rightarrow c \) 
(2)  assume \( a \) 
(3)  assume \( b \) 
{ by introduction rule for \( \land \) on (2) and (3) }  
(4)  \( a \land b \) 
{ by elimination rule for \( \Rightarrow \) on (1) and (4) }  
(5)  \( c \) 
{ by introduction rule for \( \Rightarrow \) on (3) and (5) }  
(6)  \( b \Rightarrow c \) 
{ by introduction rule for \( \Rightarrow \) on (2) and (6) }  
(7)  \( a \Rightarrow (b \Rightarrow c) \) 
{ by introduction rule for \( \Rightarrow \) on (1) and (7) }  
(8)  \( ((a \land b) \Rightarrow c) \Rightarrow (a \Rightarrow (b \Rightarrow c)) \) 
Art by averza on Tumblr (opens new tab)
Incorrect Reasoning
It is important to remember that assumptions and facts can only be used within the context that they were made, unless there is a specific rule for it. The indentation also helps to make this more obvious. An example of an INCORRECT proof that \( a \Rightarrow b \) is a tautology (which it clearly isn't) would be:
(1)  assume \( a \) 
(2)  assume \( b \) 
{ from assumption (2) }  
(3)  \( b \) 
{ by introduction rule for \( \Rightarrow \) on (2) and (3) }  
(4)  \( b \Rightarrow b \) 
{ from assumption (2) (NOT ALLOWED!) }  
(5)  \( b \) 
{ by introduction rule for \( \Rightarrow \) }  
(6)  \( a \Rightarrow b \) 
We used assumption (2) to prove that \( b \Rightarrow b \), which is completely valid, but we then tried to use that assumption outside of its intended scope, which leads to the incorrect conclusion that \( a \Rightarrow b \) is a tautology.
Exercises

Prove that the following formulas are tautologies, using natural deduction:
 \( (a \land b) \Rightarrow a \)
 \( ((a \Rightarrow b) \land (b \Rightarrow c)) \Rightarrow (a \Rightarrow c) \)
 \( (a \Rightarrow (b \Rightarrow c)) \Rightarrow ((a \land b) \Rightarrow c) \)
 \( ((a \Rightarrow b) \land (a \Rightarrow c)) \Rightarrow (a \Rightarrow (b \land c)) \)

For the following formulas, if they are tautologies, prove it; otherwise, give values to \( a \), \( b \) and
\( c \) to show that it also can be false (this is called giving a counterexample):
 \( a \Rightarrow (a \land b) \)
 \( a \Rightarrow (b \Rightarrow a) \)
 \( (b \Rightarrow a) \Rightarrow a \)
Next Lesson
Although this is just an introduction to proving, these concepts are still the "real deal" and are used in basically every proof made by computer scientists (though they may use different notation or leave out some details). In the next chapter, we're going to look at a few more rules that are needed for the other connectives like \( \lor \), \( \lnot \) and \( \Leftrightarrow \). Make sure to do the exercises before moving on to the next chapter!