[FOM] EFQ and Faithful Formalization

[Alan Weir]

Neil Tennant writes in response to me:

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

I need to be sharper in my expressing my thoughts here. Neil also writes (FOM Vol 152 Issue 40):

>Logicians have simply been mistaken in thinking that the rule EFQ is needed for the faithful formalization of the deductive reasoning involved in either mathematics or the empirical testing of scientific theories.<

My thought was that Core Logic formalizations would not be ‘faithful’ to many classical proofs. Neil’s metatheorems establish that if we have a formalization of a classical proof of A from X then there is a proof in (classical) Core Logic, a logic in which EFQ is not a derived rule, of either absurdity or A, from a subset of X. And if we have another classical proof of B from A,Y then (focussing on the most important case, of X,Y being part of a consistent theory) there is a Core proof of B from a subset of X,Y. So I accept that there is a clear sense in which Core Logic requires no amendment of classical practice- you get (in the consistent case) the same conclusions from the same premisses, or even better, a proper subset thereof.

But two formalised proofs, each of the same conclusion from the same premisses, may differ radically in terms of faithfulness to an informal proof of that conclusion from those premisses. To take an extreme example: if there actually is a formal PA proof of Fermat’s Last Theorem there is a clear sense it will not be a faithful representation of Wiles’ proof, since the latter brings in content from branches of mathematics other than arithmetic.

EFQ/ECQ is a different case, though those who take a proof-theoretic view of the meaning of logical operators (if there is such a single thing) may hold it is not completely different in that they may claim a different content is expressed by negation in a system with EFQ than in one without. But at any rate there is the question of whether a given formalization captures a particular piece of  informal reasoning. This is a hugely complex question and I agree with Timothy Chow that the issue of revisionary or not will be, at best, a fuzzy one if it relies on whether formalization via this or that logic, e.g. Core Logic, is faithful to the original proofs.

I say ‘at best’ because of course some, such as Yehuda Rav, have argued that  there are principled reasons why the informal proofs which are currently the norm in mathematics cannot all be formalised. (To toot my own trumpet, I say something about this in a recent paper in the Review of Symbolic Logic).

Leaving that to one side, I wonder if Neil would sign up to this, or something close to it:

All (or the overwhelming majority) of good informal proofs are such that if they admit of formalization at all, they admit of a formalization in Core Logic which competent experts would agree is faithful to the informal proof.

Here competent experts would be people more than conversant with the relevant logics (which include not only relevant logics!) and who at least understand the informal proofs well- even better are recognised practitioners in the production of standard mathematical proofs. ‘Faithfulness’ might require some sort of isomorphism at a more gross level between the structure of the informal and the structure of the formal  proofs but that seems too exigent a requirement. One might require that the operational rules (if one can make sharp enough sense of the operational/structural distinction despite it being rather dependent on proof architecture) in the formal proof be discernible in the practice of the informal provers (even if perhaps not in the particular proof in question). And one might attempt a similar restriction for structural rules.

In these terms, I am suggesting that Core Logic will not represent faithfully mathematical practice for faithful formalisation will include the operational ECQ rule, or at any rate structural principles of unrestricted chaining forbidden in Core Logic (as applied there to its proper operational rules); I submit that the postings  of some members of FOM are evidence of this. But I admit it would be very difficult to get a compelling argument to that effect and some may think that the issue, involving notions such as ‘faithfulness’, is not well enough posed to be worth pursuing fruitfully.

Perhaps the  fruitful issue is just whether ECQ is valid even though not of persuasive utility. But of course in addressing that we run into a host of difficulties and dangers of talking at cross purposes too. Neil himself (in Review of Symbolic Logic 2012 ‘Cut for Classical Core Logic’) has said

>Some relevantists go so far as to say that it [EFQ] is invalid. I do not. To be sure, it is semantically or model-theoretically valid in both the intuitionistic and the classical senses. But its premises lack that relation of relevance that we wish to see between premises and conclusions<

and another OSU logician  Stewart Shapiro, in an excellent recent book ‘Varieties of Logic’, has argued that ‘consequence’ and ‘validity’ are polysemous or cluster concepts and  that questions as to whether e.g. negation has the same meaning in classical, intuitionist, paraconsistent etc mouths admit of no context-independent answer. Failure to appreciate this and adopt an eclectic approach to logic, he argues, leads to a lot of talking at cross purposes.

This perspective would help explain the impasse in the current debate. So too would the hypothesis (not actually incompatible with the first) that there is a (fairly) determinate fact as to whether Core Logic proofs faithfully formalize actual (best) mathematical practice but that the relationship between informal and formal proof is so complex it is very difficult, perhaps impossible, to get a definite answer. For many, even if the second hypothesis is right, that’s reason enough to abandon the question. But of course philosophers have been arguing inconclusively over certain issues, including logic, for over two and a half thousand years and for most of us the intractability of the questions only incites us to argue further, rather than shuts us up!

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150907/0415476b/attachment-0001.html>