FOM: relevance and interpolation
neilt at hums62.cohums.ohio-state.edu
Thu Nov 20 17:12:19 EST 1997
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
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*.
More information about the FOM