# Loi de Peirce

En logique, la loi de Peirce est la proposition $((A\to B)\to A)\to A$ où $\to$ désigne l'implication. Elle a été proposée par le logicien et philosophe Charles Sanders Peirce.
Cette formule, valide en logique classique, est invalide en logique intuitionniste. Cela signifie que, bien que ne possédant pas de référence explicite à la négation, la loi de Peirce est directement liée à la façon dont on traite celle-ci. Ainsi, on peut montrer que, en logique intuitionniste, il y a équivalence entre loi de Peirce, règle d'élimination de la double négation ou principe du tiers exclu. L'ajout d'un seul de ces principes à la logique intuitionniste redonne la totalité de la logique classique.

## Démonstration de la loi de Peirce en logique classique

L'un des principes de la logique classique est le raisonnement par l'absurde. Pour montrer une proposition $A$, on suppose que $A$ est faux. Si on aboutit à une contradiction, alors on déduit $A$.
Pour montrer que l'implication $((A\to B)\to A)\to A$ est valide, nous allons donc supposer $((A\to B)\to A)$ et nous devons montrer que $A$ est vraie. Raisonnons par l'absurde et supposons que $A$ soit fausse. Mais si $A$ est fausse, par contre l'implication $A\to B$ est vraie. Comme on a supposé $((A\to B)\to A)$ et que l'hypothèse $A\to B$ est vraie, la conclusion $A$ est également vraie, d'où une contradiction.
On peut aussi la démontrer en se servant de quelques principes comme la contraposée, les lois de De Morgan et le principe du tiers exclu, également valides en logique classique. La loi de Peirce est en effet équivalente à :
$\left(\neg A\to \left(\left(A\to B\right)\wedge \neg A\right)\right)$
$\Leftrightarrow \left(\neg A\to \left(\left(\neg A\vee B\right)\wedge \neg A\right)\right)$
$\Leftrightarrow \left(\neg A\to \left(\neg A\vee \left(\neg A\wedge B\right)\right)\right)$
$\Leftrightarrow \left(A\vee \neg A\vee \left(\neg A\wedge B\right)\right)$
Ce qui est vrai selon le principe du tiers exclu $A\vee \neg A$.

## Logique intuitionniste et loi de Peirce

La loi de Peirce n'est pas valide en logique intuitionniste. La logique intuitionniste traite la négation de la façon suivante (on suppose le lecteur familier avec des notations qui sont précisées par exemple dans l'article calcul des propositions) :
* Si on a à la fois une proposition $A$ et sa négation $\lnot A$, alors on a une contradiction, notée $\bot$ (règle dite d'élimination de la négation) ;
* Si une proposition $A$ conduit à une contradiction, alors c'est que $\lnot A$ est valide (règle dite d'introduction de la négation). Dans ce sens, $\lnot A$ n'est rien d'autre qu'un synonyme de $A\to \bot$ ;
* Si un raisonnement conclut à une contradiction, alors on peut en déduire la validité de toute proposition (règle dite d'élimination de la contradiction).
Considérons alors les règles suivantes :
* Élimination de la double négation : $\lnot \lnot A\to A$
* Tiers exclu : $A\lor \lnot A$
* Contraposition : $(\lnot A\to \lnot B)\to (B\to A)$
Plaçons-nous dans le cadre de la logique intuitionniste (avec $\bot$, négation, disjonction et conjonction) et ajoutons à cette logique la loi de Peirce. Nous allons montrer que les trois règles précédentes sont valides et qu'on obtient la logique classique. Remarquons d'abord que, si on instancie la loi de Peirce en remplaçant $B$ par la proposition contradictoire $\bot$, on obtient la variante suivante $(\lnot A\to A)\to A$ (en se rappelant que $\lnot A$ est $A\to \bot$).
Preuve de l'élimination de la double négation : Soit l'hypothèse $\lnot \lnot A$. Supposons en outre $\lnot A$, on obtient une contradiction (une proposition et sa négation). Par la règle d'élimination de l'absurde (aussi appelée principe d'explosion, à ne pas confondre donc avec le raisonnement par l'absurde), on déduit $A$. Puisque de $\lnot A$ on déduit $A$, on en conclut l'implication $\lnot A\to A$ (introduction de l'implication). Appliquant la variante ci-dessus de la loi de Peirce, on en déduit la validité de $A$. On a donc montré que $\lnot \lnot A\to A$.
L'élimination de la double négation sous-tend le raisonnement par l'absurde. En effet, si $\lnot A$ conduit à une contradiction, alors on a $\lnot \lnot A$ par la règle d'introduction de la négation, et donc on a $A$ par élimination de la double négation. On a donc montré que l'adjonction de la loi de Peirce à la logique intuitionniste donne la logique classique.
Preuve du tiers exclu : c'est en fait une conséquence directe de l'élimination de la double négation ou du raisonnement par l'absurde. Si on a $\lnot (A\lor \lnot A)$ alors on a $\lnot A\land \lnot \lnot A$, ce qui est contradictoire. Donc on a $\lnot \lnot (A\lor \lnot A)$ et donc $A\lor \lnot A$ par élimination de la double négation.
Preuve de la contraposition : c'est également une conséquence de l'élimination de la double négation. Soit la proposition $\lnot A\to \lnot B$. Montrons que $B\to A$. Pour cela supposons $B$ et montrons $A$. Si on avait $\lnot A$, on aurait $\lnot B$, ce qui est contradictoire avec l'hypothèse. On a donc $\lnot \lnot A$, et par élimination de la double négation, on a $A$.