Contradiction et négation

Utilité et subtilité de la négation

Depuis le début de ce cours, nous démontrons que certains énoncés mathématiques sont vrais. Mais il est parfois utile de savoir qu'un énoncé est faux, soit parce qu'il s'agit d'une information pertinente directement, soit comme étape intermédiaire dans une démonstration. L'exemple le plus simple consiste à affirmer que deux objets mathématiques sont différents. Par exemple on peut affirmer que les nombres entiers $1$ et $2$ sont différents, c'est-à-dire que l'énoncé « $1 = 2$ » est faux. Un exemple légèrement plus complexe, mais historiquement important, est celui de l'irrationalité de $\sqrt 2$ : il n'existe aucun nombre rationnel $p/q$ tel que $(p/q)^2 = 2$. Autrement dit, l'énoncé $∃ (p, q) ∈ ℤ × ℕ^*, (p/q)^2 = 2$ est faux, mais il s'agit d'une information intéressante qu'on aimerait aussi voir comme une affirmation.

De plus nous avons vu qu'il est essentiel dans le contexte d'énoncés quantifiés que $P ⇒ Q$ soit vrai quand $P$ est « faux ». Par exemple l'énoncé $∀ x ∈ ℤ, x > 0 ⇒ 2x > 0$ est vrai, on peut donc le spécialiser à $x = -1$ qui est bien un entier relatif. On obtient l'énoncé $-1 > 0 ⇒ 2×(-1) > 0$ qui est bien correct car $-1 > 0$ est faux donc il est inutile d'examiner l'autre côté de l'implication pour savoir que l'implication est vraie. Cette règle logique est souvent désignée sous le nom latin ex falso, abréviation de ex falso quod libet : « du faux découlerait tout ce que l'on désire ».

Un autre point essentiel sous-jacent à cette discussion est qu'un énoncé mathématique ne peut pas être à la fois vrai et faux. Un tel énoncé serait dit contradictoire, et toute tentative de construire une théorie mathématique se doit d'éviter cette situation.

On pourrait penser à première vue que les considérations ci-dessus suffisent à cerner suffisamment la question de la négation d'énoncé mathématique et de la contradiction pour les utiliser en pratique dans le raisonnement mathématique. Mais l'expérience montre que ce niveau intuitif (ou même le niveau intermédiaire des « tables de vérité ») ne suffit pas pour comprendre correctement les négations d'énoncés comportant des quantificateurs et des implications. Il s'agirait par exemple de comprendre sans hésitation ce que signifie : « la fonction $f$ n'est pas croissante », c'est-à-dire la négation de l'énoncé « $∀ x\, y, x ≤ y ⇒ f(x) ≤ f(x)$ ». Une erreur classique consiste à penser que cette négation serait « f est décroissante ». Cela ne peut pas être la réponse correcte car il existe des fonctions qui ne sont ni croissantes ni décroissantes, par exemple $x ↦ x^2$. Ce type d'erreur est particulièrement tentant si on emploie le mot plus vague « contraire » à la place de « négation ». Plus difficile, il est indispensable de savoir sans hésitation ce que signifie « la suite $u$ ne tend pas vers zéro », c'est-à-dire la négation de « $∀ ε > 0, ∃ N, ∀ n ≥ N, |u_n| ≤ ε$ ». Ici l'erreur classique consiste à penser que la réponse est « $\lim u_n ≠ 0$ », alors que la suite pourrait n'avoir aucune limite (c'est d'ailleurs la raison pour laquelle la notation $\lim$ du lycée n'est presque jamais employée dans les cours de mathématiques sérieux). Dans les deux sections suivantes, nous allons donc décrire une façon minimale d'introduire un langage et des règles permettant de donner un sens à tout cela. On en déduira un certain nombre de règles pratiques de manipulation des négations.

Le faux et négation

Voici les deux premiers ingrédients de l'axiomatisation concise annoncée : d'abord on introduit dans la théorie un énoncé qu'on appelle $\mathrm{Faux}$ et qui, par définition, n'a pas de démonstration. Puis, pour chaque énoncé $P$, on définit la négation « $\mathrm{non} P$ » de $P$ comme étant l'énoncé « $P ⇒ \mathrm{Faux}$ ».

On peut aussi lire $\mathrm{Faux}$ comme « contradiction » ou « absurdité » puisque toute démonstration semblant aboutir à $\mathrm{Faux}$ est nécessairement basée sur quelque chose d'incorrect.

