Because of the thoughts like the above, I found the following paper quite interesting:
https://www.tandfonline.com/doi/abs/10.1080/11663081.2014.911540

Vidal points out that (P ^ Q) -> R is equivalent to (P -> R) v (Q -> R). Both these forms can be seen to be equivalent to ~P v ~Q v R. Specific instances of this equivalence can be awkward/counterintuitive:

Example 1:
("x is a rhombus" ^ "x is a rectangle") -> "x is a square"
("x is a rhombus" -> "x is a square") v ("x is a rectangle" -> "x is a square")

(3/n)

Example 2: write a|x for "x is divisible by a" or "a divides x". Then
(2|x ^ 3|x) -> 6|x
(2|x -> 6|x) v (3|x -> 6|x)

In both cases, the first form is natural and obvious and the second is something you'd normally never write. But, if pressed, maybe you'd bite the bullet and agree it's an equivalent form. I'm still undecided but I enjoyed the paper.
#logic #implication #conditional (3/3)

I should have been more precise. The two formal expressions

(2|x ^ 3|x) -> 6|x
(2|x -> 6|x) v (3|x -> 6|x)

are equivalent. However, it is less clear cut with their ordinary language translations:

"If x is divisible by 2 and x is divisible by 3, then x is divisible by 6."
"If x is divisible by 2, then x is divisible by 6, or if x is divisible by 3, then x is divisible by 6."
#logic #implication #conditional

@imdef the main advantage is simplicity; classical logic gives the only reasonable truth functional definition of connectives, so mathematical statements can be readily understood without reference to elaborate semantics or axiom systems. But e.g. constructive proofs, which are used at least sometimes by all mathematicians, would not allow the inference you discuss (invalid in intuitionistic logic)

@RanaldClouston Fair point, simplicity is a point in favor of material implication. What leaves me unsatisfied with the justifications I've read, though, is that they appear to beg the question by not seriously considering what would be different with a non-truth functional "if-then". E.g. a common argument is that it is convenient to allow vacuously true universal statements, but other non-truth functional implications can also allow these.

@imdef I think there's plenty of literature on this, although I'm not an expert on it. Certainly lots written on intuitionistic vs classical; the relevance logicians have plenty to say although I'm not sure how interested they are in mathematical applications; and I have no idea how Lewis's strict conditional would apply to maths (what would the box mean, precisely?)

@RanaldClouston I'm sure logicians have written a lot, I'm just not so familiar with this literature. I think identifying "if-then" with strict implication would avoid some, but not all, unnaturalness. For example, we could translate from English to formal language, and manipulate the material implication:

1. "If 2|x and 3|x, then 6|x."
2. [](2|x ^ 3|x -> 6|x)
3. []((2|x -> 6|x) v (3|x -> 6|x))

But then we'd be blocked from translating back into English, because for an if-then form of line 3 we'd need the stronger

3'. [](2|x -> 6|x) v [](3|x -> 6|x)

@RanaldClouston (With []P meaning "Necessarily, P".)

Vidal also gives the example with a specific value x=4 in the above statement. Here, if I understand the meaning of '2', '4', '6' and the box correctly, the box doesn't really make any difference.

@imdef sure, but what does 'necessarily' mean when applied to mathematics? Most mathematicians would hold that all mathematical truths are necessarily true, which trivialises the modality and hence strict implication collapses to regular implication.

@RanaldClouston At least in simple cases, I think [](P -> Q) says in the object language what P |= Q says in the meta-language. Maybe there's a divergence in complicated cases, I don't know. In the particular case above, I'd take

[](3|x -> 6|x)

to be equivalent to

(for all natural numbers x)(3|x -> 6|x)