[FOM] relevant logic and paraconsistent logic

[Neil Tennant]

On Fri, 3 Mar 2006, Arnon Avron wrote:

> On Thu, Mar 02, 2006 at 04:42:17PM -0500, Neil Tennant wrote:
>  
> > If X is a consistent set of axioms, then any classical consequence of X
> > can be proved from X in classical relevant logic (CR); and
> > if X is a consistent set of axioms, then any intuitionistic consequence of
> > X can be proved from X in intuitionistic relevant logic (IR).
> 
> Neil, I dont quite understand what you mean, and what is the exact
> theorem you have in mind. As far as I remember, even relevant
> arithmetics is very different from classical arithmetics, and quite weak
> (I think Harvey can tell us about it. As far as I recall 
> he once solved one of the main open problems about relevant
> arithmetics). In any case, what happens if X consists just of the
> axioms {P, -P\/Q}? Classically (and intuitionistically) we can infer Q,
> but in the usual relevant logics we cannot. I am sure that you know
> this, so can you clarify your posting?

Arnon,

One needs to distinguish between the systems I call IR and CR, on the one
hand, and those others, like the relevant logic R, that were investigated
by the Anderson-Belnap school. My approach concentrates on the
deducibility relation  |-; the Anderson-Belnap approach concentrates on
the object-language intensional arrow ->. The A-B school is quietist
about the usual structural rules governing |- in their systems. On my
approach, by contrast, one has to take a closer look at those structural
rules, and restrict them in order to avoid irrelevance. Arguably, the
resulting restrictions are methodologically benign. One loses no part of
the deductive power that is needed either for mathematics or for the
testing of empirical theories.

You will be able to find a comprehensive presentation of IR and of CR in
either of my books Autologic or The Taming of The True (ch.10), along with
references to the original papers in which the ideas were first published.
Full details are available on my publications webpage accessible from
http://people.cohums.ohio-state.edu/tennant9/ .

On both approaches (mine or A-B's), the thing to avoid is the first Lewis
paradox, whether in its positive form:

	A, ~A : B

or in its negative form:

	A, ~A : ~B.

Lewis famously gave the following proof of the positive form.

________________________

   First, one can infer AvB in one step from A, by means of vI:

	A
       ___
       AvB

   Secondly, one has Disjunctive Syllogism:

       AvB  ~A
       _______
	  B

   So, by Cut (i.e. [Unrestricted] Transitivity of Deduction), one has

       A   ~A
       ______
	 B
______________________

Now, no-one wishes to reject or restrict or disallow the rule of
disjunction-introduction. So there are only two possible culprits left:
disjunctive syllogism (DS) and [Unrestricted] Transitivity of Deduction
(UTD).

The way my appproach to relevant logic differs from that of
Anderson-Belnap is as folows:

	DS	UTD

A-B     No	Yes

NT	Yes	No

The "failure" of UTD in my systems, however, is benign. The emphasis is on
the "U" in "UTD", not on the "T". Indeed, I argue that the *restricted*
transitivity of deduction that obtains in my system CR (say), is one that
affords *epistemic gain*. The following principle of Restricted
Transitivity holds for CR (in the language of sequents for classical
logic):

	X:Y,A   A,Z:W
	_____________
	 X',Z':Y',W'

where X', Z'. Y', W' are subsets, respectively, of X, Z, Y, W.
So, where CR fails to match C on what is delivered by unrestricted Cut, CR
instead delivers a *proper* subsequent of the sequent that C would
deliver. But having a *proper* subsequent represents epistemic gain! By
"subsetting down" on the right, or on the left, or on both sides, one
learns a stronger logical result.

Illustration: We saw earlier, with the proof of the first Lewis paradox,
that
	A:AvB   AvB,~A:B

(assuming, of course, that one accepts some proof of Disjunctive
Syllogism). Unrestricted Cut would then give the undesired Lewis sequent

	A,~A:B

But CR does not give this. Instead, it gives only

	A,~A:emptyset

which exemplifies the *restricted* transitivity of deduction in CR, since

	A,~A:emptyset 

is a (proper) subsequent of the Lewis sequent.

Now, to return to your question quoted above: the "relevant arithmetic" to
which you refer is the closure (so-called R#, or "R-sharp") of the Peano
axioms under the relevant logic R of Anderson-Belnap. The joint
Friedman-Meyer paper in the JSL showed that that system (contrary to
Meyer's earlier conjecture) failed to satisfy Gamma for R#, which (if I
remember correctly) is the claim "If A is a theorem of R# and (A->B) is a
theorem of R#, then B is a theorem of R#". [The conjectured truth of this
claim was the basis, by the way, of the academic proposal at The
Australian National University which resulted in a significant amount of
money being devoted to the Automated Reasoning Project, whose professed
aim was to find an automated Fermat's Last Theorem (!) by a method whose
plausibility depended on the truth of the conjecture in question. Too bad
Harvey was not brought in as a referee at the time. It could have saved
the Australian taxpayer a lot of money.]

By contrast with the chequered fortunes of R#, the relevantist using CR
can simply say that, if PA is consistent, then any theorem of PA can be
proved from the axioms of PA by means of a CR-proof. Arithmetic (like any
branch of classical mathematics) does not need EFQ.

Neil Tennant