[FOM] Use of Ex Falso Quodlibet (EFQ) (or ECQ)

[Alan Weir]

The debate on EFQ (better, as Sara L. Uckelman said, 'ex contradictione quodlibet', ECQ) has been interesting, partly because it seems to show (unsurprisingly) that lots of the logicians commenting on the issue, though very familiar with non-classical logic in the form of intuitionism, are much less familiar with, and have difficulty getting their heads round, substructural logics; in particular, logics in which structural principles such as transitivity of entailment (or derivability) are restricted. But I think this in itself poses difficulties for Neil's desire to present his position as essentially non-revisionary.

To pick up on Martin Davis's entertaining references to Bishop Berkeley (but leaving Hegel and Marx to one side!) the good Bishop maintained that in his views on the external world he was defending common sense by attacking metaphysical mis-readings of common sense by philosophers such as Locke. Likewise Neil seems to be arguing that his philosophical logic preserves the practice of working mathematicians, at least in best practice, whilst attacking distortions and misinterpretations of that practice by formal logicians.

Now let us suppose Neil is right about this as regards ECQ as an operational rule. I don't have very firm views on how to formalise correctly the informal 'triviality' examples which were given such as proving the empty set is a subset of any set because I think the relationship between informal and formal proof is a highly complex one and there may often by no unique right answer. But suppose it is perfectly legitimate to end up with a formalisation which, like Neil's, avoids use of ECQ

Suppose b in {x|~x=x}. Then ~b=b. But b=b. Contradiction. So, if b in {x|~x=x}, then b in A.

Thus the general non ECQ rule is

>From X,B |- # conclude X |- B -> A, for any A.

Now I think many of Neil's critics are saying, well so what, once you have that rule ECQ is very easily shown to be a derived rule, given B, ¬B |- # just apply modus ponens (or disjunctive syllogism given -> is material) on ¬B |- B -> A. This derived rule is thus, if not explicitly in actual practice, barely below the surface.

Neil's reply is that such chaining together of legitimate proofs does not yield a legitimate proof in Core logic because of the substructural normalizability restrictions. But it seems to me that the problem the reaction to this illustrates is that such transitive chaining is in fact deeply embedded in ordinary mathematical proof and to amend it is highly revisionary.

(Another potential source of confusion here is that 'transitivity' is not the same as 'Cut'. The latter is a rule of sequent systems not systems generally and moreover you can have Cut-Free sequent systems with transitive derivability built into the structural rules and non-transitive systems with a Cut rule.)

To put it another way, 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. Perhaps more feasibly, if there really does emerge a time when informal proofs are standardly written up in a form which can be processed for automated checking before being accepted in journals that would be a big revision in practice; but an additional revisionary move would be to design Core Logic automated provers and checkers and make them the sentinels for good journals.

I say all this as someone who, though having no problem with ECQ, as I think validity should be sharply separated from persuasive utility, is a proponent, like Neil, of restricting transitivity (albeit in a different way). But I am under no illusions but that this is revisionary not just of metatheoretic interpretation of mathematical practice, but of mathematical practice itself.

So to return to the Good Bishop, who most agree was a radical revisionary unlike, perhaps, Thomas Reid and the Scottish Philosophy of Common Sense, Neil is surely to be accounted as on the Irish, revisionary rather than the Scottish, irenic, side of this logical divide!

Alan Weir,

Roinn na Feallsanachd/Philosophy
Sgoil nan Daonnachdan/School of Humanities
Oilthigh Ghlaschu/University of Glasgow
GLASGOW G12 8QQ
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150906/8b3d93c7/attachment.html>