[FOM] Tennant on Relevant Logic

[Neil Tennant]

On Wed, 8 Mar 2006, A.P. Hazen wrote:

> Note that it is the logics of the Anderson-Belnap 
> tradition which permit interesting non-trivial negation-inconsistent 
> theories, and weak logics of that family which have been explored as 
> bases for non-trivial "naive" set theory.

The Anderson-Belnap logics are not the only so-called relevant logics that
permit "interesting non-trivial negation-inconsistent theories". So do CR
and IR. All that is required, for interesting non-trivial 
negation-inconsistent theories, is that the inference A,~A:B not hold.
Both CR and IR allow there to be interestingly different, "localized"
inconsistencies.

> 	(1) The "Automated Reasoning Project" at the Australian 
> National University was initially started ... to explore 
> the computer implementation of decision procedures for non-classical 
> logics ...

At the ANU, I read the original funding proposal for the ARP. The
prospect of an automated proof of FLT was, if my memory is correct,
explicitly held out in that document. 

> The proof that it isn't stems  from a result of Harvey 
> Friedman's; the observation that Friedman's result applied to R# was 
> Meyer's, and the result was reported in a joint paper, JSL 57
> (1992), pp. 824-831.

The reason why Friedman proved his result in the first place was because
Meyer had enlisted his help in trying to settle the (false) conjecture
Gamma for R#. I was present at the historic seminar when Meyer returned
from his trip to Columbus, to announce the bad news and explain Friedman's
result and its devastating implications (for the ARP).

> ... the A.R.P. was not sold 
> to the funding bodies as a "We'll prove Fermat's Last Theorem" 
> project.

No, it was sold *within the ANU* as a project holding out the prospect of
an automated proof of FLT. As you probably know, the Institute of Advanced
Study at the ANU often considers proposals for the establishment of units
such as the ARP for special funding during an initial project phase.
The expectation is that after that initial phase the personnel will be
absorbed into other, more permanent units within the ANU. So the ARP
evolved according to the general plan. That it has "been merged into the 
A.N.U.'s general computer science research program" is therefore no
particular endorsement of its project-goals, nor acknowledgement of any
alleged successes. Such mergers would be expected even for failed
projects.

May I add that the ARP was a center for lively research and discussion of
logic and its computational applications, and provided an atmosphere for
investigation of much more than its original stated aims. It greatly
enriched the intellectual atmosphere that I enjoyed during my time at the 
ANU. I even found myself in disagreement with those detractors who, when
asked what extra benefits the ARP actually provided for its graduate
students (as opposed to those who were affiliated within the Philosophy
program), were wont to give the caustic reply "Air-conditioning and color
screens!".

Neil Tennant