[FOM] Use of Ex Falso Quodlibet (EFQ)

[Paul B Levy]

> Date: Mon, 31 Aug 2015 12:36:09 +0000
> From: "Tennant, Neil" <tennant.9 at osu.edu>
> To: "fom at cs.nyu.edu" <fom at cs.nyu.edu>
> Cc: "Friedman, Harvey M." <hmflogic at gmail.com>, "aa at tau.ac.il"
> 	<aa at tau.ac.il>
> Subject: [FOM] Use of ex falso quodlibet (EFQ)
> Message-ID:
> 	<3188F1ACFDF24246BE3EB20656F10C5D5176108F at CIO-TNC-D2MBX04.osuad.osu.edu>
> 	
> Content-Type: text/plain; charset="iso-8859-1"
> 
> Arnon Avron writes
> 
> ____
> I have always thought that  mathematicians (NEED TO) USE  [EFQ], e.g.,
> when they claim that the empty set is a subset of any other set.
> Do you have another logical explanation of this claim
> on the basis of the standard definitions of the empty set
> and the subset relation?
> _____
> 
> The Core logician has a reassuring answer to this question (and all others like it).
> I described in an earlier posting how Core Logic liberalizes the rule of v-Elimination, so as to avoid the need for EFQ within either of the case proofs. There is only one other rule that needs to be liberalized in a similar fashion, and this is the rule of ->Introduction (a.k.a. Conditional Proof). The truth table for -> tells use that if A is False, then A->B is True. So the following step of inference is permitted as PRIMITIVE in Core Logic:
> 
> ___(i)

Or-elimination may be seen as the special case n=2 of n-ary
or-elimination.  The case n=0 is EFQ.  I can think of no philosophical
or ideological reason for accepting n=2 but rejecting n=0.

Paul



-- 
Paul Blain Levy
School of Computer Science, University of Birmingham
http://www.cs.bham.ac.uk/~pbl