Why do we define logical implication p ⇒ q the way we do? Is it an arbitrary convention, just a shorthand for ¬p ∨ q, or a fundamental concept of great importance?

I prefer to look for justifications that are internal to mathematics. A worthy mathematical idea unveils important structure, has great explanatory power, unifies several hitherto unrelated concepts, or exhibits a phenomenon as a special case of a more general one.

When studying a fundamental concept, we should strive for generality, so that we are forced to make the most efficient analysis with as few assumptions as necessary, untainted with the peculiarities of a less general situation.

For example, defining implication p ⇒ q as an abbreviation for ¬p ∨ q is only satisfactory in the presence of excluded middle – a peculiar situation. Also, it does not explain anything. Why should ¬p ∨ q be of any importance?

Next, explaining logic in terms of truth tables is unsatisfactory. We can only do so thanks to an (important!) theorem stating that the Boolean algebra {⊥,⊤} is complete for classical propositional calculus – but just stating this presupposes the propositional calculus.

Also, truth tables only capture the bare truth-value semantics, but not the meaning of connectives. That is, just because two statements have the same truth value, they are not interchangeable in every situation.

Ok, so how then should we explain ⇒? Note that I am not asking for a bare formal definition of ⇒, but rather an insight of why ⇒ is defined the way it is. I am aware of several such explanations that collectively justify ⇒ as significant and far from arbitrary.

(1) A category theorist might point out that a cartesian-closed poset is precisely a Heyting algebra, and thus implication is a special case of exponentiation. Exponentiation is important because it is right adjoing to products.

(2) A second category theorist might point out that, in a poset, p ⇒ q is the right adjoint to p ∧ q (in the sense of Galois connections), where ∧ is infimum. But that is just what the first category theorist said, only with different words.

(3) A proof theorist would say that p ⇒ q is the "internal logical entailment", i.e., ⇒ is the connective satisfying "p₁, ..., pᵢ, q ⊢ r if and only if p₁, ..., pᵢ ⊢ q ⇒ r" – which would amuse the second category theorist, because that's what they said already.

(4) A philosopher would perform an analysis that revealed p ⇒ q as the connective that faithfully reflects hypothetical reasoning. The proof theorist suspects that's just a vague restatement of what they said (if only the proof theorist knew more history of logic...)

(5) A young type theorist would start explaining λ-calculus and computation, and how according to the Curry-Howard correspondence implication is just the function type. The proof theorist would not be impressed, but the philosopher would be intrigued.

Finally, a working mathematician would innocently ask what the fuss is all about, isn't p ⇒ q equivalent to ¬p ∨ q, and why isn't that good enough? Everyone would roll their eyes, and the first category theorist would mumble someting about Boolean algebras being Heyting.