[FOM] relevant logic and paraconsistent logic

[Neil Tennant]

On Fri, 3 Mar 2006, Eray Ozkural wrote:

> On 3/2/06, Neil Tennant <neilt at mercutio.cohums.ohio-state.edu> wrote:
> > Mathematics DOES NOT NEED ex falso quodlibet.
> 
> That is interesting, and I am not familiar with relevance logics at all.
> Could you please provide an example?

What you might need is not so much an example, but an explanation of the
metatheorem behind that claim that mathematics does not need EFQ.

I'll deal with the classical case here. For the intuitionistic case,
simply substitute I for C and "intuitionistic" for "classical" in what
follows.

Whether the parent natural-deduction system S is that of classical logic C
or intuitionistic logic I, the relevant natural-deduction system SR is
obtained by
1. not allowing EFQ as a rule of inference;
2. requiring that proofs be in normal form;
3. not allowing "vacuous discharge" with applications of negation
introduction or with applications of conditional introduction of the form

      []__(i)
	P
	:
	#
      _____(i)
      P->Q

Here, the box [] indicates that the assumption P must have been used for
the sub-derivation of absurdity (#). The other half of conditional
introduction is the form that is usually stated all by itself, namely

      <>__(i)
        P
	:
	Q
       _____(i)
       P->Q

where the diamond <> indicates that the assumption P need not have been
used for the sub-derivation of Q, but can be discharged if it has been so
used.

There is also one further liberalization to note. Disjunction elimination
('proof by cases') now takes the form

			[]__(i)  []__(i)
			  P        Q
			  :        :
		PvQ      R/#      R/#
	        ______________________(i)
			 R/#

This is to be understood as follows: If either one of the two case-proofs
ends with #, then the conclusion of the other case-proof can be brought
down as the main conclusion. This allows the patterns

	R  R   (of which   #  #   is a special case);   R  #   ;  #  R
	____               ____                         ____      ____
        R		   #                            R         R

This formuulation of proof by cases answers to the intuition that if one
case closes off with absurdity, then the truth must lie in the other
case. Note that by using this rule we can prove disjunctive syllogism
[AvB, ~A; so B] which is crucial to mathematical reasoning, but which is
normally rejected in competing systems of relevant logic:

	    (1)__
		A   ~A
		______    __(1)
	AvB       #       B
	____________________(1)
		  B

The system CR of classical relevant logic obeys the following metatheorem:

  Any C-proof of conclusion A from premises X can be transformed into a
  CR-proof either of A or of absurdity from (some subset of) X.

As corollaries we have

i.   Any C-proof of A from the empty set of premises can be transformed
     into a CR-proof of A from the empty set of premises;

ii.  Any C-proof of absurdity from a non-empty set X of premises can be 
     transformed into a CR-proof of absurdity from (some non-empty subset
     of) X.

iii. Any C-proof of A from a consistent non-empty set X of premises can be
     transformed into a CR-proof of A from (some subset of) X.

So: CR matches C on (i) logical truths, (ii) inconsistencies, and 
(iii) logical consequences of consistent sets of premises. And in some
cases transforming one's C-proof into a CR-proof will bring with it
"epistemic gain"---either by finding that # is derivable, in place of A;
or by finding that some *proper* subset of X suffices for the logical
implication of A (possibly even: the empty set).

To repeat, the foregoing all holds also for intuitionistic I in place of
classical C.

Since (i)-(iii) form an exhaustive list of theoretical demands on what
what is provable in principle within a logic that is to serve the needs of
mathematics, one can conclude that EFQ is not actually needed for
mathematics.

Neil Tennant