[FOM] Use of Ex Falso Quodlibet (EFQ) (or ECQ)--reply to Michael Finney

[Tennant, Neil]

Michael Finney's singular email is quoted in chunks below, with my replies interpolated.

"I have been looking on the web have only found a few papers on the
"Core Logic" or "Core Classical Logic". Worse, what I have found are
entirely based on natural deduction and none of them define the
complete systems or their justifications."

Have you looked at any of the papers that can be downloaded from
http://u.osu.edu/tennant.9/publications/ ?
Articles 6, 7, 10 and 15 define Core Logic.
The rules need no justification; they are self-justifying.

"Can anyone point me to a basic paper (or web presentation) using
normal Hilbert axiomatizations of "Core Logic" and "Core Classical
Logic" (hopefully with justifications for the chosen axioms)?"

I very much hope not. So far, Core Logic has been presented only in natural deduction form, or in the form of a sequent calculus. (The two presentations are isomorphic, so there is little point in distinguishing them.) Anyone who ventured to besmirch Core Logic by formulating it as a Hilbert-style system would either need their heads read, or their ears boxed.

"I work with substructural logics and am willing to consider omitting
any specific axiom. Where I have a problem is when the details are
"hidden" by using "natural" deduction. One paper that I found
indicates that "Core Classical Logic" contains Ross Brady's system R.
But only in a diagram and does not indicate how it differs from R."

The system R that I refer to when writing about the relationship the Core Logic bears to other familiar systems is that of Anderson and Belnap, for their version of relevance logic. Since R is well known, and the rules for Core Logic are explicitly stated, the reader can easily work out how the two systems differ. Section 3.1 of article 6 at
http://u.osu.edu/tennant.9/publications/ has the heading 'Core proofs of some sequents not in the Anderson-Belnap system R or in system M of minimal logic', and Section 3.2 has the heading 'Core proofs for the axioms of R'.

"Natural deduction is not "plug-n-play"."

No, it's "plug-n-prove".

"With Hilbert axiomatizations, you can snap things in and out like Lego
blocks and see what happens, what is essential and where it is used.
With automation, you can track every single interaction and see what
is essential to a proof. It is not so easy with natural deduction."

Who says? I found matters to be precisely the reverse. (See my book Autologic.) Has it occurred to you that systems of natural deduction have been automated too?

"Using a Hilbert axiomatization is like taking a microscope to the
structure."

... and no doubt losing the big picture (about strategy in proof-search)?

"Frequently even the smallest theorems need over 50 steps in a Hilbert
system and a proof for a higher level concept might have 1000s of
steps. Those steps can be easily broken down and understood in a
Hilbert system. Not so in a natural deduction system."

Are you kidding?? The whole point of the natural deduction formulation of rules of inference is that they result from breaking steps down to their ultimately atomic forms. Each primitive rule focuses on but a single dominant operator (in a conclusion or a major premise).

I once heard Dana Scott quip that the proof of P->P in one of the Frege-Hilbert style systems (it might even have been the system for propositional logic in Russell & Whitehead's Principia Mathematica) took about 60 steps of substitution and detachment. It takes a single step in natural deduction.

Compare also the Hilbert-style system of Nicod for the Sheffer stroke. It has the single axiom

(p|(q|r))|((t|(t|t))|((s|q)|((p|s)|(p|s))))

and proves otherwise easy results only at the cost of horrible complications. Much more direct proofs can be obtained with the elegant natural deduction rules

        (i)___  ___(i)
             A   ,  B
                  :
                  #
               ____(i)
                A|B


          A    A|B    B
         __________
                  #                  for the constructive system; plus

                ____(i)
                 A|A
                   :
                   #
                 ___(i)
                   A                for the classical system


"It is virtually impossible to even present those same proofs using "natural" deduction
without using an entire wall."

But why would the natural deduction theorist bother with producing "those same proofs"---those unnecessarily long ones, that are made that long only because of the artificiality of the Hilbert-style formalization---as natural deductions? The natural deductions that s/he would be interested in obtaining would be the shorter, more elegant ones that one would find by using the rules of natural deduction!

"Notation is essential in mathematics and logic, and natural deduction is a step backwards by about 2000 years."

Words fail me. So I shall have to resort to just one symbol:  #.

Neil Tennant

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150908/0d5d0522/attachment.html>