En logique formelle, le principe du tiers exclu (ou "principium medii exclusi" [principe du milieu exclu] ou " tertium non datur" [une troisième possibilité n'est pas accordée] ^[1], ou simplement le « tiers exclu ») énonce qu'ou bien une proposition est vraie, ou bien sa négation est vraie. Par exemple, Socrate est vivant ou mort, et il n'y a pas de cas intermédiaire entre ces deux états de Socrate, c'est pourquoi on parle de « tiers-exclu » : tous les autres cas de figure sont nécessairement exclus. C'est un des principes de la logique classique. Au début de la formalisation des mathématiques, ce principe a été tenu comme un dogme intangible. D'ailleurs, David Hilbert, un de ses grands défenseurs, a écrit,

« Priver le mathématicien du tertium non datur [pas de troisième possibilité] serait enlever son télescope à l'astronome, son poing au boxeur^[2]. »

Le tiers-exclu est souvent comparé au principe de non-contradiction qui affirme que les propositions p et non-p ne peuvent être simultanément vraies, c'est-à-dire que la conjonction « p et non-p » est nécessairement fausse.

Dans sa Métaphysique, Aristote introduit le principe du tiers exclu comme complément du principe de non-contradiction^[3].

En philosophie, le principe du tiers exclu, comme le principe d'identité, a une double version, ontologique ou logique. La version ontologique rejette la notion de gradation dans l'être : il y a être, ou non-être, pas de demi-être.

Parmi les deux propositions p et non-p (ou toute autre paire de propositions), en l'absence de système de logique formelle, on pourrait en théorie avoir l'un des trois cas suivants :

1. p est vraie ou non-p est vraie, exclusivement ;
2. p et non-p sont toutes deux vraies ;
3. ni p ni non-p ne sont vraies.

Le principe de non-contradiction qui fonde la logique formelle rejette le cas 2 pour une paire de propositions qui sont la négation logique l'une de l'autre : on ne peut penser p et non-p vraies à la fois. Le principe du tiers-exclu rejette le cas 3 : on ne peut penser que p ou non-p, il n'y a pas de troisième cas hypothétique.

La « loi de l'alternative » (Robert Blanché) ^{[réf. nécessaire]} résulte de la conjonction du principe de non-contradiction et du principe du tiers exclu. À eux deux, ces principes participent à fonder la logique mathématique formelle dite classique. La logique intuitionniste, quant à elle, n'inclut pas le principe du tiers-exclu.

Parménide utilise implicitement le principe du tiers exclu.

« Il [l'être] est absolument ou il n’est pas du tout^[4]. »

Aristote le mentionne, le premier, avec clarté :

« Il n'est pas possible qu'il y ait aucun intermédiaire entre les énoncés contradictoires : il faut nécessairement ou affirmer ou nier un seul prédicat, quel qu'il soit^[5]. »

Kant, dans sa Logique (1800), lie principe du tiers exclu et problèmes apodictiques (nécessaires).

« Nous pouvons poser ici trois principes comme critères universels de la vérité, simplement formels et logiques, ce sont : 1) le principe de contradiction et d'identité (principium contradictionis et identitatis) par lequel la possibilité interne d'une connaissance est déterminée pour des jugements problématiques, 2) le principe de raison suffisante (principium rationis sufficientis) […] pour les jugements assertoriques ; le principe du tiers exclu (principium exclusi medii inter duo contradictoria) […] pour des jugements apodictiques. […] Les jugements sont problématiques, assertoriques ou apodictiques. Les jugements problématiques sont accompagnés de la conscience de la simple possibilité, les assertoriques de la conscience de la réalité, les apodictiques enfin de la conscience de la nécessité du jugement^[6]. »

Les « logiques polyvalentes » mettent en question le principe dès Lukasiewicz en 1910^[7], qui revient à l'antique question des « futurs contingents » : si une proposition qui concerne le futur pouvait être caractérisée au présent déjà comme vraie ou fausse, on devrait admettre que le cours des événements est déterminé à l'avance. Les logiques polyvalentes contestent le principe du tiers exclu. Elles reconnaissent d'autres valeurs que le vrai et le faux, elles admettent, entre les deux, l'indéterminé, ou le possible, ou, en deçà, l'impossible (qui est un faux renforcé), et au-delà le nécessaire (degré supérieur du vrai). Heyting ne dit pas que le tiers exclu est faux, il en limite la portée^[8]. Une proposition peut être absurde ou probable, et non seulement vraie ou fausse.

Brouwer puis Arend Heyting en 1930^[9], en tant qu'intuitionnistes, critiquent les raisonnements fondés sur le tiers exclu. Ils estiment qu'on n'a pas le droit d'inférer une proposition de l'absence de démonstration de sa négation. Leur position est adoptée par les logiciens spécialistes de la théorie des types, assez nombreux, avec le développement de l'informatique.

En mathématiques, le principe du tiers exclu affirme la disjonction « ${\displaystyle \phi }$ ou (non ${\displaystyle \phi }$) », pour toute proposition ${\displaystyle \phi }$. Cela signifie que pour toute proposition ${\displaystyle \phi }$, on doit accepter soit ${\displaystyle \phi }$, soit sa négation.

En logique, le principe du tiers exclu est équivalent à l'implication de la double négation ${\displaystyle \neg \neg p\to p}$, au sens que l'un se déduit de l'autre. Comme la double négation, le raisonnement par l'absurde est équivalent au 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. Plus formellement

${\displaystyle {\frac {\neg \phi \vdash \bot }{\phi }}}$

où ${\displaystyle \Gamma \vdash \phi }$ signifie de l'ensemble ${\displaystyle \Gamma }$ de propositions je déduis ${\displaystyle \phi }$ et ${\displaystyle \bot }$ représente la contradiction. Quand le tiers-exclus est mis en œuvre dans un assistant de preuve, on parle de réflexion booléenne, c'est un concept clé de la démonstration du théorème de Feit-Thompson^[10],[11].

La logique intuitionniste ne stipule pas le « principe » du tiers exclu. Autrement dit, le tiers exclu n'est pas un dogme en logique intuitionniste. En revanche, on peut montrer en logique intuitionniste que le tiers exclu est irréfutable, c'est-à-dire qu'admettre sa négation aboutirait à une contradiction. Dit autrement, la négation du tiers-exclu n'est pas démontrable en logique intuitionniste.

Un exemple de raisonnement faisant appel au tiers-exclu est le suivant :

${\displaystyle \forall a,b\in \mathbb {R} ,ab=0\Rightarrow a=0\ {\rm {ou}}\ b=0}$

Pour cela, appelons R la proposition « a=0 » et utilisons 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 vraie ;
• 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 reformulera le raisonnement précédent en termes de démonstrations^[12] :

• soit il y a une démonstration de R, alors un il y a une démonstration de « R ou b=0 »
• soit il n'y a pas de démonstration de R, mais cette absence de démonstration ne nous fournit pas une démonstration de « b= 0 ».

Le mathématicien intuitionniste refusera de conclure qu'il a une démonstration de a=0 ou b=0, parce qu'il ne peut pas exhiber une démonstration de a=0 ou une démonstration de non(a=0) ».

D'ailleurs, en logique intuitionniste, pour démontrer ${\displaystyle \phi }$ ou ${\displaystyle \psi }$, il faut soit avoir une démonstration de ${\displaystyle \phi }$, soit avoir une démonstration de ${\displaystyle \psi }$.

On se propose de démontrer que « Il existe des nombres irrationnels a et b, tels que a^b est rationnel ». Considérons la démonstration suivante^{[13],[14],[15]} :

« On sait que √2 est irrationnel et que 2 est rationnel. Notons φ la proposition « √2^√2 est rationnel ». Appliquons le tiers exclu : φ est vraie ou φ est fausse.

• si φ est vraie alors les irrationnels ${\displaystyle a={\sqrt {2}}}$ et ${\displaystyle b={\sqrt {2}}}$ conviennent ;

• si φ est fausse alors les irrationnels ${\displaystyle a={\sqrt {2}}^{\sqrt {2}}}$ et ${\displaystyle b={\sqrt {2}}}$ conviennent, puisque ${\displaystyle a^{b}=({\sqrt {2}}^{\sqrt {2}})^{\sqrt {2}}={\sqrt {2}}^{{\sqrt {2}}\times {\sqrt {2}}}={\sqrt {2}}^{2}=2}$ est rationnel ».

Cette démonstration n'est pas constructive ; en effet, de par son utilisation du tiers exclu, elle n'exhibe pas une solution explicite, mais démontre seulement l'existence d'un couple-solution sans pouvoir préciser lequel (puisqu'on ne sait pas si φ est vraie ou fausse). En fait, φ est faux car d'après le théorème de Gelfond-Schneider, √2^√2 est même transcendant.

Nous avons vu plus haut des formulations équivalant au tiers exclu, mais ce ne sont pas les seules. Voici des formulations équivalant au tiers-exclu, parmi les plus connues :

• ${\displaystyle \neg \neg p\to p}$, élimination de la double négation,
• ${\displaystyle ((p\to q)\to p)\to p}$, loi de Peirce,
• ${\displaystyle (p\to q)\to (\neg p\vee q)}$, implication vue comme une disjonction,
• ${\displaystyle \neg (\neg p\wedge \neg q)\to (p\vee q)}$, loi de De Morgan.
• ${\displaystyle (\neg p\to \neg q)\to (q\to p)}$, contraposition.

En revanche, la proposition ${\displaystyle (p\to q)\vee (q\to p)}$, est une tautologie (classique), non démontrable en logique intuitionniste, et plus faible que le tiers-exclu.

• Analyse constructive
• Consequentia mirabilis
• Loi de Peirce
• Non-sens
• Principe de bivalence
• Principe de non-contradiction
• Principe d'identité
• Tétralemme
• Trichotomie

• Robert Blanché, La science actuelle et le rationalisme, PUF, 1967, p. 91-93.
• Jean-Baptiste Gourinat, « Principe de contradiction, principe du tiers-exclu et principe de bivalence : philosophie première ou organon ? », dans M. Bastit, J. Follon (éds.), Logique et métaphysique dans l’Organon d’Aristote, Actes du colloque de Dijon, Louvain, Peeters, 2001, p. 63-91.
• René David, Karim Nour et Christophe Raffalli, Introduction à la logique. Théorie de la démonstration. Cours et exercices corrigés, Paris, Dunod, 2001, 352 p. (ISBN 2-10-006796-6)

• Portail de la logique
• Portail de la philosophie