Un principe logique qui, pour toute proposition P, affirme que soit P est vraie soit sa négation ¬P est vraie, sans troisième possibilité (formalement : P ∨ ¬P).

Principe

Vérité binaire : les propositions sont considérées comme satisfaisant la bivalence, permettant des raisonnements reposant sur la dichotomie et l'argument indirect (p. ex. la preuve par l'absurde).

Démonstration

Exemple classique : en logique propositionnelle, la tautologie p ∨ ¬p tient dans la sémantique classique des valeurs de vérité. En mathématiques, de nombreuses preuves classiques l'utilisent pour conclure l'existence ou la vérité en excluant la négation (p. ex. preuves classiques de l'irrationalité par contradiction).

Mauvaise application

Employer la loi dans des contextes constructifs ou intuitionnistes pour prétendre à une existence ou produire des témoins explicites — supposer que P∨¬P implique la décidabilité de P — ou l'appliquer à des propositions à contingence future où la bivalence est contestée philosophiquement.

Conséquence

Permet les preuves indirectes, la simplification des dérivations logiques (élimination de la double négation) et soutient de nombreux métathéorèmes classiques (complétude du calcul propositionnel classique).

Inversion

Rejeter la loi conduit à la logique intuitionniste, où P∨¬P n'est pas généralement admis et les preuves doivent construire des témoins ou fournir des disjonctions constructives ; d'autres inversions incluent les logiques à plusieurs valeurs ou paraconsistantes qui admettent des lacunes ou des surcharges de valeurs de vérité.

Limite

Valable dans les logiques propositionnelle et des prédicats classiques qui supposent la bivalence ; non valable en tant que principe général en mathématiques constructives, dans certains contextes modaux ou dans des cadres paraconsistants. Elle affirme une dichotomie logique, pas une décidabilité algorithmique — P∨¬P n'implique pas une procédure effective pour décider P.

Tension sémantique

Tension entre la vérité classique (la loi comme affirmation métaphysique sur les valeurs de vérité) et les vues constructivistes/proof-théoriques (la vérité comme démontrabilité ou constructibilité). Tension aussi entre affirmer une dichotomie logique et préserver le contenu computationnel des preuves.

Synthèse

La loi du tiers exclu est la dichotomie classique selon laquelle toute proposition est vraie ou fausse ; elle est puissante pour les raisonnements indirects et la métathéorie classique, mais elle est restreinte ou rejetée dans les cadres exigeant un contenu constructif ou admettant des valeurs de vérité intermédiaires.