FOM: relevance and v-Elim

[Neil Tennant]

This is in reply to Jon's comments on v-Elimination. I think I had
made exactly his point already, by recommending "(d) liberalizing
slightly the rule of v-Elim (proof by cases) so that if one case leads
to absurdity then the conclusion of the other case can be brought down
as the main conclusion".

Perhaps it would have been better to state the new natural deduction
rule of v-Elim graphically. It would be like this:

		__(i)	__(i)
		A	B
		:	:
	AvB    C/#     C/#
	__________________(i)
	       C/#

	where in each subordinate case proof the indicated assumption
	has really been used, so is available for discharge.

Here I use # for the absurdity symbol. It does not occur as a
subformula.  Its only role is in proofs. It comes into the picture
only via applications of negation elimination:

	A	~A
	__________
	    #
  
The rule of v-Elim as stated above is a portmanteaux scheme for four
kinds of application:


		__(i)	__(i)
		A	B
		:	:
	AvB     C       C	where C is a sentence, not #
	__________________(i)
	        C


		__(i)	__(i)
		A	B
		:	:
	AvB     #       #
	__________________(i)
	        #


		__(i)	__(i)
		A	B
		:	:
	AvB     C       #
	__________________(i)
	        C


		__(i)	__(i)
		A	B
		:	:
	AvB     #       C
	__________________(i)
	        C

These last two cases are of the sort that Jon had in mind. In the last
one, for example, you explore case A and find that it leads to
absurdity. So you immediately transfer your attention to case B, which
you find leads to your desired conclusion C. So you bring down C as
your main conclusion of a proof by cases.

Liberalizing v-Elim in this way means that you don't have to keep
applying the absurdity rule to 'fake' a derivation of C within a
case-proof that actually ends with #. Thus you can prove disjunctive
syllogism as follows:

		__(1)
		A	~A 	
		__________	__(1)
 	AvB	    #		B
	__________________________(1)
		    B

Obviously by iterating applications of the new rule of v-Elim you can
achieve exactly what a mathematician does when disregarding those
cases among A1,...,An that lead to absurdity, finding that in all the
other cases you can derive B, and thus concluding that B follows from
A1v...vAn.

Neil Tennant