[FOM] Use of Ex Falso Quodlibet (EFQ) (or ECQ)--reply to Alan Weir

[Tennant, Neil]

There are two matters I would like to address in Alan Weir's characteristically insightful comments about EFQ/ECQ.

Alan writes

"... transitive chaining is in fact deeply embedded in ordinary mathematical proof and to amend it is highly revisionary."

I am not seeking to amend the practice of transitive chaining. All I am proposing is the labor-saving concentration on the task of formalizing *only the links* in the chains. This is because we have the metatheorem "for all core proofs P of X:A, for all core proofs P' of A,Y:B, there is an effectively determinable core proof [P,P'] of either A or # from some subset of X,Y." Mathematicians use sets of axioms whose consistency is presumed. So we have: "for all consistent (X union Y), for all core proofs P of X:A, for all core proofs P' of A,Y:B, there is an effectively determinable core proof [P,P'] of A from some subset of X,Y."

Alan also writes

"... if Neil actually convinced working mathematicians (say  by persuading them that the  epistemic gain, in spotting inconsistent systems, outweighed the additional time and effort) to go over their informal proofs and desist from sending them forward for publication if they suspected they could not be normalised according to Core Logic rules, that would be a major change in practice."

This is evidence of some misunderstanding of the status of Core Logic, and the reasons one might have for recommending it. I am not suggesting at all that mathematicians 'go over their informal proofs' in this way, let alone suggesting that they might find proofs of theirs that "could not be normalised according to Core Logic rules". My contention is that all sound/good/expert/non-fallacious constructive mathematical reasoning IS formalizable in Core Logic! And all sound/good/expert/non-fallacious non-constructive mathematical reasoning IS formalizable in Classical Core Logic!

My recommendation of Core Logic is aimed not at the mathematical experts who do the mathematics, but at the logicians who claim it as their task to provide formal systems that faithfully capture exactly what the mathematicians are doing.

There is some danger, of course, that a few brilliant and expert mathematicians are also brilliant logicians, but have absorbed and mastered orthodox logical systems at such a tender and impressionable age that they now see all that they do (as mathematicians) only through a certain logical lens, or within a certain systematic box. I am more than happy not to proselytize about Core Logic to them if they are not interested in opening that rather different box. In the western tradition, we all have Pandora as the big precedent.  :-)

My reason for being only too happy to live and let live is that there is a metatheorem of some interest that tells us that we might as well let them labor away to produce (if that is their fancy) rigorous formal regimentations of their informal proofs of their favorite mathematical (and metamathematical!) theorems, using (say) their preferred system of Classical Logic, EFQ-warts, cuts, and all.

Take their formal proof P of deep result #666 from the axioms of whatever theory (ZFC?) they have chosen. So P proves the sequent X:#666, where X is a set of ZFC axioms. P will of course contain many applications of the Cut rule. Chant rhythmically "Gen-tzen-ize! Gen-tzen-ize!". They, after all, worship this rule of Cut, this very rule that it was Gentzen's prime objective to show he did not need; for Gentzen showed that all applications of this rule could be eliminated from any proof containing them. Proof P, upon having its cuts eliminated by the hyptonized victim of your chants, is now the Cut-free proof P', of sequent X':#666, where X' is a subset of X. But P' will be bristling with Thinnings---all of them needed, upon elimination of all those Cuts, in order to make the logical moves legal according to the preferred formulation of the rules that prover of #666 has inherited from Gentzen. Now the aforementioned metatheorem kicks in: there is a linear-time algorithm for transforming P' into a Classical Core proof of #666 from (some subset of) X'.

Neither Cuts nor Thinnings are actually needed for the codification of mathematical practice. Cuts are simply attempts to register, as steps within proofs themselves, what we already understand from outside the system, as the Admissibility of Cut. And Thinnings are simply not needed, once one has suitably re-formulated the logical rules of inference governing the connectives. (By the way, *all* the changes in 'Core-ification' involve only the rules for the connectives. Gentzen got the rules for the quantifiers right.)

Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150907/a38be8fc/attachment.html>