[FOM] From EFQ to Research 5--reply to Harvey Friedman (typo corrected)

[Joe Shipman]

Does any of this have any prospect of making it easier for mathematicians to prove theorems, either by providing more powerful or general proof techniques or by indicating where they need to bring in a new axiom?

-- JS

Sent from my iPhone

> On Sep 13, 2015, at 9:31 AM, Tennant, Neil <tennant.9 at osu.edu> wrote:
> 
> In 'From EFQ to Research 5', http://www.cs.nyu.edu/pipermail/fom/2015-September/019125.html, Harvey Friedman quotes himself as follows:
> 
> "...we have discussed
> 
> p, not p |- q
> p |- (not p arrows q)
> |- p implies (not p arrows q)
> |- (p and not p) implies q
> 
> The offered treatments of these four have all the trappings of a
> rhetorical point that is not responsive to what is going on in actual
> mathematical proofs."
> 
> I do not understand the phrase "trappings of a rhetorical point" in the context in question, which was one in which I had *informed* Harvey (as the main, and unfortunately uninformed, interlocutor) that:
> 
> In Core Logic we do NOT have   
> p, not p |- q;
> In Core Logic we DO have each of
> p |- (not p arrows q);
> |- p implies (not p arrows q); and
> |- (p and not p) implies q.
> 
> This is not rhetoric; these are just some important truths about deducibility in a particular formal system, whose merits or demerits for the formalization of mathematical reasoning are under consideration.
> 
> Harvey goes on to complain
> 
> "Neil fails to mention that the bidirectional Deduction Theorem is
> destroyed, which is probably considered by most to be far more
> egregious than any kind of irrelevance. Why doesn't Neil mention the
> crucial fact that the bidirectional Deduction Theorem is destroyed?"
> 
> Umm ... I didn't mention it in that particular discussion, I guess, because it was so darned OBVIOUS. How can any competent logician aver that a system that s/he is commending does NOT have
>    p, not p |- q
> but DOES have
>    p |- (not p arrows q)
> and NOT expect his/her audience to twig immediately that the much-celebrated Deduction Theorem must therefore fail in the direction
>    X |- P->Q   =>   X,P |- Q ??
> And this failure should then prompt further, deeper reflection on just what is supposedly so important in having the Deduction Theorem hold in this particular direction. Note that consistent X can imply P->Q for a choice of P inconsistent with X. So blind allegiance to, or insistence on, the Deduction Theorem holding in this particular direction would commit one to thinking that an arbitrarily chosen Q follows logically from inconsistent X,P. For sheer consistency in one's theoretical approach, the logician who is relevantizing at the level of the turnstile must avoid this commitment. The failure of the Deduction Theorem in this particular direction turns out to be both foundationally innocuous AND absolutely necessary in order to avoid irrelevance.
> 
> Harvey complains further that
> 
> "...when Neil was challenged to give a proof
> of "emptyset included in A" without use of EFQ[,] Neil just repeated the
> usual proof of this with EFQ."
> 
> This is a gross misrepresentation of what I did by supplying the Core Logical proof of "emptyset included in A". In that proof, it was evident how a suitably re-formulated rule of ->I accomplishes exactly what is needed, WITHOUT one's having to commit oneself to the rule of EFQ, stated all by itself, and meant to hold across the board. I pointed out that the move from a refutation of p to the conclusion p->q (thereby discharging p) is directly justified by the truth table for ->, and does not stand in need of any (highly implausible and counterintuitive) spiel about contradictions implying absolutely every proposition. So my core proof of "emptyset included in A" was not in any way a repetition of the usual proof that uses EFQ. 
> 
> I even went so far as to explain how it is that diehard supporters of the orthodox systems in which EFQ is stated as a completely separate rule of inference, meant to hold across the board, could have convinced themselves that they had to include EFQ in their system. It is because they are wedded to the unfortunately over-restricted but conventional formulations of two particular rules: ->I and vE. The conventional formulations have the following signal features:
> 
> ->I  You may infer A->B if you have a subordinate proof **of B**; and you may discharge the assumption A if you have used it in your subordinate proof of B
> 
> vE You may infer C from AvB if you have two subordinate (case-)proofs, one of C from A, and the other of C from B; and you may discharge these case assumptions when you apply this rule
> 
> Note that in these conventional formulations, due to Gentzen 1934-5, via Prawitz 1965, there is a fixation on having B as the actual conclusion of the subordinate proofs in question. But there is no need to specify the two rules ->I and vE in such a cramped way. One can instead *liberalize* both of them, in ways that are immediately and intuitively obvious, *without* having to appeal to EFQ. Just allow for the subordinate conclusion for ->I to be # (but make sure the assumption A has been used in the subordinate proof); and allow for one or more of the subordinate conclusions for vE to be # !
> 
> The surprising fact (proof-theoretic, not "rhetorical") is that just these two tweaks ensure that normal-form proofs are complete for logical consequence.
> 
> Neil Tennant
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150913/973a0e9d/attachment.html>