[FOM] Use of Ex Falso Quodlibet (EFQ)

[Mario Carneiro]

By your description, if all n branches of the case proof give #, then the
result is #. Thus by a vacuous forall, in the n=0 case # is always the
conclusion. But the n=0 case input is a 0-ary disjunction, which is #. Thus
the 0-ary or-elimination is:

   #
____
    #

and so there is no EFQ recovery.

Mario

On Wed, Sep 2, 2015 at 2:45 PM, Tennant, Neil <tennant.9 at osu.edu> wrote:

> Paul Levy writes:
>
>     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.
>
> I must respectfully disagree. This is in error. If one were to frame n-ary
> or-elimination in Core Logic, it would be done graphically thus:
>
>                           __(i)  ...  __(i)
>                           A1          An
>                            :             :
>    A1v...An           B/#        B/#
>    _________________________(i)
>                          B/#
>
> where this is to be understood as follows:
> 1. if # is the conclusion of every case-proof (all n of them!), then the
> main conclusion is # ;
> 2. otherwise, the main conclusion is B .
>
> There is no case of n-ary or-elimination corresponding to n=0. What on
> earth would it look like?
>
> Neil Tennant
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150902/3feb5b1b/attachment-0001.html>