EFQ

[Arnon Avron]

Just to clarify the situation:  It is well-known (and easily seen) that if one accepts the usual  ND rules for disjunction,
then EFQ is equivalent to the disjunctive syllogism (from -P and P\/Q infer Q)  as well
as to (MP) for the mathematical implication (from P and -P\/Q infer Q).  In either of these two forms,
EPQ is indespensible for mathematics in general and for its foundations in particular.

Arnon
________________________________
From: FOM <fom-bounces at cs.nyu.edu> on behalf of Lawrence Paulson <lp15 at cam.ac.uk>
Sent: Monday, May 16, 2022 6:02 PM
To: Tennant, Neil <tennant.9 at osu.edu>
Cc: fom at cs.nyu.edu <fom at cs.nyu.edu>
Subject: Re: Bourbaki and foundations

Dear Neil,

Perhaps more accurate word would be "admissible”. I wonder why beginners find it difficult. “Proof by contradiction” is simply double negation, so not relevant. The question is what happens if 1=0, and in any specific context (Peano arithmetic, ZF, lambda-calculus) deriving x=y is a trivial calculation, so the principle is a codification of that. Computationally it corresponds to type systems in which non-terminating computations can be assigned any type.

I guess it’s not a situation that mathematicians bump into every day, thank goodness!

Larry

> On 15 May 2022, at 22:57, Tennant, Neil <tennant.9 at osu.edu> wrote:
>
> Since EFQ (from absurdity infer any proposition you please) is typically taken to be a rule of inference, I take you to be claiming that EFQ is valid, rather than true. But EFQ is certainly not obviously valid. Beginners in formal find it highly counterintuitive. It’s also the main source of irrelevance. IMHO it’s a rule that students are just brainwashed into accepting.
> Moreover, mathematical and scientific deductive reasoning has no need for it at all.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220517/77f7aacd/attachment-0001.html>