En logique mathématique, l'implication est l'un des connecteurs binaires du langage du calcul des propositions, généralement représenté par le symbole « ⇒ » et se lisant « … implique … », « … seulement si … » ou, de façon équivalente, « si …, alors … » comme dans la phrase « s'il pleut, alors mon gazon est arrosé ».
L'implication logique est une opération binaire qui a donc deux arguments : l'argument de gauche, qui est l’impliquant et l'argument de droite, qui est l’impliqué.
L'implication admet des interprétations différentes selon les différents systèmes logiques (logique classique, modale, intuitionniste, etc.).
Classiquement, le connecteur d'implication est formalisé de deux façons, soit en fonction de valeurs de vérité, soit en termes de déduction. L'implication (correspondant au « si …, alors … »), qui est un connecteur, se distingue de la relation de déduction (marquée, par exemple, par le mot « donc »).
Dans le premier cas, il s'agit de donner une valeur de vérité à toute proposition. En logique formelle, pour chaque connecteur, la valeur de vérité du résultat dépend uniquement de celles des opérandes, c'est-à-dire que la valeur de vérité de p⇒q ne dépend que de celles de p et q. Par exemple, il n'est pas question de rendre compte d'un lien de causalité, qui indiquerait comment la vérité de q découle de celle de p. On définit donc l'implication en l'interprétant par une fonction de vérité. La logique classique n'a que deux valeurs de vérité : le vrai et le faux.
L'implication est ainsi résolument différente de la déduction qui est une relation entre propositions.
