[FOM] The unbearable ghastliness of EFQ, and sundry other matters arising from Harvey's last post

[Tennant, Neil]

Harvey says

"there ought to be a theorem to the effect that any proof of

"empty set is contained in A"

must have the idea that a contradiction yields everything. "

OK, try to find such a theorem. You won't. For there is the counterexample that "empty set is contained in A" is provable in Core Logic from the axioms of set theory that one would normally use, without Core Logic in any way "having the idea that a contradiction yields everything".  If one infers "if P then Q" immediately from a refutation of P, one is just 'doing the truth table' for arrow. The same holds if one infers "if P then Q" immediately upon proving Q, without even using P as an assumption. Truth table again.

No one is suggesting that mathematicians should 'change the way they write proofs'. Rather, I am simply pointing out that when logicians approach the task of rendering in excruciatingly minute formal detail, in proofs within their formal systems, what the mathematicians have accomplished, they can do so very naturally indeed in a system that allows no applications at all of EFQ.

"I wonder if Neil has connected with them [i.e. 'the MIZAR people'] about just this [i.e., EFQ]?"

No, I have not connected with the MIZAR people. My 1992 book Autologic laid the foundations of a case for Core Logic as the best system to use when automating constructive *and relevant* reasoning. If the MIZAR people were to study it, they might achieve considerable speed-up in proof-search.  :-)

"c times x

for integers c,x, does really depend on what c,x is. They are both
relevant --- EXCEPT when c is not 0. This is very much like EFQ to a
working mathematician."

No, it is not. Consider:

"P->Q

for sentences P,Q, does really depend on what P,Q is. They are both relevant --- EXCEPT when P is false or Q is true. This is not at all like EFQ to a working mathematician."

By the way, it ought to be pointed out that all this praise for 'working mathematicians' does rather idolize them. In all walks of life, there are practitioners who don't get things completely right. Doctors who give knee-jerk prescriptions for statins, for example. Dentists who put in mercury fillings. Nutritionists who tell one not to consume saturated fats. School principals who administer caning. The list goes on and on. Why should 'working mathematicians' be any different? Harvey does not always accord them such authority or reverence in foundational matters---witness his searing critiques [by which I am suitably impressed] of the lack of g.i.i. in what he calls 'core mathematics'!  (One begins to wonder whether perhaps the word 'core' has become a trigger for him.)

"A or (A implies B)
(A and not(A)) implies B

are "Ghastly"? "

I am happy to reassure Harvey that neither of these is ghastly. The first has a lovely proof in Classical Core Logic; the second likewise in Core Logic. Here they are:

                    (2)___         ___(1)
                        ~A           A
                        __________
                                 #
        __(2)              ____(1)
         A                   A->B
     ________     _________
     Av(A->B)        Av(A->B)
     ____________________(2)
                Av(A->B)


                     (1)___     _____(1)
                           A          ~A
    (2)_____        _________
         A&~A               #
         _______________(1)
                     #
           ____________(2)
             (A&~A) -> B



"You cannot prove any of

1+...+1 = 0 implies 1 = 0

for more than one plus sign."

Yes one can, in Core Logic.  There is the primitive rule (for arithmetic)

          t+1 = 0
         _______
               #


 So there is the proof

          _______________(1)
           ((1+1)+...)+1 = 0
           ________________
                        #
       ________________________(1)
       ((1+1)+...)+1 = 0  ->  1=0


"On the "cut" side of things, I think Neil is offering up a system with
no cut."

There is ample evidence for Harvey's being correct in thinking such a thing. It is emphasized explicitly in all my publications on Core Logic. That is, the system of Core Logic has no cut rule *in* the system itself. It does, however, satisfy Admissibility of Cut, in this sense:

     There is an effective binary operation [ , ] on core proofs such that
     for any core proof P of X:A, for any core proof P' of A,Y:B,
     [P,P'] is a core proof of some subsequent of X,Y:B.

One does not need an explicit cut rule as a rule *in* one's logical system in order to faithfully formalize mathematical reasoning. All one needs to be able to do is formalize the cut-free bits 'in between' the cut sentences involved, and rely on the foregoing metatheorem. (By the way, the Core logician manages all this without using Thinning either.)

There is a faint irony here. Suppose the orthodox logician formalizes a tract of mathematicial reasoning using N applications, overall, of the explicit cut rule. Then the Core Logician's formalization of the same tract of reasoning will involve N+1 core proofs (for the bits 'in between' the cuts) and will, overall, be N steps *shorter* than the orthodox logician's formalization!

No one ever asks the orthodox logician to actually eliminate cuts, by appeal to the cut-elimination theorem. For we all know about blow-up. The Core Logician should be cut the same slack (if you will excuse the pun), and not be required to actually compute [P,P'] for each and every appeal to the foregoing metatheorem.

The Core Logician and the orthodox logician are in exactly the same boat here. To stress the hyperexistential blow-up resulting from cut-elimination is to preach to the choir.

Neil  Tennant

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