Les mathématiques usuelles se passent de notation pour $\mathrm{Faux}$ et pour la négation, mais les logiciens et les informaticiens utilisent la notation $⊥$ pour le faux et $¬ P$ pour la négation (ou parfois $\bar P$ mais cette dernière notation n'est vraiment pas commode quand $P$ est long à écrire). Lean utilise au choix false ou ⊥ pour $\mathrm{Faux}$ et ¬ P pour la négation. Puisque le symbole ⊥ est aussi utilisé pour d'autres choses, nous utiliserons uniquement false dans ce cours.

Vérifions que les propriétés attendues découlent de cette construction. Tout d'abord $\mathrm{Faux} ⇒ P$ est vrai pour tout énoncé $P$. En effet cette implication affirme que toute démonstration de $\mathrm{Faux}$ peut être utilisée pour démontrer $P$, ce qui est correct car il n'y a aucune démonstration de $\mathrm{Faux}$ donc l'affirmation n'a aucun contenu. Bien qu'on puisse ainsi démontrer le principe ex falso quod libet, on continue à l'appeler « règle du ex falso » pour insister sur son rôle fondamental.

Exemple

Vérifions le principe de non-contradiction. Soit $P$ un énoncé. Montrons que supposer que $P$ et non $P$ sont tous deux vrais aboutit à une contradiction.

example (P : Prop) : P ∧ ¬ P → false :=
Démonstration
Supposons que $P$ et non $P$, et montrons une contradiction. 
  intro h,

P : Prop
⊢ P ∧ ¬P → false

P : Prop,
h : P ∧ ¬P
⊢ false

  cases h with hP hnP,

P : Prop,
h : P ∧ ¬P
⊢ false

P : Prop,
hP : P,
hnP : ¬P
⊢ false
Vu l'hypothèse « non $P$ », il suffit de montrer que $P$ est vrai pour obtenir la contradiction. 
  apply hnP,

P : Prop,
hP : P,
hnP : ¬P
⊢ false

P : Prop,
hP : P,
hnP : ¬P
⊢ P
Or on a supposé $P$ donc c'est fini. 
  exact hP,

P : Prop,
hP : P,
hnP : ¬P
⊢ P

no goals
QED.

La version concise de cette démonstration serait rintro ⟨hP, hnP⟩, exact hnP hP. La démonstration ci-dessus n'utilise rien d'autre que l'existence d'un symbole false et la définition de ¬ P comme P → false. Pour invoquer la règle du ex falso, on utilise la commande exfalso.

Exemple

Montrons que si on suppose qu'un énoncé $P$ est à la fois vrai et faux alors les entiers naturels $0$ et $1$ sont égaux.

example (P : Prop) (h : P ∧ ¬ P) : 0 = 1 :=
Démonstration
D'après la règle ex falso, il suffit de trouver une contradiction dans les hypothèses. 
  exfalso,

P : Prop,
h : P ∧ ¬P
⊢ 0 = 1

P : Prop,
h : P ∧ ¬P
⊢ false
Or on a supposé $P$ et non $P$ 
  cases h with hP hnP,

P : Prop,
h : P ∧ ¬P
⊢ false

P : Prop,
hP : P,
hnP : ¬P
⊢ false
donc on peut appliquer l'hypothèse non $P$ à l'hypothèse $P$ pour conclure. 
  exact hnP hP,

P : Prop,
hP : P,
hnP : ¬P
⊢ false

no goals
QED.

La leçon à tirer de l'exemple ci-dessus n'est pas que $0 = 1$ mais bien que les hypothèses de cet exemple sont contradictoires. On verra dans la section suivante comment utiliser cette stratégie de façon beaucoup moins artificielle.

Puisque la négation d'un énoncé $P$ est définie comme l'implication $P ⇒ \mathrm{Faux}$, la démonstration (directe) de « $\mathrm{non} P$ » se fait en supposant $P$ et en démontrant une contradiction.

Exemple

Montrons par exemple que si $P$ est vrai alors $\mathrm{non} P$ est faux.

example (P : Prop) : P → ¬ ¬ P :=
Démonstration
Supposons $P$ 
  intro hP,

P : Prop
⊢ P → ¬¬P

P : Prop,
hP : P
⊢ ¬¬P
Pour montrer $\mathrm{non} (\mathrm{non} P)$, on suppose $\mathrm{non} P$ 
  intro hnP,

P : Prop,
hP : P
⊢ ¬¬P

P : Prop,
hP : P,
hnP : ¬P
⊢ false
et on obtient une contradiction avec l'hypothèse que $P$ est vrai. 
  exact hnP hP,

P : Prop,
hP : P,
hnP : ¬P
⊢ false

no goals
QED.

L'exemple précédent montre que si $P$ est vrai alors $P$ n'est pas faux. Mais l'axiomatique introduite jusqu'ici ne permet pas de démontrer la réciproque : si on suppose que $P$ n'est pas faux, on ne peut encore en déduire que $P$ est vrai. Ce problème sera traité dans la section suivante.

Principe du tiers exclu, raisonnement par l'absurde et disjonction de cas

On a vu qu'un énoncé mathématique ne peut pas être à la fois vrai et faux, et que l'axiomatisation introduite ci-dessus rend bien compte de ce principe de non-contradiction. Mais elle n'inclus pas le principe du tiers exclu qui postule que tout énoncé mathématique est soit vrai soit faux : pour tout énoncé $P$, « $P$ ou non $P$ » est vrai.

Pour certaines applications de la logique, il est important de bien séparer les résultats qui dépendent de ce principe de ceux qui n'en dépendent pas. Par exemple si on démontre qu'il existe un logiciel de pilotage automatique d'avion se comportant toujours correctement mais que la démonstration utilise le principe du tiers exclu alors la démonstration risque de n'avoir aucune utilité pratique : le fait de savoir que, par le principe du tiers exclu, à tout moment l'avion doit soit changer de vitesse soit garder sa vitesse ne dit rien sur ce que doit faire l'avion...

Bien sûr ce genre de considération ne concerne pas ce cours de maths. On ajoute donc ce principe à la théorie, c'est le troisième ingrédient promis. Mais on signalera (au moins au début) quels sont les résultats dont la démonstration nécessite le principe du tiers exclu. On récupère au passage que si $P$ n'est pas faux alors $P$ est vrai (voir l'exemple suivant). Puisque nous avons déjà expliqué l'autre implication, on obtient le principe d'élimination des doubles négations qui stipule qu'un énoncé est vrai si et seulement si il n'est pas faux : $P ⇔ ¬ ¬ P$.

Exemple

Soit un énoncé $P$ vrai ou faux. Si $P$ n'est pas faux alors il est vrai.

example (P : Prop) (h : P ∨ ¬ P) : ¬ ¬ P → P :=
Démonstration
Supposons que $P$ n'est pas faux 
  intro hnnP,

P : Prop,
h : P ∨ ¬P
⊢ ¬¬P → P

P : Prop,
h : P ∨ ¬P,
hnnP : ¬¬P
⊢ P
Par hypothèse, $P$ est vrai ou faux 
  cases h with hP hnP,

P : Prop,
h : P ∨ ¬P,
hnnP : ¬¬P
⊢ P

2 goals
case or.inl
P : Prop,
hnnP : ¬¬P,
hP : P
⊢ P

case or.inr
P : Prop,
hnnP : ¬¬P,
hnP : ¬P
⊢ P
Si $P$ est vrai, on a terminé 
    exact hP,

2 goals
case or.inl
P : Prop,
hnnP : ¬¬P,
hP : P
⊢ P

case or.inr
P : Prop,
hnnP : ¬¬P,
hnP : ¬P
⊢ P

case or.inr
P : Prop,
hnnP : ¬¬P,
hnP : ¬P
⊢ P
Supposons maintenant que $P$ est faux. On veut toujours démontrer que $P$ est vrai. Pour démontrer quoique ce soit, il suffit de démontrer une contradiction. 
    exfalso,

case or.inr
P : Prop,
hnnP : ¬¬P,
hnP : ¬P
⊢ P

P : Prop,
hnnP : ¬¬P,
hnP : ¬P
⊢ false
Or nos hypothèses sont contradictoires, puisque nous supposons que $P$ n'est pas faux et qu'il est faux. 
    exact hnnP hnP,

P : Prop,
hnnP : ¬¬P,
hnP : ¬P
⊢ false

no goals
QED.

En pratique le résultat précédent n'est jamais invoqué sous cette forme (et on ne passe pas non plus son temps à le redémontrer comme ci-dessus). On écrit « Supposons par l'absurde que $P$ est faux » puis on démontre une contradiction et on en déduit que $P$ est vrai. Cela correspond bien à l'application de $¬ ¬ P → P$. Dans Lean, la commande correspondante est by_contradiction h qui introduit une hypothèse h affirmant que le but que nous voulions démontrer est faux et produit comme nouveau but la contradiction false.

En toute rigueur il ne faut pas confondre le raisonnement par l'absurde et la démonstration d'une négation (qui se termine aussi par une contradiction, mais sans utiliser le principe du tiers exclu). Mais les mathématiciens sont souvent négligents et écrivent les mots « raisonnement par l'absurde » dans les deux cas. Il s'agit d'un abus de langage inoffensif dans la mesure où le principe du tiers exclu permet d'introduire et de retirer des doubles négations librement.

En cas d'hésitation entre l'utilisation des commandes exfalso et by_contradiction, il faut se souvenir exfalso n'est à utiliser que quand le contexte est manifestement incohérent, indépendamment du but à démontrer. En effet elle ne conserve aucune trace du but, alors que le raisonnement par l'absurde initié par by_contradiction h ajoute au contexte une hypothèse h affirmant la négation du but.

Une autre incarnation classique du principe du tiers exclu est la démonstration par disjonction de cas. Étant donné un énoncé $Q$ à démontrer et un énoncé auxiliaire $P$, on démontre $Q$ d'abord en supposant que $P$ est vrai puis en supposant que $P$ est faux. Puisque le principe du tiers exclu assure qu'il n'y a pas d'autre alternative pour $P$, on a bien démontré $Q$. La commande Lean qui déclenche une disjonction de cas selon la véracité d'un énoncé $P$ est by_cases hP : P. Cette commande provoque un embranchement dans la démonstration. La première branche suppose hP : P et la seconde suppose hP : ¬ P (le nom hP de ces hypothèses est choisi librement par l'auteur de la démonstration). On reconnaît bien dans cet embranchement l'effet de l'utilisation de P ∨ ¬ P.

Exemple

Soit $P$, $Q$ et $R$ trois énoncés tels que $P$ implique $R$, $\mathrm{non} P$ implique $Q$ et $Q$ implique $R$. Montrons que $R$ est vrai.

example (P Q R : Prop) (hPR : P → R) (hPQ : ¬ P → Q) (hQR : Q → R) : R :=
Démonstration
On distingue suivant que $P$ est vrai ou pas. 
  by_cases hP : P,

P Q R : Prop,
hPR : P → R,
hPQ : ¬P → Q,
hQR : Q → R
⊢ R

2 goals
P Q R : Prop,
hPR : P → R,
hPQ : ¬P → Q,
hQR : Q → R,
hP : P
⊢ R

P Q R : Prop,
hPR : P → R,
hPQ : ¬P → Q,
hQR : Q → R,
hP : ¬P
⊢ R
Supposons d'abord que $P$ est vrai. On obtient alors la conclusion via l'implication $P ⇒ R$ 
    exact hPR hP,

2 goals
P Q R : Prop,
hPR : P → R,
hPQ : ¬P → Q,
hQR : Q → R,
hP : P
⊢ R

P Q R : Prop,
hPR : P → R,
hPQ : ¬P → Q,
hQR : Q → R,
hP : ¬P
⊢ R

P Q R : Prop,
hPR : P → R,
hPQ : ¬P → Q,
hQR : Q → R,
hP : ¬P
⊢ R
Si au contraire $P$ est faux. On obtient $Q$ via l'implication $¬ P ⇒ Q$ 
    have hQ : Q, exact hPQ hP,

P Q R : Prop,
hPR : P → R,
hPQ : ¬P → Q,
hQR : Q → R,
hP : ¬P
⊢ R

P Q R : Prop,
hPR : P → R,
hPQ : ¬P → Q,
hQR : Q → R,
hP : ¬P,
hQ : Q
⊢ R
Puis $R$ via l'implication $Q ⇒ R$ 
    exact hQR hQ,

P Q R : Prop,
hPR : P → R,
hPQ : ¬P → Q,
hQR : Q → R,
hP : ¬P,
hQ : Q
⊢ R

no goals
QED.

Reformulations de l'implication

La notion de négation et le principe du tiers exclu rendent possibles plusieurs reformulations des implications.

La plus importante est sans doute le principe de contraposition, qui affirme que, pour tous énoncés $P$ et $Q$, l'implication $P ⇒ Q$ est équivalente à l'implication dite contraposée : $¬ Q ⇒ ¬ P$, qui est parfois plus facile à démontrer directement. Il ne faut pas confondre la contraposée $¬ Q ⇒ ¬ P$ avec la réciproque $Q ⇒ P$ qui est un énoncé n'ayant en général aucun lien logique avec $P ⇒ Q$.

Exemple

Soit $P$ et $Q$ deux énoncés. Montrons le principe de contraposition : $P$ implique $Q$ si et seulement si $\mathrm{non} Q$ implique $\mathrm{non} P$.

example (P Q : Prop) : (P → Q) ↔ (¬ Q → ¬ P) :=
Démonstration
On démontre successivement les deux implications. 
  split,

P Q : Prop
⊢ P → Q ↔ ¬Q → ¬P

2 goals
P Q : Prop
⊢ (P → Q) → ¬Q → ¬P

P Q : Prop
⊢ (¬Q → ¬P) → P → Q
Supposons d'abord que $P$ implique $Q$. 
    intro hPQ,

2 goals
P Q : Prop
⊢ (P → Q) → ¬Q → ¬P

P Q : Prop
⊢ (¬Q → ¬P) → P → Q

2 goals
P Q : Prop,
hPQ : P → Q
⊢ ¬Q → ¬P

P Q : Prop
⊢ (¬Q → ¬P) → P → Q
Montrons $¬ Q ⇒ ¬ P$. Pour cela, supposons que $Q$ est faux. 
    intro hnQ,

2 goals
P Q : Prop,
hPQ : P → Q
⊢ ¬Q → ¬P

P Q : Prop
⊢ (¬Q → ¬P) → P → Q

2 goals
P Q : Prop,
hPQ : P → Q,
hnQ : ¬Q
⊢ ¬P

P Q : Prop
⊢ (¬Q → ¬P) → P → Q
On doit montrer que $P$ est faux, donc on suppose $P$ vrai et on cherche une contradiction. 
    intro hP,

2 goals
P Q : Prop,
hPQ : P → Q,
hnQ : ¬Q
⊢ ¬P

P Q : Prop
⊢ (¬Q → ¬P) → P → Q

2 goals
P Q : Prop,
hPQ : P → Q,
hnQ : ¬Q,
hP : P
⊢ false

P Q : Prop
⊢ (¬Q → ¬P) → P → Q
On observe que $Q$ est vrai car on a supposé que $P ⇒ Q$ et $P$ sont vrais. 
    have hQ : Q,

2 goals
P Q : Prop,
hPQ : P → Q,
hnQ : ¬Q,
hP : P
⊢ false

P Q : Prop
⊢ (¬Q → ¬P) → P → Q

3 goals
P Q : Prop,
hPQ : P → Q,
hnQ : ¬Q,
hP : P
⊢ Q

P Q : Prop,
hPQ : P → Q,
hnQ : ¬Q,
hP : P,
hQ : Q
⊢ false

P Q : Prop
⊢ (¬Q → ¬P) → P → Q

      exact hPQ hP,

3 goals
P Q : Prop,
hPQ : P → Q,
hnQ : ¬Q,
hP : P
⊢ Q

P Q : Prop,
hPQ : P → Q,
hnQ : ¬Q,
hP : P,
hQ : Q
⊢ false

P Q : Prop
⊢ (¬Q → ¬P) → P → Q

2 goals
P Q : Prop,
hPQ : P → Q,
hnQ : ¬Q,
hP : P,
hQ : Q
⊢ false

P Q : Prop
⊢ (¬Q → ¬P) → P → Q
On a donc une contradiction avec l'hypothèse que $Q$ est faux. 
    exact hnQ hQ,

2 goals
P Q : Prop,
hPQ : P → Q,
hnQ : ¬Q,
hP : P,
hQ : Q
⊢ false

P Q : Prop
⊢ (¬Q → ¬P) → P → Q

P Q : Prop
⊢ (¬Q → ¬P) → P → Q
Réciproquement, supposons $¬ Q ⇒ ¬ P$. 
    intro hnQnP,

P Q : Prop
⊢ (¬Q → ¬P) → P → Q

P Q : Prop,
hnQnP : ¬Q → ¬P
⊢ P → Q
Montrons $P ⇒ Q$. Pour cela, supposons que $P$ est vrai. 
    intro hP,

P Q : Prop,
hnQnP : ¬Q → ¬P
⊢ P → Q

P Q : Prop,
hnQnP : ¬Q → ¬P,
hP : P
⊢ Q
Supposons par l'absurde que $Q$ est faux, et montrons une contradiction. 
    by_contradiction hnQ,

P Q : Prop,
hnQnP : ¬Q → ¬P,
hP : P
⊢ Q

P Q : Prop,
hnQnP : ¬Q → ¬P,
hP : P,
hnQ : ¬Q
⊢ false
L'hypothèse $¬ Q ⇒ ¬ P$ montre alors que $P$ aussi est faux. 
    have hnP : ¬ P,

P Q : Prop,
hnQnP : ¬Q → ¬P,
hP : P,
hnQ : ¬Q
⊢ false

2 goals
P Q : Prop,
hnQnP : ¬Q → ¬P,
hP : P,
hnQ : ¬Q
⊢ ¬P

P Q : Prop,
hnQnP : ¬Q → ¬P,
hP : P,
hnQ : ¬Q,
hnP : ¬P
⊢ false

      exact hnQnP hnQ,

2 goals
P Q : Prop,
hnQnP : ¬Q → ¬P,
hP : P,
hnQ : ¬Q
⊢ ¬P

P Q : Prop,
hnQnP : ¬Q → ¬P,
hP : P,
hnQ : ¬Q,
hnP : ¬P
⊢ false

P Q : Prop,
hnQnP : ¬Q → ¬P,
hP : P,
hnQ : ¬Q,
hnP : ¬P
⊢ false
Mais ce dernier résultat contredit notre hypothèse que $P$ est vrai. 
    exact hnP hP,

P Q : Prop,
hnQnP : ¬Q → ¬P,
hP : P,
hnQ : ¬Q,
hnP : ¬P
⊢ false

no goals
QED.

On notera au passage que seule la deuxième implication de la démonstration ci-dessus utilise le principe du tiers exclu. La première se contente d'utiliser la définition de la négation. Ainsi les deux implications se démontrent en obtenant une contradiction mais, stricto sensu, seule la deuxième est une démonstration par l'absurde.

Bien sûr il est inutile de redémontrer ce principe de contraposée à chaque utilisation. Dans Lean, on peut transformer un but d'implication $P ⇒ Q$ en sa contraposée $¬ Q ⇒ ¬ P$ à l'aide de la commande contrapose.

Il est également possible de réécrire l'implication $P ⇒ Q$ en terme de disjonction et de négation.

Exemple

Soit $P$ et $Q$ deux énoncés. Montrons que « $P ⇒ Q$ » est équivalent à « $\mathrm{non} P$ ou $Q$ ».

example (P Q : Prop) : (P → Q) ↔ (¬ P ∨ Q) :=
Démonstration
On démontre successivement les deux implications. 
  split,

P Q : Prop
⊢ P → Q ↔ ¬P ∨ Q

2 goals
P Q : Prop
⊢ (P → Q) → ¬P ∨ Q

P Q : Prop
⊢ ¬P ∨ Q → P → Q
Supposons d'abord $P ⇒ Q$. 
    intro h,

2 goals
P Q : Prop
⊢ (P → Q) → ¬P ∨ Q

P Q : Prop
⊢ ¬P ∨ Q → P → Q

2 goals
P Q : Prop,
h : P → Q
⊢ ¬P ∨ Q

P Q : Prop
⊢ ¬P ∨ Q → P → Q
On distingue selon que $P$ est vrai ou faux (en utilisant le principe du tiers exclu). 
    by_cases hP : P,

2 goals
P Q : Prop,
h : P → Q
⊢ ¬P ∨ Q

P Q : Prop
⊢ ¬P ∨ Q → P → Q

3 goals
P Q : Prop,
h : P → Q,
hP : P
⊢ ¬P ∨ Q

P Q : Prop,
h : P → Q,
hP : ¬P
⊢ ¬P ∨ Q

P Q : Prop
⊢ ¬P ∨ Q → P → Q
Si $P$ est vrai, on va montrer que $Q$, et donc « $\mathrm{non} P$ ou $Q$ », est vrai. 
      right,

3 goals
P Q : Prop,
h : P → Q,
hP : P
⊢ ¬P ∨ Q

P Q : Prop,
h : P → Q,
hP : ¬P
⊢ ¬P ∨ Q

P Q : Prop
⊢ ¬P ∨ Q → P → Q

3 goals
P Q : Prop,
h : P → Q,
hP : P
⊢ Q

P Q : Prop,
h : P → Q,
hP : ¬P
⊢ ¬P ∨ Q

P Q : Prop
⊢ ¬P ∨ Q → P → Q
Cela découle de l'hypothèse $P ⇒ Q$ et de l'hypothèse que $P$ est vrai. 
      exact h hP,

3 goals
P Q : Prop,
h : P → Q,
hP : P
⊢ Q

P Q : Prop,
h : P → Q,
hP : ¬P
⊢ ¬P ∨ Q

P Q : Prop
⊢ ¬P ∨ Q → P → Q

2 goals
P Q : Prop,
h : P → Q,
hP : ¬P
⊢ ¬P ∨ Q

P Q : Prop
⊢ ¬P ∨ Q → P → Q
Si au contraire $P$ est faux, on a directement le membre de gauche de « $\mathrm{non} P$ ou $Q$ ». 
        left,

2 goals
P Q : Prop,
h : P → Q,
hP : ¬P
⊢ ¬P ∨ Q

P Q : Prop
⊢ ¬P ∨ Q → P → Q

2 goals
P Q : Prop,
h : P → Q,
hP : ¬P
⊢ ¬P

P Q : Prop
⊢ ¬P ∨ Q → P → Q

        exact hP,

2 goals
P Q : Prop,
h : P → Q,
hP : ¬P
⊢ ¬P

P Q : Prop
⊢ ¬P ∨ Q → P → Q

P Q : Prop
⊢ ¬P ∨ Q → P → Q
Réciproquement, supposons que « $\mathrm{non} P$ ou $Q$ » est vrai. 
    intro h,

P Q : Prop
⊢ ¬P ∨ Q → P → Q

P Q : Prop,
h : ¬P ∨ Q
⊢ P → Q
On veut montrer que $P$ implique $Q$. Supposons donc $P$. 
    intro hP,

P Q : Prop,
h : ¬P ∨ Q
⊢ P → Q

P Q : Prop,
h : ¬P ∨ Q,
hP : P
⊢ Q
On a supposé que soit $P$ est faux soit $Q$ est vrai. 
    cases h with hnP hQ,

P Q : Prop,
h : ¬P ∨ Q,
hP : P
⊢ Q

2 goals
case or.inl
P Q : Prop,
hP : P,
hnP : ¬P
⊢ Q

case or.inr
P Q : Prop,
hP : P,
hQ : Q
⊢ Q
Dans le premier cas, on obtient $Q$ comme on obtiendrait n'importe quoi car nos hypothèses sont contradictoires. 
      exfalso,

2 goals
case or.inl
P Q : Prop,
hP : P,
hnP : ¬P
⊢ Q

case or.inr
P Q : Prop,
hP : P,
hQ : Q
⊢ Q

2 goals
P Q : Prop,
hP : P,
hnP : ¬P
⊢ false

case or.inr
P Q : Prop,
hP : P,
hQ : Q
⊢ Q
En effet on a supposé à la fois non $P$ et $P$. 
      exact hnP hP,

2 goals
P Q : Prop,
hP : P,
hnP : ¬P
⊢ false

case or.inr
P Q : Prop,
hP : P,
hQ : Q
⊢ Q

case or.inr
P Q : Prop,
hP : P,
hQ : Q
⊢ Q
Dans le deuxième cas on a directement $Q$. 
      exact hQ,

case or.inr
P Q : Prop,
hP : P,
hQ : Q
⊢ Q

no goals
QED.

Ainsi la notion de négation étend notablement les possibilités de démonstration d'une implication $P ⇒ Q$ en ajoutant des démonstrations indirectes, qui ne commencent pas par « Supposons $P$ ». C'est évidemment une richesse mais aussi une difficulté car cela nécessite de prendre des décisions stratégiques durant l'élaboration d'une démonstration, plutôt que de se laisser guider complètement par la forme de l'énoncé.

De même on peut démontrer, en utilisant le principe du tiers-exclu, que « $P$ ou $Q$ » est vrai si et seulement si $¬ P$ implique $Q$ (ou encore si et seulement si $¬ Q$ implique $P$). On obtient ainsi deux nouvelles stratégies pour démontrer une disjonction.

Négation des conjonctions, disjonctions et énoncés quantifiés

Avec le même type de démonstration, on obtient sans peine les lois de de Morgan : la négation de « $P$ et $Q$ » est équivalente à « $\mathrm{non} P$ ou $\mathrm{non} Q$ », et la négation de « $P$ ou $Q$ » est équivalente à « $\mathrm{non} P$ et $\mathrm{non} Q$ ». On notera que ces deux résultats se déduisent aisément l'un de l'autre via l'élimination des doubles négations. Comme toujours la symétrie parfaite ainsi obtenue nécessite le principe du tiers exclu pour certaines implications.

En combinant ces lois de de Morgan avec l'équivalence $(P ⇒ Q) ⇔ (¬ P ∨ Q)$ démontré ci-dessus, on obtient une expression commode pour la négation de $P ⇒ Q$. En effet on obtient la succession d'énoncés équivalents : $¬ (P ⇒ Q)$, $¬ (¬ P ∨ Q)$, $¬ ¬ P ∧ ¬ Q$, et enfin $P ∧ ¬ Q$, donc la négation de $P ⇒ Q$ est équivalente à $P \text{ et non } Q$. Bien sûr cette démonstration utilise le principe du tiers exclu, sans lequel seule l'implication $(P \text{ et non } Q) ⇒ \text{ non }(P ⇒ Q)$ est démontrable.

En voyant les énoncés quantifiés universellement comme de grandes conjonctions et les énoncés quantifiés existentiellement comme de grandes disjonctions, on a l'intuition de la façon de « pousser les négations à l'intérieur des quantificateurs » : pour tout prédicat $P$, on a $¬ (∀ x, P x) ⇔ ∃ x, ¬ P x$ et $¬ (∃ x, P x) ⇔ ∀ x, ¬ P x$.

Dans le cadre logique de ce chapitre, on peut démontrer ces résultats de négation des énoncés quantifiés, cela sera fait en TP. De telles démonstrations ne sont pas accessibles par la méthode dite des « tables de vérités ». Cette méthode consiste à démontrer l'équivalence de deux énoncés combinant un nombre fini d'énoncés $P_1, \dots, P_N$ non quantifiés en appliquant indistinctement le principe du tiers exclu à tous les $P_i$ jusqu'à obtenir une disjonction de $2^N$ cas. L'analogue pour un énoncé quantifié sur $x$ parcourant un ensemble infini conduirait à une infinité de cas à discuter… Bien sûr on peut se contenter d'ajouter les règles de négations des énoncés quantifiés comme axiomes logiques. En pratique on utilise ces règles sans discuter pour savoir si elles ont été démontrées ou sont des axiomes.

Un problème nettement plus pertinent en pratique est de comprendre la négation des quantifications bornées, comme par exemple $∀ ε > 0,\; P\, ε$ ou bien $∀ x ∈ [0, 1],\; P\,x$, et leurs analogues existentiels. Pour cela il faut se souvenir que, par définition, $∀ ε > 0,\; P\, ε$ signifie $∀ ε, ε > 0 ⇒ P\, ε$. On peut donc nier cet énoncé en utilisant les règles de négation du quantificateur $∀$ et de l'implication. On obtient $¬ (∀ ε, ε > 0 ⇒ P\, ε) ⇔ (∃ ε, ¬ (ε > 0 ⇒ P \, ε)) ⇔ (∃ ε, ε > 0 ∧ ¬ P ε) ⇔ (∃ ε > 0, ¬ P\, ε)$, la dernière équivalence étant la définition de la notation $∃ ε > 0$. Le point à noter attentivement est que l'inégalité n'est pas niée. On démontre par un raisonnement analogue que $¬ (∃ ε > 0, P\, ε) ⇔ (∀ ε > 0, ¬ P\, ε)$. Bien sûr les mêmes remarques s'appliquant à $∀ x ∈ A, P\, x$ dont la négation est $∃ x ∈ A, ¬ P\, x$, sans nier l'appartenance.

On verra en TP comment appliquer ces règles pour écrire la négation d'un énoncé tel que « la suite $u$ tend vers $l$ » (qui ne saurait être « la limite de u est différente de $l$ » car il existe des suites n'ayant pas de limite du tout !). En attendant, voici un tableau récapitulatif des équivalences discutées dans ce chapitre ou dans le TP correspondant. Bien que, ainsi qu'on l'a vu, on puisse démontrer ces énoncés en revenant aux bases, il est bien plus efficace de les connaître par cœur.

Dans Lean, la commande push_neg permet de pousser les négations du but vers l'intérieur des formules, en utilisant les règles ci-dessus. On peut faire de même dans une hypothèse h à l'aide de push_neg at h. Dans les deux cas, il faut que les quantificateurs et connecteurs logiques soient visibles dans la formule. On utilisera unfold ou change pour les faire apparaître si besoin. La suite de commande très commune contrapose, push_neg peut être abrégée en contrapose! mais, au moins au début, il peut être instructif de séparer les deux opérations et bien étudier l'évolution du but à chaque instruction.