7.1: Derived Rules

This section begins with a somewhat strange example. We will first follow our noses in putting together a derivation using the strategies I have recommended. When we are done, we will notice that some of the steps, although perfectly corn, do no real work for us. We will then find interesting ways to avoid the superfluous steps and to formulate in a general way some methods for making derivations easier.

Let's derive 'A⊃(B⊃C)' from '(A⊃B)⊃C'. Our derivation must begin like this:

1 | (A⊃B)⊃C P
| ?
| ?
| A⊃(B⊃C)

We will pursue the obvious strategy of getting the conclusion by constructing a subderivation from the assumption of 'A' to 'B⊃C' as conclusion:

1 | (A⊃B)⊃C P
2 | | A A
| | ?
| | ?
| | B⊃C
| A⊃(B⊃C) ⊃I

We have reduced our task to that of deriving 'B⊃C' from 'A', w can use the outer derivation's premise. But how are we going to do that?

The target conclusion we now need to derive, 'B⊃C', is itself a conditional. So let's try setting up a sub-subderivation with 'B' as assumption from which we are going to try to derive 'C'. We are shooting for a derivation which looks like this:

1 | (A⊃B)⊃C P
2 | | A A
| | | B A
| | | ?
| | | ?
| | | C
| | B⊃C ⊃I
| A⊃(B⊃C) ⊃I

How are we going to squeeze 'C' out of 'B'? We have not yet used our premise, and we notice that the consequence of the premise is just the needed sentence 'C'. If only we could also get the antecedent of the premise, 'A⊃B', in the sub-sub-derivation, we could use that and the premise to get 'C' by ⊃E.

It might look rough for getting 'A⊃B' into the sub-sub-derivation, but once you see how to do it, it's not hard. What we want is 'A⊃B', which, again, is a conditional. So we will have to start a sub-sub-sub-derivation with 'A' as assumption where we will try to get 'B' as a conclusion. But that's easy because this sub-sub-sub-derivation is a subderivation of the derivation with 'B' as its assumption. So all we have to do is reiterate 'B' in our sub-sub-sub-derivation.

If this is a little confusing, follow it in the completed derivation below, rereading the text if necessary to see clearly the thought process which leads me along step by step:

1 | (A⊃B)⊃C P
2 | | A A
3 | | | B A
4 | | | (A⊃B)⊃C 1, R
5 | | | | A A
6 | | | 4| B 3, R
7 | | | A⊃B 5-6, ⊃I
8 | | 3 | C 4, 7, ⊃E
9 | 2 | B⊃C 3-8, ⊃I
10 | A⊃(B⊃C) 2-9 , ⊃I

I've carefully gone through this example for you because I wanted to illustrate again our strategies for constructing derivations. In this case, though, we have produced a derivation which, while perfectly correct, has an odd feature. Notice that I got 'B' in step 6 by just reiterating it. I never used :he assumption, 'A'! In just the same way, I never used the assumption of 'A' on line 2 in deriving 'B>C' in line 9. The fact that 'A' was assumed (twice no less!), but never used, in no way shows anything technically wrong with the derivation. Any derivation correctly formed, as this one is, following the rules, counts as correct even if it turns out that parts were not used. No one ever said that a line, either an assumption or a conclusion, has to be used.

I should refine what I just said: The assumptions of 'A', both in line 2 and in line 5, were not used in deriving the target conclusions of the subderivations in which 'A' was assumed. But we had to assume 'A' in both cases to permit us to apply ⊃I to introduce a conditional with 'A' as - the antecedent. However, if in subderivation 2 the assumption 'A' was never used in deriving 'B⊃C', you would suspect that we could derive not just 'A⊃(B⊃C)' but the stronger conclusion 'B⊃C' from the original premise. And, indeed, we can do just that:

1 | (A⊃B)⊃C P
2 | | B A
3 | | | (A⊃B)⊃C 1, R
4 | | | | A A
5 | | | | B 2, R
6 | | A⊃B 4, 5, ⊃I
7 | | C 3, 6, ⊃E
8 | B⊃C 2-7, ⊃I

