> Many understand implication intuitively, yet find its symbolic formulation puzzling.
Yes, and for a reason: material implication (the kind of implication discussed in the article) cannot always explain our intuitive sense of implication. My favourite example, from Priest's Introduction to Non-Classical Logic: (A ⇒ B) ∧ (C ⇒ D) ⊦ (A ⇒ D) ∨ (C ⇒ B) is valid when ⇒ is material, yet the statement:
"If John is in Paris he is in France, and if John is in London he is in England. Hence, it is the case either that if John is in Paris he is in England, or that if he is in London he is in France."
makes no intuitive sense. It is very important to discard intuition when dealing with implication in mathematics -- this is why although I'm a big fan of using English connectives instead of symbolic ones, I try to not use the English "if" and "then" in proofs.