Paradoxes of Material Implication (1997) (opens in new tab)

Material implication has its advantages, but it does sometimes lead to errors. That said, there are ways to reduce the problem.

One error is that sometimes people use material implication inside of for-all, and forget that if the antecedent is always false than the entire expression is always true. I specifically created a quantifier called allsome that counters that problem: https://dwheeler.com/essays/allsome.html

Another problem is using material implication inside there is quantifier. That is almost always a mistake, as usually and is meant instead. However, that is pretty easy to detect automatically. Both Why3 and SPARK already attack that.

There's another "solution" to this paradox: if we assert something we are guided by a set of "conversational principles". For example, asserting "X implies Y" if we know that X is false is inappropriate. If X is false, "not-X" would be the appropriate assertion.

According to this theory, there's nothing wrong with the truth-functional meaning of "X implies Y". We just need to take into account what is implied by asserting "X implies Y", rather than e.g. "not-X", or "X and Y".

Same with disjunction: "X or Y" is true if we know that X is true. However, if we assert "X or Y", it is implied that we're not certain that X is true, otherwise we would have used "X", which is the simplest way to convey what that fact.

This is known as Grice's Pragmatic Defence of Truth-Functionality.

Entailment: The Logic of Relevance and Necessity suggested in the article as further reading on relevance logics is on the expensive side. If you can't get hold of it, the Standford Encyclopedia of Philosophy goes on at some length into the subject of relevance (or relevant) logics:

https://plato.stanford.edu/entries/logic-relevance/

And also the related subject of necessity and sufficiency:

https://plato.stanford.edu/entries/necessary-sufficient/

Btw, all these are issues with material implication in propositional logics. I'm not sure, but I think, in first-order (and, I guess, higher order) logics you can determine the relevance of premises to conclusions more easily, thanks to quantifiers.

For example, if I say that ∀x,y P(x) → Q(y), or even P(x) → P(y), it's easy to see that the premises are irrelevant to the conclusions (and if not, I can always add that x ≠ y and, in higher order logics, that P ≠ Q).

But, I don't know, there may be something I'm missing. Am I wrong about this?

This was one of my headaches while studying any type of logic - material implication properties just sound weird and don't model what I call implication in my brain. IMO the only case when we can say anything about two unrelated propositions in general, is when T -> F yields F; the rest should be either undefined or defined based on their relationship/context (something like what relevance logic tries to do).

Classical logic is optimized for the verification that no contradiction is made and convenient mathematical manipulation: Boolean algebras are very nice. Unfortunately intuition goes out the window.

On the other hand I found intuitionistic implication more... intuitive :)