[FOM] Concerning EFQ and Cut

[Tennant, Neil]

Let me address Harvey's complaint (to the Core logician) that

"... the significance of what you are saying for
actual mathematical proofs is not at all apparent. The distinction you
seem to be making does not seem to reflect in the way mathematicians
write or think of proofs."

and enter once again my respectful disagreement.

Avron asked how the Core logician would prove the simple set-theoretical statement "the empty set is included in every set". I showed exactly how the Core logician would do this. Remarkably, Harvey ended up offering as the best possible *informal* proof a passage in logician's English that translates directly into a core proof. (That he did not see this seems, to me, to be evidence for the charitable hypothesis that he might be conflating Core Logic---for want of thorough familiarity with that system---with some other kind of really weird relevance logic that is clearly inappropriate for the faithful formalization of mathematical reasoning.)

We are going to carry on talking right past each other unless I enable my tenacious interlocutors to achieve a much clearer understanding of Core Logic than has been evident thus far in our exchange.

Here are some important points about Core Logic (and/or its classicized extension, Classical Core Logic).
(I'll make the points as though we are discussing constructive mathematics, and its formalizability in Core Logic. Completely analogous points would hold for classical mathematics, and its formalizability in Classical Core Logic.)

1. Core Logic, in its natural deduction formulation, has only introduction and elimination rules, *suitably formulated*. All elimination rules are in parallelized form, and in all applications of the elimination rules, their major premises stand proud, with no proof-work above them. There is no rule EFQ. Parallelization of the elimination rules, with the condition that MPEs stand proud, makes all proofs normal.
2. Core Logic, in its sequent calculus formulation, has only Left and Right logical rules, *suitably formulated*. The only structural rule is Reflexivity. So there is no rule of Cut, and there is no rule of Thinning.
3. Core natural deductions are isomorphic, in a rigorously definable sense, to the corresponding sequent proofs.
4. Just as Core natural deductions are in normal form, so too Core sequent proofs are cut-free and thinning-free.
5. Core Logic has enough transitivity of deduction to do everything that needs to be done. There is a computable binary operation [ , ] on core proofs such that: if P is a core proof of the sequent X:A, and P' is a core proof of the sequent A,Y:B, then [P,P'] is a core proof of X',Y':B or of X',Y':#, for some subsets X',Y' of X,Y respectively. More pithily: [P,P'] proves a subsequent of X,Y:B.
6. [Confining ourselves now to the natural deduction formulation:] The introduction and elimination rules are altered in slight but very subtle ways from the familiar rules in the Gentzen-Prawitz tradition. The rules ->I and vE are liberalized in the important ways described in earlier postings. These liberalizations enable one to *directly and faithfully* formalize simple moves that mathematicians make in their deductive reasoning (such as 'closing off a case' within a proof by cases when they have shown that the case-assumption leads to absurdity; or inferring "if A then B" immediately upon refuting A).
7. Core Logic is complete: if the sequent X:A is valid, then there is a core proof of some subsequent of X:A.
8. Thus: If A is a logical truth, then Core Logic proves A; if X is not satisfiable, then Core Logic proves X':#, for some subset X' of X; and if X is satisfiable and X:A is valid then Core Logic proves X':A, for some subset X' of X.

Core Logic does NOT 'allow EFQ in through the back door', or 'exploit EFQ in some tacit or hidden way'. That kind of criticism is completely ill-informed. For Core Logic satisfies a 'variable sharing' condition (or 'extralogical vocabulary sharing condition, at first order) that is more demanding than any that has been established, to date, for any competing relevance logic. This result can be found in

  1.  ‘The Relevance of Premises to Conclusions of Core Proofs’ [pdf]<https://u.osu.edu/tennant.9/files/2015/02/core_relevance_revised-11cnfkt.pdf>, Review of Symbolic Logic, 8, no. XXX, 2015, pp. XXX-XXX, DOI: http://dx.doi.org/10.1017/S1755020315000040

Now, let us return to Harvey's allegation

"... the significance of what you are saying for
actual mathematical proofs is not at all apparent. The distinction you
seem to be making does not seem to reflect in the way mathematicians
write or think of proofs."

Au contraire, it should (now, at least) be painfully apparent. What I am saying is that actual mathematical proofs can all be faithfully formalized in Core Logic, without any recourse to the irrelevance-inducing rule EFQ.

And the distinction I am seeking to make, between a system of constructive *and relevant* reasoning like Core Logic, and the better-known system of constructive but permissibly *irrelevant* reasoning called Intuitionistic Logic, is being made precisely because (I maintain) the former system perfectly reflects the way [constructive] mathematicians write or think of proofs.

Remember too that I said earlier that analogous points hold in the classical case:  the distinction I am seeking to make, between a system of non-constructive *and relevant* reasoning like Classical Core Logic, and the better-known system of non-constructive but permissibly *irrelevant* reasoning called Classical Logic, is being made precisely because (I maintain) the former system perfectly reflects the way [non-constructive] mathematicians write or think of proofs.

The Core systems AT LAST capture the essence of mathematical reasoning, which, intuitively---and pacete Avron and Harvey---NEVER trades on irrelevancies. It is simply in error to think that we have to have the *rule* EFQ in order to formalize what might look like the occasional exploitation of 'anything follows from a contradiction'. Those apparent exploitations can ALWAYS be regimented by using the liberalized rules of ->I and vE mentioned earlier. So the Core systems are free of this truly ghastly rule EFQ, which should never have been put into the canon in the first place. I think the only reason why it was (by Gentzen) is that he was hung up on having conclusions of case-proofs in proofs-by-cases be *equiform*, and on having ->I formulated as the usual rule of conditional proof that did not accommodate, as a primitive move, concluding A->B as soon as one has refuted A.

Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150903/309598d2/attachment-0001.html>