Implication Propositional natural deduction

The next connective to be introduced is the conditional 'IMP'. As noted earlier, this is intended to be read 'if. . . then. . .'. Conditional constructions and related ones such as wh- clauses are rather complex in natural languages and their meanings are the subject of debate in linguistics and philosophy. For our purposes, however, the important use of the locution is to signify a plain sort of implication between the two embedded statements. To get a grip on this notion, consider an instance in which you might assert a conditional and give reasons for it.

A:   If Timmy is a tiger, Timmy is a carnivore.
B:   Why?
A:   Because all tigers are carnivores.

What is going on in this deathless passage of dialogue? There is an appeal to a simple argument

All tigers are carnivores
Therefore, if Timmy is a tiger then Timmy is a carnivore

and this argument is valid. It is valid because of its relationship to another valid argument

All tigers are carnivores
Timmy is a tiger
Therefore Timmy is a carnivore

which is of a valid form as already discussed in the Introduction. The relationship consists in this: a premise entails a conditional iff by putting it together with the left side we can validly get the right side. That is, in the example, by taking 'Timmy is a tiger' as an extra premise we give ourselves enough to entail 'Timmy is a carnivore'. The left side of a conditional is called its antecedent and the right side its consequent. So the fundamental principle underlying conditionals in logic is this:

I.e. if and only if

A conditional follows from premises X iff its consequent follows from X and its antecedent taken together.

To put it another way, what makes 'If p then q' true is that q follows logically from p together, perhaps, with some truths. This account of the truth conditions for conditionals has two parts. Firstly, if you are in a position to assert p IMP q then you are in a position to argue from p to q. This is obvious, for you are in a position to use the clearly valid inference

p IMP q, p therefore q

Secondly, if there is available enough collateral information to enable you to deduce q from p then you may correctly assert p IMP q.

Given the suggested account of conditionals, we should expect a formal logic which deals with the connective 'IMP' intended as 'if. . . then' or 'implies' to satisfy the condition that for any formulas A and B and for any set X of assumptions

X ⊢ A IMP B   iff   X, A ⊢ B

This is the Deduction Equivalence and lies at the heart of logic as we are doing it. Its importance is that it ties the connective IMP to the relation of deducibility, giving us a way to speak inside our (formalised) language about what follows from what; and the question of what follows from what is the very stuff of logic. The meaning of valid inference is that if the premises hold then so does the conclusion, so this close tie between the connective and the relation is to be expected.

:   Rules for implication

	X, A  ⊢  B IMPI X  ⊢  A IMP B
	X  ⊢  A Y  ⊢  A IMP B IMPE X, Y  ⊢  B

The Deduction Equivalence quickly gives rise to the introduction and elimination rules for 'IMP' in the formal system. IMPrules gives the formal specifications. It should be evident that IMPI is just half of the Deduction Equivalence, while IMPE is the formal realisation of the "clearly valid inference" used above to make the other half of the Deduction Equivalence look plausible.

The two rules governing conditionals go by several names in the literature. IMPI is called conditional proof by several authors including Lemmon Lemmon. IMPE is often called detachment, or goes by its Latin name modus ponendo ponens or modus ponens for short.

Notice that IMPI is unlike the other rules introduced so far in that the conclusion A IMP B depends only on assumptions X, whereas the premise B depends on A as well. That is, one of the assumptions has been removed in the step from the top line to the bottom line: the A is no longer an assumption but has become the antecedent of the conditional, as it has been discharged by the application of IMPI. In terms of the definition of compound derivation, the conditional A IMP B is an immediate consequence of a subderivation of B from A. Our notations for writing proofs need ways to represent such things. An example to illustrate the techniques will be more useful than a verbal definition.

SP {p ⊢ (q IMP r) IMP (q IMP (p AND r))} PL {1} {1} {p} {A} PL {2} {2} {q IMP r} {A} PL {3} {3} {q} {A} PL {2,3} {4} {r} {2, 3 IMPE} PL {1,2,3} {5} {p AND r} {1, 4 ANDI} PL {1,2} {6} {q IMP (p AND r)} {5 [3] IMPI} PL {1} {7} {(q IMP r) IMP (q IMP (p AND r))} {6 [2] IMPI} EP

