Relevant Implications

The 'material implication' of classical logic does a fairly poor job of capturing our intuitive understanding of if-then.  It holds X -> Y [if X then Y] to be logically equivalent to ~X v Y [either not-X, or Y].  So an implication will be true whenever the antecedent is false (regardless of the consequent), or else whenever the consequent is true (regardless of the antecedent).  But it just seems wrong to say "if today is Tuesday then today is Wednesday".  We are more inclined to interpret this as a counterfactual / subjunctive conditional, i.e. "if today were Tuesday then today would be Wednesday" - and this we can see is obviously false.

Further, there are true material implications where the antecedent has nothing to do with the consequent at all.  For example, "if I click my fingers, then 2+2=4".  This is true, even if understood subjunctively (since 2+2=4 is true in all possible worlds).  So the problem isn't so much to do with counterfactual truth-values, as relevance.  Our common-sense understanding of if-then seems to involve an explanatory (perhaps even causal) notion.  To say "if A then B" often means that B depends on A, in some sense.  We might even think that if A is false, then B will be too (which is fallacious reasoning according to classical logic).

I'm not suggesting that our intuitive understanding is better than classical logic, or vice versa (though for particular purposes one might be more suitable than the other).  I just think it would be interesting to formalise the intuitive notion, though I'm not sure how this is best done.  As always, feel free to leave a comment if you know more about all this stuff.

In class today we briefly discussed some oddities about the 'Conditional Proof' natural deduction rule.  The basic idea is that you (temporarily) assume X, somehow or other derive Y, then you can cancel the assumption and conclude that X -> Y.  The oddity arises from the fact that you need not use X when deriving Y.  So if you have already proven Y, then you can use CP to prove X -> Y for any proposition X at all, no matter its truth value or relevance.

One suggestion a classmate offered was that we could modify our CP rule to require that the assumption X must be used in the derivation of Y.  The problem with this (as our lecturer pointed out) is that it is too weak.  One could always just append X using &-intro, then remove it again using &-elim.  It would then be used in the derivation, though in an utterly redundant way.

What we really want here is some way of telling that X needs to be used to derive Y.  My first thought was that we could formalize this requirement as ~(~X -> Y), but in classical logic that is equivalent to X & ~Y, which is clearly not the meaning I was after!  I was really thinking of something like "If X were false then you would not be able to derive Y any longer".  But that begs the question of how to represent counterfactuals.

The closest truth-functional approximation I could think of was ~X -> ~Y, but that's a bit too strong really.  Combined with the original CP, that would prove the biconditional X <--> Y.  Instead, I want to say that if X is false then we cannot (yet) know that Y is true.  Note that this doesn't necessarily mean that Y is false, however.  Hmm... This might work according to some sort of constructivist logic, I'm not sure (I know very little about that stuff).  Suppose "~X" means "I cannot construct a proof of X" (rather than the usual "X is false").  Then I think this formula would capture what I want: If you lack a proof of X, then you cannot construct a proof of Y. [Should this instead be done subjunctively too?  I'm hoping I can get away without it.]

Perhaps it isn't possible to formalize a relevance requirement on CP whilst remaining within classical logic.  Framing relevance in terms of what we can know turns it into an epistemic question (seemingly requiring constructivist logic?), whereas the earlier notion of what we need raises modal issues (and so we need a logic of counterfactuals, to deal with other possible worlds). Truth-functional logic is merely concerned with 'brute' truth-values.  The concept of relevance goes beyond this, so I guess it would make sense for the concept to be unanalysible in truth-functional terms.

Incidentally, a quick google turned up the Stanford encyclopedia entry for Relevance Logic.  I've only skimmed it, but it looks fairly interesting.