[FOM] EFQ and Faithful Formalization--Reply to Alan Weir

[Tennant, Neil]

Alan Weir is of the view that

"that version [i.e., the parallelized one] of &E seems to me definitely not to be implicit in ordinary practice."

I beg to differ. The first thing anyone does, when they have a conjunctive premise available, is break it down into its two conjuncts. Thus the problem

    .... P&Q .... ?- R

becomes the problem

    .... P , Q .... ?- R.

As soon as the latter is solved by means of a proof, a final step of parallelized &E then wraps it up. The parallelized rule can be applied when only P is used; when only Q is used; and when both P and Q are used (in the subproof).

"... Neil's algorithm for generating larger Core proofs out of smaller clearly isn't part of ordinary practice but simple linear chaining arguably is, ..."

Remember that I'm recommending formalizing any mathematical proof of an overall result X:A by providing core proofs for all the bits of informal proof *between* appeals to cut. Because of the metatheorem about computable reducts, one can then simply leave it at that, without actually performing any cuts with the formal proofs. If, however, one's interlocutor/audience insists on being given a core proof of the overall sequent X:A, it can be computed from the bits of core proof already in hand---just as one could compute a cut-free classical proof if for any reason one's audience didn't like seeing applications of cut in one's initial proof. Both the classical core logician and the orthodox classical logician face the same problem of blow-up here.

"Now take the informal EFQ-free empty set proof we looked at, ... 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."

[I think Alan intended to write "b in {x|~x=x}, b=b proves  A, for arbitrary A".]

Alan's appeal to Modus Ponendo Ponens (->E) with major premise

      b in {x|~x=x} -> A

makes that MPE a maximal occurrence, since it also stands as the conclusion of ->I. Upon determining the appropriate reduct, one ends up with a proof not of A, but of #. So EFQ has not been shown to be a derived rule.

Neil Tennant

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150911/d39156be/attachment-0001.html>