FOM: relevance and interpolation

[Neil Tennant]

In reply to Stephen Ferguson', who wrote 

_________________________________________________________________
(Q Is [Tennant] also ruling out A|-B where [A and B have] no 
vocab[ulary in common] and B [is] a theorem, by restricting 
thinning, as this should just be |-B, and the A is
irrelevant?)
_________________________________________________________________

Answer: Yes.  I omitted to mention the undesirability of

	A; therefore (B v ~B)

for a classical relevant logician. This sequent is bad because it is 
a proper dilution of a valid sequent, namely

	[zilch]; therefore (B v ~B)

A further property I want to secure for *relevantly* provable sequents 
is that they should be substitution instances of sequents whose antecedents
are consistent and whose consequents are not provable. This will guarantee
that there has been `no funny business' in the course of the proof.

Stephen goes on to explain a line of thought of Poincare:

___________________________________________________________________
If I know A mathematically, and I
have a logical proof of A-->B, I then have a proof of B. But I don't have
a mathematical proof of B, as I have not [shown] any sort of connection
between A and B, I have not exposed the "inner architecture"
Would a Tennant-style relevantization of the logic have satisfied
Poincare, or do his objections require an even stronger notion of relevant
connection, than Tennant's methods could provide?
_____________________________________________________________________

I would very much hope that Poincare would have accepted that a relevant
proof of the kind I am proposing (with assumption A and conclusion B)
preserves the status of `having a correct mathematical proof' as one passes 
relevantly from A to B. Thus my proofs would preserve not only truth, but
its status as *mathematically established*.

Neil Tennant