[FOM] Use of Ex Falso Quodlibet (EFQ)

[Mario Carneiro]

On Wed, Sep 2, 2015 at 11:08 PM, Tennant, Neil <tennant.9 at osu.edu> wrote:
>
> But that there so much as exists a case for n=0 baffles me. What is a
> disjunction with no disjuncts? I should imagine it is a
> passing-over-in-silence, because it cannot be said. But isn't that a very
> far cry from saying something absurd (#) ? And how would the B be obtained
> in the 'case proof' using no case-assumption at all?
>

The n-ary disjunction can be understood as the function f(x1,...,xn) which
satisfies

f(x1,x2) = x1 v x2
f(x1,...,xn,x(n+1)) = f(x1,...,xn) v x(n+1)

Plugging in n=1 to the second rule gives x1 v x2 = f(x1) v x2, so clearly
we want f(x1) = x1. Then considering the n=0 case we get x1 = f() v x1,
where f() is the 0-ary disjunction. It is a boolean function with no
arguments, so it is a constant, so it must be either the constant true or
false. But since true v x1 = true and false v x1 = x1, clearly only f() =
false will make the equation correct. Thus the 0-ary disjunction is
absurdity, which in Core Logic would be represented as #.

The description of n-ary or-elimination by Paul Levy:

                     [A_1]    [A_n]
                       :  ...   :
A1 or ... or A_n       B        B
------------------------------------
               B

is not suitable for Core Logic because there is no EFQ rule to deduce B
from #, so one does not have the ability to ensure that every branch gives
B, even those which yield absurdity. That's why Neil Tennant's description
has to explicitly account for B/# in the branches, and the way that this is
passed to the consequent, where the output is B only if some branch yields
B, ensure the "relevance" property because the B doesn't come from nowhere
like it does in EFQ, you can trace it back to one (or more) of the branches
of the disjunction.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150903/a9a2b69c/attachment-0001.html>