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 il y a des nuages ».
L'implication admet des interprétations différentes selon les différents systèmes logiques (logique classique, modale, intuitionniste, etc.).
Étant un connecteur, qui produit une proposition à partir de deux autres, et qui est interprété par une opération sur les propositions ou sur les valeurs de vérités, l'implication n'est pas la déduction qui est une relation entre propositions.
Les logiciens utilisent couramment pour l'implication la flèche simple « → », et encore parfois le symbole « ⊃ » introduit par Peano. La déduction logique ou l'affirmation d'un théorème peuvent être représentées par des symboles au sens proche mais non identique : « ∴ », « ⊢ » et « ⊨ ».
L'implication logique est une opération binaire qui a donc deux arguments : l'argument de gauche est l’impliquant et l'argument de droite est l’impliqué.
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.
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 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. Elle peut prendre dans d'autres logiques des formes différentes mais analogues dans la démarche, comme la sémantique de Kripke qui permet d'interpréter les logiques modales et la logique intuitionniste (cette sémantique de la logique intuitionniste traduite en fonction de valeurs de vérité en aurait nécessairement une infinité).