Conjunction Propositional natural deduction
The simplest connective of all to grasp and to use is conjunction, 'AND'. This is intended to correspond to the English word 'and', as the latter is used in compounds like
Africa is hot and Greenland is cold
though the correspondence is in some ways not exact. In the first place, 'and', like its cognates in other Indo-European languages, does not only join sentences. As a result of the process sometimes called Chomsky-adjunction, it can join nouns, verbs, adjectives, etc.
| Jack and Jill went up the hill. | (joining proper nouns) |
| Dogs delight to bark and bite. | (joining verbs) |
| I'm ready and willing if you are. | (joining adjectives) |
It may also join adverbs or phrases of almost any kind. In the second place, these constructions may not always be straightforward Chomsky-adjunctions, since unpacking them into conjunctions of the form p AND q may give incorrect results. The second example above does indeed mean the same as
Dogs delight to bark and dogs delight to bite.
However, we cannot carry out a similar conversion on examples like
Chalk and cheese are different.
York is between London and Edinburgh.
Bob and Carol are married.
Tom, Dick and Harry carried a piano upstairs.
That Tom carried a piano upstairs is not true, and 'York is between London and York is between Edinburgh' is not even sense. In the third place, even where 'and' really is a connective, it may carry connotations which we want to ignore for the purposes of elementary logic. The pair
Joe found he had no friends and became a logician.
Joe became a logician and found he had no friends.
are not synonymous in English, for example, even though the very first trivial proof exercise we do is to prove p AND q logically equivalent to q AND p. In some cases compounds built up with the word 'and' depart even more radically from the logical paradigm:
One false move and I shoot!
for instance, is not a conjunction at all but a conditional.
For all that, 'and' is relatively well-behaved logically. The other connectives are in their various ways even harder to formalise adequately. We shall return to the problem of the mismatch between the formal symbols of logic and their natural language counterparts later. The formal rules for 'AND' are very simple and very intuitive. A conjunction p AND q carries exactly the force of its two conjuncts p and q taken together. What is said in an assertion of 'p and q' is just what is said by asserting p and also asserting q – the whole point of the connective is to combine two sentences into one without changing the meaning of asserting them. So we may validly infer the conjunction from the conjuncts and conversely. That is to say
p AND q entails p
p AND q entails q
p, q entail p AND q
For example, suppose that we are in a position to assert that Africa is hot, and that, perhaps for different reasons, we are also in a position to assert that Greenland is cold. Then we can combine the two and go on to assert that Africa is hot and Greenland is cold. Conversely, if we know that dogs delight to bark and bite, then we can infer (among other things) that they delight to bark. These primitive inferences are not supposed to be very exciting: they are intended to be as trivial and obvious as logic gets.
|
|
||||||||
|
|||||||||
These facts immediately give rise to the general rules for conjunction. Where A and B are any formulas, A is an immediate consequence of A AND B, and B is also an immediate consequence of A AND B. Conversely, A AND B is an immediate consequence of A and B (in either order). Hence, any derivation in which A AND B occurs may be extended in one step to become a derivation of A. The same goes for B. Moreover, given a derivation in which A and B occur on any two lines, we may extend in one step to give a derivation of A AND B.
In specifying the abstract rules of logic we shall follow standard practice in using a notation involving a horizontal line. The reading is that whenever formulae of the forms given above the line have been derived the rule lets us pass to the corresponding formula of the form given below the line. Thus in the case of conjunction we have the rules given abstractly in shortANDrules. The upper two of these, saying that we can pass from a conjunction to either of its conjuncts, are called AND-Elimination (abbreviated to ANDE) since the connective in question is eliminated or removed from the formula allowing us to get at its parts. The lower rule, with two input sequents, is called ANDI for AND-Introduction because by means of it the connective is introduced into the conclusion.
|
|
||||||||
|
|||||||||
In a derivation, some of the formulae may be assumptions on which a given later formula depends. The derivation records the validity of the corresponding sequent. In specifying the rules, we should really consider not only the effect on the formulae to which they apply, but also the assumptions on which the new conclusion depends. We can easily write out the rules "in full" as transformations on sequents (ANDrules) with the reading that whever sequents of the forms above the line have been proved, the rule immediately generates the corresponding sequent given below the line. Clearly the long and short versions of the rules say the same thing, but the long version says it more explicitly. ANDE does not change the stock of assumptions on which the formula depends, and ANDI merely collects up those of its inputs, so we shall generally prefer to write the conjuinction rules as in shortANDrules. For some other connectives, however, the longer, sequent-based versions will be more natural, so it is important to have that notation available as well.
SP {p AND q, r AND s ⊢ p AND s} PL {1} {1} {p AND q} {A} PL {2} {2} {r AND s} {A} PL {1} {3} {p} {1 ANDE} PL {2} {4} {s} {2 ANDE} PL {1,2} {5} {p AND s} {3, 4 ANDI} EPThere are many ways in which we might write proofs to make them easy to discover and to read. ANDproof shows a simple proof using the AND rules, written out in a linear format, with the sequence of formulae which constitute the derivation written in a vertical column. Each line of proof consists of a formula, to the left the line numbers of the assumptions on which it depends and to the right some annotation saying which rule was applied to get it. The lines are numbered for easy reference.
To get any derivation under way we must start by asserting its premises. The same applies to proofs: they all start with assumptions. The Rule of Assumptions is entirely straightforward:
At any stage of any proof, any formula at all may be introduced on a new line. Its assumption number is that very line number only (that is, it depends only on itself). 'α' subscripted with that very line number (that is, it depends only on itself). The annotation is the letter 'A'. the smallest positive integer not used in the proof so far (that is, the next number in sequence, starting from 1). 'α' subscripted with the smallest positive integer not used in the proof so far (that is, the next number in sequence, starting from 1). The annotation is the letter 'A'.
That is to say, you can assume anything you like for the sake of argument. Evidently the rule of assumptions on its own only allows us to prove sequents which are substitution instances of p ⊢ p. All such sequents are clearly valid but rather unexciting. To make logic more interesting we need rules governing the behaviour of various connectives. These will transform the trivially valid results of the rule of assumptions into non-trivially valid sequents, some of which may even be surprising.
Lines (1) and (2), then, are assumptions. Lines (3) and (4) record the inferences by ANDE whereby conjuncts are derived from the conjunctions on lines (1) and (2). Line (5) is where they are put together to make a new conjunction. The operation of the AND rules should be intuitively clear. Note how the assumption numbers on the left accumulate and are inherited by conclusions drawn from premises.
|
|||||||||||||||||||||||
treeProof shows the same proof
written out as a tree. The formulae are the same as in the
linear representation, but of course line numbers are not
required because the horizontal inference strokes connect
the formulae concerned. To obtain the assumptions on which
each formula depends, we must trace the inferences back up
to the leaves at the
top. ANDproof
and treeProof do not just show
two proofs which happen to be in some sense equivalent,
but one and the same proof. The difference is
purely one of superficial presentation.
Click
here to see it happen.