[FOM] The unbearable ghastliness of EFQ, and sundry other matters arising from Harvey's last post

[W.Taylor at math.canterbury.ac.nz]

Quoting "Timothy Y. Chow" <tchow at alum.mit.edu>:

> I haven't followed all the ins and outs of this particular discussion,
> but the debate seems to be turning on whether the following argument---
>
> Let b be arbitrary. Suppose b in {x|~x=x}. Then ~b=b. But b=b.
>     Contradiction. So, if b in {x|~x=x}, then b in A. QED
>
> ---employs the idea that "a contradiction yields everything."  I don't
> understand what Core Logic is, and I'm not sure I even understand what
> "a contradiction yields everything" means.  But I can give a data point
> as a mathematician introspecting on what he thinks he is doing when
> reasoning as above.  I think I am making an assumption, arriving at a
> contradiction, and then concluding that my assumption must be mistaken.
>  I am not, or at least am not consciously, thinking about "a
> contradiction yields everything."  Where is that step supposedly coming
> in?  I guess this is a question for Harvey.  Am I supposedly arriving
> at the contradiction, then making a further step that the contradiction
> yields everything, and then balking at accepting everything, and only
> then backtracking to my assumption to reject it?  It's not possible to
> balk at the contradiction itself and backtrack immediately?  We have to
> justify balking at the contradiction by appealing to its undesirable
> consequences, or something?
>
> Tim

I agree with everything Tim has said here, including my lack of understanding.

But it seems to me Tim has put his finger on a good point.

Ex falso quodlibet seems to say all cases of  "from p ^ ~p    deduce q";
and the empty set lemma seems merely to say   "from p -> q^~q deduce ~p".

The latter *seems* to be weaker, but I have no idea in which logics
either implies the other.   Is there a clear answer?

Bill Taylor



----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.