Principe du tiers exclu
Un article de Wikipédia, l'encyclopédie libre.
En mathématiques, le principe du tiers exclu affirme que la proposition « φ ou (non φ) » est vraie, pour toute proposition φ. Cela signifie que pour toute proposition φ, on doit accepter soit φ, soit sa négation.
Le principe du tiers exclu a été introduit par Aristote comme conséquence du principe de non-contradiction, alors que ces deux principes sont différents. Le principe de non contradiction stipule que pour toute proposition φ on ne peut pas avoir φ et non φ en même temps.
En logique classique, le principe du tiers exclu se déduit de l'élimination de la double négation ( non(non(R)) = R ) :
- non contradiction : non (R et (non(R)) <=> non(R) ou non(non(R)) <=> non(R) ou R (tiers exclu)
Ce n'est toutefois pas le cas dans tous les formalismes logiques, et en particulier en logique intuitionniste, qui conserve le principe de non-contradiction mais n'utilise pas le « principe » du tiers exclu. En logique intuitionniste, nous ne pouvons pas dire que « R ou (non R) » est vraie a priori pour toute proposition R, il faut le démontrer pour chaque proposition R (et, dans certains cas, cela sera impossible sans introduire un nouvel axiome). Pour un mathématicien intuitionniste, le principe du tiers exclu est au mieux inutile (pour les démonstrations qu'on pourrait faire sans l'utiliser), au pire stérilisant (il tranche des propositions indécidables, sans que cela résulte d'une décision consciente et délibérée, sachant qu'à chaque fois on peut créer plusieurs formalismes distincts et potentiellement féconds).
Un exemple de raisonnement faisant appel au tiers-exclu est le suivant: nous voulons démontrer l'implication
Pour cela, nous pouvons considérer la proposition R: « a=0 » et utiliser le principe du tiers exclu pour R. Il y a alors deux cas à examiner (un troisième cas étant exclu) :
- soit R est vraie: alors la proposition « R ou b=0 » est vérifiée
- soit R est fausse i.e. a≠0 alors en simplifiant par a la relation ab=0, nous obtenons b=0, et « R ou b=0 » est vérifiée.
Dans l'implication précédente, un mathématicien intuitionniste refusera de conclure que a=0 ou b=0, parce qu'il ne peut pas prouver que « a=0 ou non(a=0) » est vraie (l'égalité sur les réels étant indécidable).
Toutefois, la logique intuitionniste n'est pas fondamentalement plus faible que la logique classique : pour toute proposition R prouvable en logique classique, il existe une proposition R' (qui peut être identique à R) telle que R et R' sont équivalents au sens de la logique classique, et R' est prouvable en logique intuitionniste. Dans notre exemple, cette proposition R' serait « non(ab=0 et non(a=0) et non(b=0)) ».
Le raisonnement par l'absurde repose sur le principe du tiers exclu. En effet, il fonctionne sur le mécanisme suivant : je veux prouver R. Pour cela, je suppose « non(R) » et je tombe sur une contradiction : c'est donc que « non(R) » est fausse, et d'après le principe du tiers exclu, que « R » est vraie. En logique intuitionniste, cette dernière étape est impossible: de « non(R) » est fausse, on peut juste conclure « non(non(R)) » est vraie, mais ce n'est pas équivalent à « R » est vraie, comme en logique classique. On a juste l'implication 
, mais pas sa réciproque.
