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

[Timothy Y. Chow]

> From: Harvey Friedman <hmflogic at gmail.com>
Harvey Friedman wrote:

> The only proof you have offered of this "empty set contained in A" in 
> ordinary mathematical language read virtually identically to the usual 
> proof with explosion (EFQ), and so I still haven't seen any proof of 
> "empty set contained in A" that isn't obviously based on the idea that a 
> contradiction yields everything. I said that if I see such a thing, I 
> will revisit this whole matter.

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