EFQ

[Tennant, Neil]

Arnon Avron writes:

"It is well-known (and easily seen) that if one accepts the usual ND rules for disjunction, then EFQ is equivalent to ... disjunctive syllogism  ... EFQ is ind[i]spens[a]ble for mathematics in general and for its foundations in particular."

This is all too swiftly dismissive of the possibility of having disjunctive syllogism without EFQ. The whole matter deserves more careful and better informed consideration. Allow me to explain.

The "usual" ND rule of v-Elimination was stated by Gentzen as follows:

                 __(i)   __(i)
                  A        B
                  :          :
      AvB     C        C
      _____________(i)
                 C

But v-Elimination can be liberalized as follows:

                 __(i)   __(i)
                  A        B
                  :         :
      AvB   #/C     #/C
      _____________(i)
                 #/C

Simply put: You may (of course) use the usual form (including the one where C is uniformly replaced by #); but, in addition: if either one of the two case-proofs ends with #, then you may bring down as the main conclusion the conclusion of the other case-proof.

This slight change to v-Elimination affords the following simple proof of disjunctive syllogism.

                          __(1)
                    ~A   A
                    ______   __(1)
           AvB       #          B
           _______________(1)
                        B

If one parallelizes all Elimination rules (which is easily done), and requires further that major premises of elimination stand proud with no non-trivial proof-work above them, then all proofs will be in normal form.

One can introduce one more liberalization, this time by furnishing a new part for the rule of ->-Intro:

Allow yourself to infer A->B as soon as you have a disproof of A
(that is, a proof of # that has A as an undischarged assumption).

One can avoid letting EFQ in through the back door by imposing a relevance requirement:

For ~-Introduction: Infer ~A from a proof of # that has A
as an undischarged assumption; and discharge A.
For Classical Reductio: Infer A from a proof of # that has ~A
as an undischarged assumption; and discharge ~A.

The resulting systems are Core Logic (without Classical Reductio) and Classical Core Logic (with Classical Reductio).

Cut is not a rule of either Core Logic or Classical Core Logic.  But it is admissible in the following form:

        There is a computable binary operation [_,_] on proofs such that
         if P1 is a proof of A from X, and P2 is a proof of B from
         X U {A}, then [P1,P2] is a proof of B or of # from some subset
         of (X U Y).

Note that EFQ (in the natural deduction system) is eschewed. And there is no derivation of EFQ (not even in Classical Core Logic).

One's natural deductions will in effect be isomorphic to cut-free, thinning-free sequent proofs. Such proofs suffice for all our deductive needs in mathematics and foundations.

All this was laid out in great detail in my book Core Logic (Oxford University Press, 2017).
My most recent contribution on this general topic is in The Philosophical Quarterly 2022
(https://doi.org/10.1093/pq/pqac001).

I have emphasized all the above logical points in journal publications dating back to the Proceedings of the Aristotelian Society 1979, where the liberalized rule of v-Elimination was first formulated.  I have written about having Disjunctive Syllogism without EFQ in my books Anti-Realism and Logic (OUP, 1987), Autologic (Edinburgh University Press, 1992), and The Taming of The True (OUP, 1997);  and in logic journals such as JSL, RSL, JPL, NDJFL, Studia Logica, Topoi, and Synthese.

The interested reader will be able to find downloadable PDFs at
u.osu.edu/tennant9/publications/

Neil Tennant




________________________________
From: Arnon Avron <aa at tauex.tau.ac.il>
Sent: Tuesday, May 17, 2022 2:55 AM
To: Lawrence Paulson <lp15 at cam.ac.uk>; Tennant, Neil <tennant.9 at osu.edu>
Cc: fom at cs.nyu.edu <fom at cs.nyu.edu>
Subject: EFQ

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 ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍

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/20220518/20f4850e/attachment-0001.html>