Voir la source de Implication (logique)

{{homonyme|implication}}
En [[logique mathématique]], l''''implication''' est l'un des [[Connecteur logique|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 »<ref>La conjonction « alors » peut être omise, par exemple on peut dire « s'il pleut, il y a des nuages ».</ref>.

L'implication admet des interprétations différentes selon les différents systèmes logiques ([[logique classique]], [[Logique modale|modale]], [[Logique intuitionniste|intuitionniste]], etc.).

Étant un connecteur, qui produit une proposition à partir de deux autres, et qui est interprété par une [[Loi de composition interne|opération]] sur les propositions ou sur les valeurs de vérités, l'implication n'est pas la [[Déduction logique|déduction]] qui est une ''relation'' entre propositions.

Les logiciens utilisent couramment pour l'implication la [[Flèche (symbole)|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 : [[Par conséquent|« '''∴ », '''« ⊢ » et « ⊨ »]].

== Définition ==
L'implication logique est une opération binaire qui a deux arguments : l'argument de gauche est l’''impliquant'' et l'argument de droite est l’''impliqué''<ref>On réserve les termes ''prémisse'' et ''conclusion'' aux [[Règle d'inférence|règles d'inférence]].</ref>. 

Classiquement, le connecteur d'implication est formalisé de deux façons<ref>Une troisième façon peut se faire via la [[correspondance de Curry-Howard]] comme le type des fonctions qui transforment une démonstration du premier argument en une démonstration du second argument.</ref>, soit en fonction de [[Valeur de vérité|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 {{Formule|''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''<ref>{{Lien Web|url=http://www.universalis.fr/encyclopedie/implication-logique/|site=universalis.fr ([[Encyclopædia Universalis]])|auteur=Françoise Armengaud|titre=article ''Implication, logique''}}.</ref>. 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 [[logique modale|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é).

Dans le second cas, si on se place dans le cadre d'un [[système formel]] de règles de [[Déduction logique|déduction]] et d'axiomes, il est souvent possible de distinguer des règles ou des axiomes particuliers associés à ce connecteur. 
 
Ces deux approches sont compatibles et sont reliées par des théorèmes comme le [[théorème de complétude]] pour la logique classique, ou le [[théorème de complétude du calcul des propositions]] pour le calcul des propositions, à titre d'exemple.

=== Définition en logique classique ===
La logique classique n'a que deux valeurs de vérité, « vrai » et « faux », que l'on représente par 1 et 0. 
Le connecteur « ⇒ » s'interprète alors par une [[application (mathématiques)|application]] de l'ensemble {0,1}<sup>2</sup> sur {0,1}, soit une [[fonction booléenne|opération booléenne]] ayant la [[table de vérité]] suivante :
{| class="wikitable" border="1" width=180px
|-----
! P || Q || P ⇒ Q
|-----
| Vrai || Vrai || Vrai
|-----
| Vrai || Faux || Faux
|-----
| Faux || Vrai || Vrai
|-----
| Faux || Faux || Vrai
|}

La proposition « {{Formule|''p'' ⇒ ''q''}} » (“''p'' implique ''q''”) est [[Équivalence logique|logiquement équivalente]] à « {{Formule|¬''p'' ∨ ''q''}} » (“non(''p'') ou ''q''”). On présente généralement cette propriété comme un théorème qui se démontre en remarquant que les tables de vérités de « {{Formule|''p'' ⇒ ''q''}} » et de « {{Formule|¬''p'' ∨ ''q''}} » sont exactement les mêmes. Certains ouvrages de mathématique<ref>{{Ouvrage|langue=français|auteur1=Marc-Aurèle Massard|titre=Maths BCPST 1re année|passage=|lieu=|éditeur=J'assure aux concours, Dunod|date=août 2018|pages totales=512|isbn=|lire en ligne=https://www.dunod.com/prepas-concours/maths-bcpst-1re-annee}}</ref> utilisent aussi parfois cette propriété comme une définition de « {{Formule|''p'' ⇒ ''q''}} ». Il n'est pas rare que des objets mathématiques puissent avoir plusieurs définitions. Mais il y a généralement une définition plus classique ou plus conforme à l'histoire et la chronologie de l’apparition de ces objets dans le corpus correspondant, même si d'autres définitions sont parfois plus pratiques à manipuler. L'avantage de définir « {{Formule|''p'' ⇒ ''q''}} » = « {{Formule|¬''p'' ∨ ''q''}} » est d'avoir une définition algébrique compacte, que l'on peut donc manipuler plus facilement dans des développements mathématiques qu'une table de vérité. Mais il est quand même préférable et plus conforme à la logique chronologique de définir cet opérateur binaire à partir de sa table de vérité tout comme ses homologues « {{Formule|¬''p'' ∨ ''q''|§=¬}} » (non), « {{Formule|¬''p'' ∨ ''q''|§=∨}} » (ou), et ∧ (et).

Ainsi, la proposition « {{Formule|''p'' ⇒ ''q''}} » est fausse exactement lorsque ''p'' est vraie et ''q'' fausse, raison pour laquelle elle peut aussi se lire « ''p'' seulement si ''q'' ». L’intérêt de cet opérateur binaire « {{Formule|''p'' ⇒ ''q''|§=⇒}} » est donc de ne pas accepter (Faux) dans le cas, et seulement celui-là, où l'on part d'une proposition P vraie et qu'on arrive à une proposition Q fausse.  En effet, la plupart des démonstrations mathématiques partent d'hypothèses supposées vraies (y compris dans les raisonnements par l'absurde) et conduisent par des déductions successives à d'autres propositions qui permettent soit d'arriver à ce qu'on veut démontrer (CQFD), soit à une absurdité, ce qui prouve alors qu'une des hypothèses est fausse. Les trois autres cas sont autorisés (Vrai), même si certains peuvent paraitre contre-intuitifs. Mais cela est facile à comprendre, cf. les exemples ci-dessous. Il y a donc bien un lien entre cette opérateur binaire « {{Formule|''p'' ⇒ ''q''|§=⇒}} » en logique classique, et celui qu'on utilise dans le cadre de règles de déduction des développements mathématiques. Exemple :

* 2=2 {{Formule|''p'' ⇒ ''q''|§=⇒}} 2*0=2*0 : (exemple de Vrai {{Formule|''p'' ⇒ ''q''|§=⇒}} Vrai), cette implication est valide (Vraie) car on a le droit de multiplier les 2 membres par 0

* <math>2^2</math>=<math>(-2)^2</math> {{Formule|''p'' ⇒ ''q''|§=⇒}} 2=-2 : (exemple de Vrai {{Formule|''p'' ⇒ ''q''|§=⇒}} Faux ), cette implication est invalide (Fausse) car en prenant la racine on doit écrire +/-

* 2=1 {{Formule|''p'' ⇒ ''q''|§=⇒}} 2*0=1*0 : (exemple de Faux {{Formule|''p'' ⇒ ''q''|§=⇒}} Vrai), cette implication est valide (Vraie) car on a le droit de multiplier les 2 membres par 0

* 2=1 {{Formule|''p'' ⇒ ''q''|§=⇒}} 2+1=1+1 : (exemple de Faux {{Formule|''p'' ⇒ ''q''|§=⇒}} Faux ), cette implication est valide (Vraie) car on a le droit d'ajouter 1 aux 2 membres

Le connecteur « implique » a donc une propriété qui le différencie d'un « donc » intuitif : d'après la table de vérité ci-dessus, si une proposition ''p'' est fausse, alors elle implique n'importe quelle autre proposition ''q'', vraie ou fausse. Dans les exemples 3 et 4 ci-dessus on voit bien que des manipulations mathématiques licites (l'opérateur binaire « implique » est vrai, ainsi que la règle de déduction mathématique) conduit d'une proposition p fausse (2=1) à une proposition q vraie (0=0) ou fausse (3=2).

==== Propriétés détaillées en logique classique ====

===== Sous forme implicative =====
Les formules suivantes, constituées seulement de l'implication et de [[Littéral (logique)|littéraux]], sont des [[Tautologie (logique)|tautologie]]s <ref group="cori_lascar_1">Chap. 1, §2.11 p. 43.</ref> :

;''p'' ⇒ ''p'' 
: ''p'' a toujours la même valeur de vérité que ''p'', donc cette implication est correcte. Elle est liée à la réflexivité de la déduction en logique classique.
;''p'' ⇒ (''q'' ⇒ ''p'')
: Si ''p'' est vrai, ''q''⇒ ''p'' est vrai aussi (c’est un des dits {{Lien|paradoxes de l'implication matérielle|trad=Paradoxes of material implication}}.)
;(''p'' ⇒ ''q'') ⇒ ((''q'' ⇒ ''r'' ) ⇒ (''p'' ⇒ ''r'' ))
: Cette formule est liée à la [[Relation transitive|transitivité]] de la relation de déduction ; elle est équivalente à la [[Tautologie (logique)|tautologie]] [(''p'' ⇒ ''q'') ∧ (''q'' ⇒ ''r'')] ⇒ (''p'' ⇒ ''r'' ) par {{Lien|Exportation (logique)|trad=Exportation (logic)|texte=exportation}}.
;(''p'' ⇒ ''q'') ⇒ (((''p'' ⇒ ''r'' ) ⇒ ''q'') ⇒ ''q'')
: Cette formule est une formulation sous forme purement implicative du fait qu’en logique des prédicats si ''p'' ⇒ ''q'' et si ¬''p'' ⇒ ''q'' alors ''q'' est vraie dans tous les cas.
;(''¬p'' ⇒ ''p'') ⇒ ''p''
: Cette tautologie conduit (par [[modus ponens]]) au raisonnement par l’absurde en logique classique.
;¬''p'' ⇒ (''p'' ⇒ ''q'')
: Cette tautologie conduit (toujours par modus ponens) au [[principe d’explosion]].

===== Sous forme composée d’autres connecteurs =====
;« ''p'' ⇒ ''q'' » [[Équivalence logique|équivaut à]] « ¬(''p'' ∧ ¬''q'') » ainsi qu'à « (¬''p'') ∨ ''q'' ».
: Ces deux formules pourraient être prises comme des définitions de l'implication. Essentiellement elles décrivent la table de vérité, la première donne le seul cas où « ''p'' ⇒ ''q'' » est fausse, la seconde les cas où « ''p'' ⇒ ''q'' » est vraie.
;« ''p'' ⇒ ''q'' » équivaut à « ¬''q'' ⇒ ¬''p'' ».
: Ces deux formules sont dites ''contraposées''.
;« ''p'' ⇒ (''q'' ∧ ''r'' ) » équivaut à « (''p'' ⇒ ''q'') ∧ (''p'' ⇒ ''r'' ) » et « ''p'' ⇒ (''q'' ∨ ''r'' ) » à « (''p'' ⇒ ''q'') ∨ (''p'' ⇒ ''r'' ) ».
: Distributivité ''à gauche'' de l’implication par rapport à la [[Conjonction logique|conjonction]] et à la [[Disjonction logique|disjonction]]
;« (''p'' ∧ ''q'') ⇒ ''r'' » équivaut à « (''p'' ⇒ ''r'' ) ∨ (''q'' ⇒ ''r'' ) » et « (''p'' ∨ ''q'') ⇒ ''r'' » à « (''p'' ⇒ ''r'' ) ∧ (''q'' ⇒ ''r'' ) ».
: En revanche elle n'est [[Distributivité|distributive]] à droite ni par rapport à la conjonction ni par rapport à la disjonction : si le « ⇒ » est à droite, dans l'expression développée le « ∧ » se transforme en « ∨ » et vice-versa <ref group="cori_lascar_1">''Op. cit.'' p. 44.</ref>.
; Non [[associativité]].
: L'implication n'est pas associative, car « (''p'' ⇒ ''q'') ⇒ ''r'' » et « ''p'' ⇒ (''q'' ⇒ ''r'' ) » ne prennent pas les mêmes valeurs pour toutes les distributions de valeurs de vérité, on s'en convaincra en donnant la valeur 0 à « ''p'' » et à « ''r'' » : la première expression vaut 0 et la seconde vaut 1.

=== Implication et 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 »). Cependant, le connecteur implication et la relation de déduction sont étroitement liées par les deux règles suivantes :
* Le [[modus ponens]] est la règle de déduction qui indique comment s'utilise une implication dans une démonstration ; elle s'énonce ainsi : de ''p'' et de ''p'' ⇒ ''q'' on déduit ''q''<ref group="cori_lascar_1">Chap. 4, §1.1 p. 229.</ref> ;
* Le lemme de déduction indique comment l'on démontre une implication : si de ''p'' on déduit ''q'', alors on en déduit ''p'' ⇒ ''q''{{refsou}}.
Ces règles sont les deux règles fondamentales qui gouvernent l'implication. Adaptées à la [[déduction naturelle]] (il faut les préciser en indiquant en particulier le contexte des hypothèses), elles deviennent ''règle d’élimination'' (modus ponens) et ''règle d'introduction'' (lemme de déduction) de l'implication<ref>Voir également [[Style de Fitch pour la déduction naturelle#Les r.C3.A8gles relatives .C3.A0 l.27implication|une autre présentation de la déduction naturelle]].</ref>. 

Ces deux règles sont suffisantes pour l'implication en [[logique intuitionniste]].

En [[logique classique]], il faut ajouter une forme de [[raisonnement par l'absurde]]. Par exemple il suffit d'ajouter comme [[axiome]] logique la [[loi de Peirce]] ((''p'' ⇒ ''q'') ⇒ ''p'') ⇒ ''p'', qui est purement implicationnelle.

=== Définition en logique intuitionniste ===
Dans le cadre de l'[[interprétation de Brouwer-Heyting-Kolmogorov]], qui est une interprétation en matière de preuves, une preuve de ''A'' ⇒ ''B'' est vue comme un procédé, une [[fonction (mathématiques)|fonction]] en un sens effectif, qui transforme une preuve de ''A'' en une preuve de ''B''. La [[réalisabilité]] est une contrepartie formelle de cette sémantique informelle.

En [[sémantique de Kripke]], qui est une sémantique traditionnelle en matière de mondes possibles, avec une relation d'accessibilité qui dans le cas de la logique intuitionniste est sans cycle, on a ''A''&nbsp;⇒&nbsp;''B'' dans le monde ''m'' quand, à chaque fois que l'on a ''A'' dans un monde accessible à partir de ''m'', on a aussi ''B''.

=== Définition en logiques modales ===
Les logiques modales sont des extensions de la logique classique, et l'implication y possède alors la même interprétation. Cependant, les opérateurs modaux permettent de définir des formes plus fortes de l'implication.

== Historique et applications de l'implication ==

L'implication était connue dès la [[Grèce antique]], notamment par les [[Stoïcisme|stoïciens]] sous une forme telle que : {{citation|Du vrai suit le vrai… Du faux suit le faux… Du faux suit le vrai… Mais du vrai, le faux ne peut s'ensuivre}}<ref>[[Diogène Laërce]], ''[[Vies, doctrines et sentences des philosophes illustres]]'', livre VII, 83.</ref>. Ceci correspond à l'« implication matérielle » (par exemple, comme toute proposition vraie implique n'importe quelle proposition vraie, on peut dire que {{citation|La mer est salée implique que la France n'est pas en Australie}}), qui fut redécouverte par [[Gottlob Frege|Frege]] en 1879 et [[Charles Sanders Peirce|Peirce]] en 1885. La pertinence de cette notion fut débattue tant dans l'Antiquité classique que dans la période contemporaine<ref>[[Willard Van Orman Quine]], ''{{Langue|en|Methods of Logic}}'', Holt, Rinchart & Winston, Inc. 1972, trad. fr. par Maurice Clavelin, ''Méthodes de logique'', Armand Colin, Paris 1973, chap. 3, pp. 32-33.</ref>.

Une proposition du type « Si Napoléon avait gagné la [[Bataille de Waterloo]], alors la gare la plus fréquentée de Londres ne s’appellerait pas [[Gare de Londres Waterloo|gare de Waterloo]] », qui est une proposition dont l'impliquant est contraire aux faits, n'est pas considérée comme une implication, par les philosophes. Ils parlent dans ce cas précis de [[raisonnement contre-factuel]].

Dans les exemples tirés du langage courant, tels que « si 1 = 2, je suis le pape », où cette implication produit des énoncés volontairement saugrenus mais vrais, les énoncés portent sur des objets fixés ; il n'en va pas de même en mathématiques, où les énoncés contiennent des variables ''x'', ''y'', ''m'', ''n'', etc.

Il s'ensuit que l'usage de l'implication par les mathématiciens diffère de celui donné par ces exemples. Ainsi, un mathématicien considèrera comme faux l'énoncé :
<center>''si ''n'' est divisible par 7, alors ''n'' est impair''.</center>

En effet, il ne s'agit pas d'une simple implication matérielle ; l'expression telle quelle n'est pas une fonction de vérité, elle est vraie pour ''n'' = 21, et fausse pour ''n'' = 28 ; elle n'a de sens qu'accompagnée d'un quantificateur, ici le quantificateur (universel) est sous-entendu<ref group="cori_lascar_1">Chap. 1, 2.1 p. 32.</ref>.

== Notes et références ==
'''Ouvrages'''
* {{Cori-Lascar I}}
{{Références|groupe=cori_lascar_1|colonnes=}}
'''Autres citations'''
{{Références|colonnes=}}

== Voir aussi ==
{{autres projets
  | wikt = implication
  | wiktionary titre = Implication
  | wikiversity = Implication et équivalence
  | wikiversity titre = Implication et équivalence
}}
* [[Implication réciproque]]
* [[Non-implication]]
* [[Implication stricte]] et [[Paradoxe du coiffeur]] sur des aspects contre-intuitifs de l'implication logique.
* [[Déduction naturelle]]
* [[Équivalence logique]]
* [[Logique mathématique]], [[logique classique]], [[logique intuitionniste]], [[logique linéaire]]
* [[Modus ponens]]
* [[Modus tollens]]
* [[Prolog]]

{{Palette|Logique|Règles de transformation|Connecteurs logiques}}
{{Portail|logique|philosophie|mathématiques}}

[[Catégorie:Connecteur logique]]