[FOM] Fwd: A request

[Martin Davis]

---------- Forwarded message ----------
From: <aa at post.tau.ac.il>
Date: Thu, Sep 3, 2015 at 6:35 AM
Subject: Re: [FOM] Concerning EFQ and Cut [from Arnon Avon]

Quoting "Tennant, Neil" <tennant.9 at osu.edu>:

"The conditional-introduction signalled by "So" in the foregoing informal
proof would is formalized as an application of the formal rule that allows
one to infer "if P then Q" upon refuting P. And this formal rule in turn is
justified by the last two lines of the familiar truth table for the
conditional, which tell one that a conditional is true if its antecedent is
false."

If upon refuting P you can infer if P then Q", then in particular
(assuming that a logic should be structural) upon refuting
"not P and P" (which I hope you can) you are allowed to infer
"if (not P and P) then Q". If this move is forbidden in your system
then you  cannot truly say that you are formalizing ordinary mathematical
ways of proving things.

In fact, "If A and B then C" and "If A then if B then C" are
always equivalent in mathematical texts. It seems that for you
they are not. Don't you find it strange?

Arnon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150903/dbc6125a/attachment.html>