Implication Glossary
Definition
The implication or conditional connective 'IMP' results in a formula A IMP B which is true if and only if A is false or B is true. A is said to be its antecedent and B is its consequent.
Connecticves with similar truth conditions in natural languages are also taken to express implication. The word 'if' in English, taken in a truth-functional sense, is the intended analogue of the formal connective.
Comments
The role of the logical conditional is to make it possible to express potential inference: it gives us something to say where we know there is a valid way to reason from one proposition to another. For instance, 'If Timmy is a tiger, Timmy is a carnivore' tells us that we have enough background information (biological theory or whatever) to argue validly from the additional assumption that Timmy is a tiger to the conclusion that Timmy is a carnivore.
Conditionals in natural languages are quite complicated. Some of the more exotic kinds of conditional construction can usefully be treated in formal logic, but not in an introduction to the subject at this level.
The truth table is:
| IMP | 0 | 1 |
| 0 | 1 | 1 |
| 1 | 0 | 1 |
In the natural deduction calculus, the elimination rule for implication says that B is an immediate consequence of A and A IMP B. This consequence is also called detachment or modus ponens in the literature of logic.
The introduction rule for implication says that A IMP B is an immediate consequence of B, optionally discharging an assumption of A if B depends on it. Equivalently, we see A IMP B as an immediate consequence of a sub-derivation in which B is derived from A.
Examples
- 'If my pen is made of copper, it conducts electricity well' does not actually say whether my pen is a good conductor or not, but we can know the conditional is true because its consequent follows from its antecedent together with the physical fact that copper is a good conductor. In fact, my pen looks like copper because of its colour, but it is really made of plastic and is a poor conductor, so the truth-functional conditional is true because its antecedent is fase.
-
The following proof illustrates the rules for
implication:
SP {p IMP (q IMP r) ⊢ (s IMP q) IMP (p IMP (s IMP r))} PL {1} {1} {p IMP (q IMP r)} {A} PL {2} {2} {s IMP q} {A} PL {3} {3} {p} {A} PL {4} {4} {s} {A} PL {1,3} {5} {q IMP r} {1, 3 IMPE} PL {2,4} {6} {q} {2, 4 IMPE} PL {1,2,3,4} {7} {r} {5, 6 IMPE} PL {1,2,3} {8} {s IMP r} {7 [4] IMPI} PL {1,2} {9} {p IMP (s IMP r)} {8 [3] IMPI} PL {1} {10} {(s IMP q) IMP (p IMP (s IMP r))} {9 [2] IMPI} EP