[FOM] The terrible EFQ: reply to Tenant

[Martin Davis]

I wrote:

"Suppose one knows that A and ~B are true and wishes to prove C.  A
reductio ad absurdam proof might proceed by proving B from A and ~C.
The principle involved can be rendered:
                                 if A,~C |- B, then A,~B |- C
Then the special case B=A gives
                                           A,~A |- C
This shows that to eliminate EFQ one must interdict a simple special
case of an important general logical principle."

As part of a long reply, Neil Tenant wrote:

"Let us look at this more closely, but in the light of (MM). Martin's
special case involves uniformly substituting A for B; so B is atomic."

Neil evidently misunderstands me. These are not sequents. I'm not
"uniformly substituting" anything. I'm noting a common pattern of
proof used every day by working mathematicians. The letters A,B,C
stand for any mathematical statements in formal or informal discourse.
It would make a curious exception to say that A and B must be
different.

Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150905/6ff19e95/attachment.html>