[FOM] Use of Ex Falso Quodlibet (EFQ) (or ECQ)

[Michael Lee Finney]

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.

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 am not
in a University environment, so I don't have access to articles that
require paid subscriptions.

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.

Ross presented R using a normal Hilbert axiomatization that can be
easily analyzed. Likewise for Ross Brady's more recent "Universal
Logic". To be fair, in that book Ross also shows the natural deduction
and Gentzen equivalents. It takes up far too much of his book and
doesn't actually contribute anything to the understanding or
development of his logic. Even so, those attempts stop short of
predicate logic because all of that work has to be redone for each
variation of the system. Natural deduction is not "plug-n-play".

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.
With substructural logics, you need to see every little "move" that
can be made and how each move interacts with other moves. One system I
am working with has over 30 axioms (before quantification is added).
None of them are surprising, but the fine detail allows me to break
principles down to their finest components and see what is happening.
Using a Hilbert axiomatization is like taking a microscope to the
structure.

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. It is virtually
impossible to even present those same proofs using "natural" deduction
without using an entire wall. Notation is essential in mathematics and
logic, and natural deduction is a step backwards by about 2000 years.

Michael Lee Finney

> The debate on EFQ (better, as Sara L. Uckelman said, 'ex
> contradictione quodlibet', ECQ) has been interesting, partly because
> it seems to show (unsurprisingly) that lots of the logicians
> commenting on the issue, though very familiar with non-classical 
> logic in the form of intuitionism, are much less familiar with, and
> have difficulty getting their heads round, substructural logics; in
> particular, logics in which structural principles such as
> transitivity of entailment (or derivability) are restricted. But  I
> think this in itself poses difficulties for Neil's desire to present
> his position as essentially non-revisionary. 
>
> Alan Weir,