:   Proof by IMPE and IMPI

Examine the application of IMPI at line (7) in IMPproof. Note that the number 2 "α₂" is the assumption number which has disappeared from the left side of line 6 in the passage to line 7. Every time an assumption is discharged like this it is given a mention in the annotation column. We bracket it to show that this is a discharge, not a citation of a line from which the conditional follows. Now look at the application of IMPI at line 6. In terms of the abstract statement of IMPI in IMPrules, X is the pair of assumptions 1 and 2, α₁ and α₂, while A is the formula q (assumption 3), (assumption α₃), and B is p AND r. With these identifications, make sure we do have an application of the rule as formally stated.

An application of IMPI does not usually just "happen", as those of IMPE or ANDI sometimes do. It has to be set up by prior assumption of the antecedent of the desired conditional. Where several IMPI steps are needed the process is iterated, as in the proof in IMPproof. Here the desired conclusion is a conditional, so at line (2) we assume its antecedent. We are then trying to get its consequent q IMP (p AND r) so that IMPI can apply. That is, the sub-goal is to derive the sequent

p, q IMP r   ⊢   q IMP (p AND r)

which we achieve at line (6). The new conclusion (the consequent of the old one) is in turn a conditional, so we assume its antecedent q and aim for its consequent p AND r from the three assumptions now in play. That is, the new sub-goal is

p, q IMP r, q   ⊢   p AND r

which is derived at line (5) by a couple of easy moves.

Click here to see the proof constructed.

:   Proof by IMPE and IMPI, tree notation

[q IMP r]2 [q]1 IMPE p r ANDI p AND r IMPI(1) q IMP (p AND r) IMPI(2) (q IMP r) IMP (q IMP (p AND r))

treeProof shows the same proof written out in the form of a tree. Here when we discharge an assumption we bracket it off and add an index number to show which rule application resulted in the discharge. The diagram represents the sequent whose conclusion is the formula on the last line and whose premises are the undischarged assumptions. This makes sense: when an assumption has been discharged, that closes off the sub-derivation stemming from it: the discharged assumption is not part of the main derivation. As before, the appearance of the derivation as a tree is different from its appearance in the linear format, but it is the same derivation nonetheless.

The tree format makes the overall structure of the proof clear, whereas the linear format tends to obscure it by putting everything in one column. However, drawing the trees becomes inconvenient as proofs get more complicated, as they tend to become too wide to fit on the page.

: The same proof, indented notation

Yet another notation is shown in fitch where the sequence of proof lines in the linear style is decorated with explicit indentation to show which parts of it constitute sub-proofs. In each indented section, the formula or formulae above the horizontal line are assumptions, and the rest are derived as shown. This has the advantage that it is easy to see the sub-proofs as separate objects. Thus it displays each column as a compound derivation with the indented sub-derivations among the objects in it. However, it has the disadvantage that it is relatively hard to see precisely which assumptions a given formula depends upon (this will be important later) and also that it may require work to be repeated where sections of the proof are the same in different sub-proofs.

In the remainder of these notes, proofs will generally be written in the manner of IMPproof, with assumptions listed on the left of each line. This is partly for typographical convenience, but more importantly because proofs written in that notation can easily be amended to give different systems of logic when we come to consider those in Chapter 8. Nothing deep turns on the choice of notation for proofs, however. In fact, it is good to become familiar with more than one notation and to be able to translate back and forth between them.

You should now go through a number of sample proofs using the rules for implication and conjunction. It is most important that you understand what you are doing in the IMPI strategy, as much of the rest of the system is obtained by building more elaborate constructions onto that foundation. If you find the whole thing obscure at this point, stop and go through the above explanations again, and talk to your tutor if that seems helpful, rather than rushing on.