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 went crazy and became a logician.
Joe became a logician and went crazy.
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.
|: Rules for conjunction|
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. Hence, where X and Y are any sets of formulas, any derivation of A AND B from X may be extended in one step to become a derivation of A from X. The same goes for B. Moreover, given a derivation of A from X and a derivation of B from Y, we may put the two derivations together and extend in one step to give a derivation of A AND B from X ∪ Y.
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 sequents of the forms given above the line have been derived the rule lets us pass to the corresponding sequent of the form given below the line. Thus in the case of conjunction we have the rules given abstractly in ANDrules. 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.
|: Brief conjunction rules|
ANDE does not change the stock of assumptions on which the formula depends, and ANDI merely collects up those of its inputs, so we can help ourselves to some more easily readable notation by simply dropping all mention of the assumption side, leaving it to be understood. This results in the preferred formulation of the rules given in shortANDrules. The rules in this form precisely specify what is an immediate consequence in virtue of the conjunction connective: each conjunct is an immediate consequence of the conjunction, and conversely the conjunction is an immediate consequence of its two conjuncts.
ANDproof shows a simple proof using the AND rules, written out in the linear format. 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'.
|: Proof by ANDE and ANDI|
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.
: Another way to write
the same proof as in ANDproof
treeProof shows the same proof written out as a tree. The formulae are the same as in the linear representation, but of course the line numbers are gone, and are not required in the annotations 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 of the relevant subtrees.
It is important to note that ANDproof and treeProof do not just show two proofs which happen to be in some sense equivalent, but one and the same proof written in two formats. That is, the difference is purely one of superficial presentation.Click here to see it happen.