[FOM] EFQ and Faithful Formalization

[Alan Weir]

Re Neil Tennant's reply  to me in FOM Vol. 153 Issue 35, I read his example of different proof lines in Gottlob's Nachlass- 'upwards'  and 'downwards'- as a matter of proof-searching heuristics or psychology of discovery not proof. (I take it the ref to B&C a typo: I do, though, agree that upwards falsity preservation is  as important to the notion of entailment as downward truth preservation though admitting of conflicting implementations. For these reasons and others- model theoretic versus modal versus proof theoretic explications of entailment, some of which have also emerged in this debate,  switching the EFQ discussion from informal proof and formalisation directly to 'what is entailment' will produce no greater consensus.)

And I didn't quite see how the different formalisations using parallel &E conformed to the differing strategies. But at any rate that version of &E seems to me definitely not to be implicit in ordinary practice. Is EFQ? One can read the postings of Harvey Friedman and the first one of Timothy Chow as suggesting opposite answers. Let's suppose it isn't. But modus ponens, as a one step rule, does seem to me to be part of ordinary practice, at least mathematical practice, which Vann McGee's counterexamples don't seem to touch.
What of structural rules? Again Neil's algorithm for generating larger Core proofs out of smaller clearly isn't part of ordinary practice but simple linear chaining arguably is, and the tree-form Gentzen-Prawitz natural deduction proof-architecture, which Neil taught me to know and love a long time ago, could also be claimed to be (notwithstanding the proclivity for exploding across the page lately alluded to), not too great a distortion of ordinary practice (unlike multiple conclusion systems- not that I take any of these as reasons not to use such systems in proof theory).

Now take the informal EFQ-free empty set proof we looked at, what seems a long time ago, amended to give an arbitrary consequent (easily done anyway if set A is {x:A}

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

Continue as follows:

>But we are supposing b in {x|~x=x}. Hence, by MPP, A<

We can formalise that, with the studied ignorance of normalisation which is part of everyday practice, to produce a demonstration that

b in {x|~x=x}, ~b=b proves  A, for arbitrary A

and with suitable variations similarly show that EFQ is a derived rule of operational rules and structural rules which I suggest are part of ordinary mathematical practice.

That is my main reason for thinking that claiming that EFQ is ghastly, more importantly claiming that it is irrational to use it (would Neil go that far?) involves revising ordinary practice. It's a revision I don't see a need to follow, unlike some others.

If, in the course of a proof, I arrive at a contradiction from the assumptions in play at the time, then if these assumptions are all part of a theory I uphold, it would be rational of me to go over the proof carefully and, if still convinced, take steps to amend my beliefs. But if, as may well be the case, there are additional assumptions in play, ‘for the sake of argument', I see nothing irrational in applying a one step move of EFQ if I think it will help me get where I want to go in the proof.

None of this is to say that Core Logic, classical and intuitionistic, is not of great interest as a proof system in its own right as well as for its inter-relations with other logics and that it may not be of high instrumental value, for computational logicians, for designing a robust relevance logic to use with data bases (which are often inconsistent, but which we don't want to throw up arbitrary garbage) and so on.

I'm not sure how to respond to Tim's points about what counts as faithful formalisation and which touch on the complexity of actual mathematical practice, need to think on that further!

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/20150910/8b1a14d2/attachment.html>