Now we notice that we could have worked the original problem in a different way. We could have first derived 'B⊃C', as I have just done. Then we could have modified this derivaton by inserting the subderivation beginning with 'A', the subderivation 2 in the previous derivation, and then applying ⊃I. In other words, if we can derive 'B⊃C', we can always derive 'A⊃(B⊃C)' by simply assuming 'A', deriving 'BX' by whatever means we used before, and then applying >I. In fact, we can organize things most clearly by separating the two steps. First derive 'B⊃C', then create a subderivation with assumption 'A' and conclusion 'B⊃C' obtained by reiterating 'B⊃C' from above. Then apply ⊃I. The relevant parts of the total derivation, beginning with the previously derived conclusion, 'B⊃C', will look like this:

| .
| .
| .
| B⊃C
| | A A
| | B⊃C R
| A⊃(B⊃C) ⊃I

We have just discovered something extremely interesting: Nothing in the above line of thought turns on the two sentences involved being 'B⊃C' and 'A'. This procedure will work for any old sentences X and Y. For any sentences X and Y, if we can derive Y, we can always extend the derivation to a new derivation with conclusion X⊃Y. If

| .
| .
| .
| Y

stands for the part of the derivation in which we derive Y, the new derivation will look like this:

| .
| .
| .
| Y
| | X A
| | Y R
| X⊃Y ⊃I

Because X and Y can be any sentences at all, we can express the fact we have just discovered as a "new" rule of inference:

| Y
| X⊃ Y Weakening (W)

In other words, if any sentence, Y, appears in a derivation, you are licensed to write X⊃Y anywhere below, using any sentence you like for X. This rule of inference is not really new (that's why a moment ago I put quotes around the word "new"). If we want to, we can always dispense with the weakening rule and use our original rules instead. Wherever we have used the weakening rule, we can always fill in the steps as shown above by assuming X, reiterating Y, and applying ⊃I.
Dispensable, shortcut rules like weakening will prove to be extraordinarily useful. We call them Derived Rules.

A Derived Rule is a rule of inference which can always be replaced by some combination of applications of the original rules of inference. The original rules are called the Primitive Rules of inference.

A proof of a derived rule is a demonstration which shows how the derived rule may be systematically replaced by application of the primitive rules of inference.

The weakening rule is proved in the schematic derivation which you saw immediately above.

By using the derived weakening rule, we can immensely simplify the derivation we have been studying in this section. For we can use weakening instead of both of the subderivations which start from 'A' as an assumption. In addition to the use of weakening which we have already i seen, we can use it in the subderivation which begins by assuming 'B'. Given 'B' as an assumption, weakening immediately licenses us to write 1 'A⊃B', which we need for applying ⊃E.

1 | (A⊃B)⊃C P
2 | | B A
3 | | | (A⊃B)⊃C 1, R
4 | | | A⊃B 2, W
5 | | | C 3, 4, ⊃E
6 | B⊃C 2-5, ⊃I
7 | A⊃(B⊃C) 6, W

Isn't that easy!
{"ft_lang_label":"__label__en","ft_lang_prob":0.9500561,"math_prob":0.697568,"size":6916,"snap":"2019-43-2019-47","text_gpt3_token_len":2124,"char_repetition_ratio":0.14800347,"word_repetition_ratio":0.07111437,"special_character_ratio":0.27515906,"punctuation_ratio":0.11237458,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9859484,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-10-23T09:19:29Z\",\"WARC-Record-ID\":\"<urn:uuid:1a81d215-d6fd-4766-8776-92b8e4e0d826>\",\"Content-Length\":\"79817\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:4e14e3ea-9634-4550-9888-de287df9850e>\",\"WARC-Concurrent-To\":\"<urn:uuid:bcedc645-93e9-440d-94d8-1878fac5a430>\",\"WARC-IP-Address\":\"35.168.122.151\",\"WARC-Target-URI\":\"https://human.libretexts.org/Bookshelves/Philosophy/Map%3A_A_Modern_Formal_Logic_Primer_(Teller)/Volume_I%3A_Sentence_Logic/7%3A_Natural_Deduction_for_Sentence_Logic_-_Derived_Rules_and_Derivations_without_Premises/7.1%3A_Derived_Rules\",\"WARC-Payload-Digest\":\"sha1:TJ66CZTMVVTCDNWZE24IDTKVN6P4QJ33\",\"WARC-Block-Digest\":\"sha1:JT76CQIA64YYYZNERKRTK46DJ47BN4FX\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-43/CC-MAIN-2019-43_segments_1570987829507.97_warc_CC-MAIN-20191023071040-20191023094540-00496.warc.gz\"}"}