[FOM] Use of ex falso quodlibet (EFQ)

[Tennant, Neil]

Arnon Avron writes

____
I have always thought that  mathematicians (NEED TO) USE  [EFQ], e.g.,
when they claim that the empty set is a subset of any other set.
Do you have another logical explanation of this claim
on the basis of the standard definitions of the empty set
and the subset relation?
_____

The Core logician has a reassuring answer to this question (and all others like it).
I described in an earlier posting how Core Logic liberalizes the rule of v-Elimination, so as to avoid the need for EFQ within either of the case proofs. There is only one other rule that needs to be liberalized in a similar fashion, and this is the rule of ->Introduction (a.k.a. Conditional Proof). The truth table for -> tells use that if A is False, then A->B is True. So the following step of inference is permitted as PRIMITIVE in Core Logic:

___(i)
         A
          :
         #
     _______(i)
      A->B

as are the more familiar steps


        B
     _______(i)  [no use made of assumption A]
      A->B

and

      ___(i)
       A
        :
       B
   _______(i)
     A->B

Allowing one to directly infer A->B as soon as one has refuted A is justified by the truth table; and it also obviates the need for EFQ (in the subordinate proof, to 'get B from' #, before applying the (usual form of the) rule of ->Introduction.

Arnon will no doubt now see immediately how to regiment (as a Core proof) the usual informal proof of the claim that the empty set is a subset of any set. If not, I will happily supply the Core proof for inspection. [It will take a little longer to type up within the constraints of these ascii messages on fom.  :-) ]

Let me repeat: mathematicians (whether constructivists or non-constructivists) never need to use EFQ when they get down to detailed formalizations of their reasoning. Core Logic (or its classicized extension) provides natural deductions (or sequent proofs) whose structures are absolutely homologous to those of the informal proofs being formalized. Logicians have simply been mistaken in thinking that the rule EFQ is needed for the faithful formalization of the deductive reasoning involved in either mathematics or the empirical testing of scientific theories.

Another nice feature of Core Logic is that it is formulated in such a way that any natural deduction of X:A is structurally isomorphic to the corresponding sequent proof of X:A. The sequent system has only reflexivity, A:A, as a structural rule. It has no rule of thinning, and no rule of cut. And it has, besides reflexivity (which allows proofs to get started!), only the Left and Right logical rules for the connectives and quantifiers, *suitably formulated*. That qualification is very important, since it covers all the innovations by means of which Core Logic departs from the standard Gentzen-Prawitz systems of intuitionistic and classical logic.

Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150831/b9d7450f/attachment-0001.html>