In general, arguments are more complicated that those we've considered so far. Here, for example, is an argument that has five premises:
Is this argument valid? Of course, you could use a truth table to check whether the conjunction of the premises logically implies the conclusion. But with five propositional variables, the table would have 32 lines, and the size of the table grows quickly when more propositional variables are used. So, in general, truth tables are not practical.
Fortunately, there is another way to proceed, based on the fact that it is possible to chain several logical deductions together. For example, if P⊢Q and Q⊢R, it follows that P⊢R. This means we can demonstrate the validity of an argument by deducing the conclusion from the premises in a sequence of steps. These steps can be presented in the form of a proof:
A formal proof that an argument is valid consists of a sequence of propositions such that the last proposition in the sequence is the conclusion of the argument, and every proposition in the sequence is either a premise of the argument or follows by logical deduction from propositions that precede it in the list.
The deduction rules, the primitive argument forms that we will chain together into complete proofs, are described in more detail below. One of the characteristics of natural deduction is that there are rules associated with each logical operator that determine how to either introduce or eliminate the operator. This can provide a great deal of guidance when writing a proof, because as you fill in the steps you can look at the main operators of the current goal(s) and the available premises—either you will work backwards from a goal by use of an introduction rule or you will work forwards from a premise by use of an elimination rule.
The existence of such a proof shows that the conclusion follows logically from the premises, and therefore that the argument is valid. Here is a formal proof that the argument given above is valid. Each proposition in the proof is justified by a subproof using an appropriate rule.
Once a formal proof has been constructed, it is convincing. Unfortunately, it's not necessarily easy to come up with the proof. Usually, the best method is a combination of working forward ("Here's what I know, what can I deduce from that?") and working backward ("Here's what I need to prove, what other things would imply that?"). For this proof, I might have thought: I want to prove s. I know that p∧r implies s, so if I can prove p∧r, I'm OK. But to prove p∧r, it'll be enough to prove p and r separately….
As mentioned above, the particular set of primitive argument forms that we will use are grouped into introduction and elimination rules for each of the logical operators. Here we will explain each deduction rule, justify it, and show examples of how they may be used in proofs. At the end of this section is a table summarizing all of the rules.
The conjunction p∧q is true when both p and q are true. Therefore, to introduce the conjunction p∧q in a proof we need to first establish the premises p and q individually:
The name of the rule is given as "∧-Intro", and the conclusion p∧q is shown after the colon on the top line of the rule box. The nested proof blocks, labeled with question marks, are "holes"; in a complete proof, they will be filled with appropriate subproofs for the corresponding propositions, p and q.
Here is an example of how this rule might be used in the proof of ¬p, p∨q ⊢ ¬p ∧ (p∨q). Note how the premises are available through the names h0 and h1.
The elimination rules for conjunction allow us to move from the premise p∧q to either the conclusion p or the conclusion q:
Here is a proof that combines the introduction and elimination rules for conjunction to prove p∧q ⊢ q∧p, i.e., that AND is commutative:
Note that we used the second elimination rule in the first subproof to extract q from the hypothesis,
while we use the first elimination rule in the second subproof to extract p. We can also break out the subproofs using a "Let" block, so that we can give them names; this is often useful when building up a proof in the "forward" direction:
The implication p→q says that whenever p is true, q must also be true. To introduce an implication in a proof, we will temporarily assume p and show that, based on that assumption, we are then able to conclude q. As a deduction rule, this argument will take the form of a nested proof, analogous to a nested block of code that may introduce temporary local variables, or a function definition that may use parameters. The notation we will use for this is inspired by the notation for an anonymous function block in languages such as JavaScript, Scala, and ReasonML:
The indented subproof after the double arrow (⇒) is like the body of a function where an additional parameter is available: the hypothesis h0 which allows us to temporarily assume p. Just as with parameters and local variables, we are not allowed to use this hypothesis outside of the nested subproof; it would be incorrect to conclude that p is true more generally, beyond the scope of this introduction rule.
Here is an example of a proof of the tautology (since a tautology may be viewed as an argument with no premises) p→p:
A Theorem box may show some features that we have not seen yet. The natural deduction environment embedded in this page can also be used to construct proofs, although all of the examples we have seen so far are uneditable. If a proof under construction contains "holes", marked with a question mark (?), then that proof is incomplete, indicated by the cross-hatched background on the Theorem box. In an active proof environment, you may interact with these holes to incrementally complete the proof, for example by dragging a hypothesis for the desired proposition, or by selecting a rule from the toolbox. There are also keyboard shortcuts for all of these actions; for example, if you type "&I" followed by the Return key, that is equivalent to choosing the And-Introduction rule, while "h0" enters a reference to hypothesis h0.
As an exercise, see if you can complete proofs of the tautologies p∧q → p∧q and p∧q → q∧p. The first should be very simple, while the second will require some of the proof rules from the previous section. Hint: start by clicking on the toolbox button and selecting the →-Intro rule, then see what remains to be shown to prove each theorem.
The analogy with defining a function taking the hypothesis p as a parameter and returning the conclusion q is not accidental. The elimination rule, which you may recognize as our old friend modus ponens, is very much like function application: if we have a proof of p→q, and we can also supply an argument that p is true, then we may conclude that q is true. Just as a function body describes how to takes an argument passed in through its parameter and compute a result, the subproof that establishes p→q tells us how to take an argument (!) for p and produce the extra steps needed to conclude q.
Here is a proof of the argument p→q ⊢ p→p∧q:
To prove the disjunction p∨q, it is enough to prove either p or q alone. This leads to two obvious introduction rules:
Here are two distinct proofs of the argument p∧q ⊢ p∨q:
Although they have the same premises and conclusions, these two proofs are giving fundamentally different reasons why the conclusion follows from the premise. Note that in the introduction rules for disjunction, one of the terms in the disjunction appears "from nowhere". The argument in proof 1 could equally well conclude p∨r from the premise p∧q, where r could be anything; however, the argument in proof 2 would allow us to conclude instead r∨q for any proposition r.
This peculiar behavior of disjunction extends to the elimination rule. Whereas the introduction rules appear to be duals of the elimination rules for conjunction, the elimination rule for disjunction is significantly more complicated that just a dual of the introduction for conjunction.1 What we have is essentially a case analysis—to eliminate an OR, we need to conduct two subproofs (nested as in the →-Intro rule), one for each possible case. Here is the rule, with holes for the bodies of the subproofs:
In words, this says that we have our disjunction, p∨q, which in this case comes from hypothesis h0 of the theorem, plus two nested subproofs. The first subproof needs to conclude the "result" proposition r from the additional premise p, while the second subproof must conclude the same result r from the alternate premise q. Since we know that either p or q is true at this point in the proof, we are able to conclude r regardless of which it is.
Here is a proof that OR is commutative (p∨q ⊢ q∨p):
We may think of True (⊤) as a conjunction of zero things: it is true whenever all of those (zero) things are true, i.e., it is always true. Compare this with taking the sum of an empty set of numbers: the result is 0, which is the identity for +, just as ⊤ is the identity for ∧. Using this analogy, we get one introduction rule for ⊤ (with zero premises) and zero elimination rules:
In words, we may conclude ⊤ at any time with no premises. This is not generally useful, but we include it for completeness.
Similarly, we may think of ⊥ as a disjunction of zero things, noting as above that ⊥ is the identity for ∨. It is false unless at least one of those zero things is true…. This suggests that we get zero introduction rules and one elimination rule, which just has the premise ⊥ and zero nested subproofs:
That is, if we have a proof of ⊥, then we can produce a proof of any arbitrary proposition r! Logicians like to refer to this as ex falso quodlibet, "from falsehood, anything." If your premises are consistent, you should never be able to prove ⊥ at the top level of a proof; if you could do that, then you could use this rule to prove anything whatsoever. This rule is useful in nested proofs (for example in disjunction elimination, doing a case analysis), where if a temporary assumption leads to a contradiction then we can conclude anything in that subproof, secure in the belief that that assumption will never actually be true.
Here is an example, where we validate the common argument that if we know that either p or q is true, and we know that p implies false, then q must actually be true:
Since the laws of Boolean algebra tell us that ¬p ≡ p→⊥, we could simply derive the rules for negation from those for implication, specialized to the conclusion ⊥. However, it is convenient to have rules explicitly to deal with negation. There is also one additional rule for negation that does not fit the pattern of the rest of the rules (see below).
Accordingly, here is the introduction rule for negation:
In words, this says that to prove ¬p, we show that the temporary assumption of p leads to a contradiction. That is, the inner proof, with an additional hypothesis h0 available to assert that p is true, is able to arrive at a proof of ⊥.
Similarly, here is the elimination rule for negation:
That is, one way to demonstrate a contradiction is to have proofs of both ¬p and p. Compare these rules to →-Intro and →-Elim, and confirm that they are just the special case of rules for p→q where q is ⊥.
Using these, here is a proof of one direction of the equivalence between p→q and its contrapositive ¬q → ¬p:
If you try to prove the other direction of this equivalence, you will have a surprisingly difficult time. In fact, it is possible to show that there is no proof of the argument ¬q → ¬p ⊢ p→q using the rules seen so far.2 The closest you will be able to get starting from the premise ¬q → ¬p is to conclude p → ¬¬q:
Although you may be tempted to just erase the double negation, in a formal proof you need to justify every step, and it turns out that we do not have any way yet to prove ¬¬q ⊢ q! Therefore, the very last rule we will add (apart from wrapping up some loose ends in the next section) is the rule of double negation elimination:
With this additional rule, we may finish the proof of the equivalence of the contrapositive:
As a convenience, once we have proven the validity of some argument p1, p2, … ⊢ q, we may reuse that proof in future proofs as if it were another deduction rule:
Note that we may perform any consistent substitution for the propositional variables in the argument. (In a real example, "My Theorem" would need to be a completed proof of a valid logical argument, but hopefully this gives the idea.)
As an example, here is a proof of the modus tollens law and the law of syllogism, followed by two examples of using them to prove an extended version of modus tollens:
In programming terms, using an already proven theorem like this is analogous to calling an already written function out of a library.
To apply all this to arguments stated in English, we have to introduce propositional variables to represent all the propositions in the argument. For example, consider:
John will be at the party if Mary is there and Bill is not there.
Mary will be at the party if it's on Friday or Saturday.
If Bill is at the party, Tom will be there.
Tom won't be at the party if it's on Friday.
The party is on Friday.
Therefore, John will be at the party.
Let j stand for "John will be at the party," m for "Mary will be there," b for "Bill will be there," t for "Tom will be there," f for "The party is on Friday," and s for "The party is on Saturday." Then this argument has the form
This is a valid argument, as the following proof shows: