Principe du tiers exclu

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] <ref>Modèle:Ouvrage.</ref>, 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, Modèle:Citation bloc

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.

En philosophie

Dans sa Métaphysique, Aristote introduit le principe du tiers exclu comme complément du principe de non-contradiction<ref>Aristote, Métaphysique, Livre Γ.</ref>.

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é) Modèle:Refnec 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.

Histoire du tiers-exclu en philosophie

Parménide utilise implicitement le principe du tiers exclu. Modèle:Citation bloc

Aristote le mentionne, le premier, avec clarté : Modèle:Citation bloc

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

Les « logiques polyvalentes » mettent en question le principe dès Lukasiewicz en 1910<ref>Jan Lukasiewicz, Sur le principe de contradiction chez Aristote, 1010.</ref>, 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<ref>Gilbert Hottois, Penser la logique, De Boeck Université, Bruxelles, 1989, p. 116.</ref>. Une proposition peut être absurde ou probable, et non seulement vraie ou fausse.

Brouwer puis Arend Heyting en 1930<ref>Arend Heyting, 1930C, « Sur la logique intuitionniste », Académie Royale de Belgique, Bulletin de la Classe des Sciences, 1930, 16, p. 957–963.</ref>, 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

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

En logique, le principe du tiers exclu est équivalent à l'implication de la double négation <math>\neg(\neg p) \Rightarrow p</math>, 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

<math> \frac{\neg \phi \vdash \bot}{\phi}</math>

où <math> \Gamma \vdash \phi</math> signifie de l'ensemble <math> \Gamma</math> de propositions je déduis <math>\phi</math> et <math> \bot</math> 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<ref>Modèle:Article, Section 3.2</ref><ref>Modèle:Article </ref>.

Logique intuitionniste et tiers exclu

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 premier exemple

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

<math>\forall a,b \in \mathbb R, ab=0 \Rightarrow a=0 \ {\rm ou}\ b=0</math>

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<ref>En effet, un mathématicien intuitionniste parle en termes de démonstration, pas en termes de vérité.</ref> :

• 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 <math>\phi</math> ou <math>\psi</math>, il faut soit avoir une démonstration de <math>\phi</math>, soit avoir une démonstration de <math>\psi</math>.

Un deuxième exemple

On se propose de démontrer que « Il existe des nombres irrationnels Modèle:Mvar et Modèle:Mvar, tels que Modèle:Mvar est rationnel ». Considérons la démonstration suivante<ref>Modèle:Article.</ref><ref>Modèle:Article.</ref><ref>Modèle:Ouvrage.</ref> :

« On sait que [[Racine carrée de deux#Preuves d'irrationalité|Modèle:Sqrt est irrationnel]] et que 2 est rationnel. Notons Modèle:Mvar la proposition « Modèle:Sqrt^Modèle:Sqrt est rationnel ». Appliquons le tiers exclu : Modèle:Mvar est vraie ou Modèle:Mvar est fausse.

• si Modèle:Mvar est vraie alors les irrationnels <math>a=\sqrt2</math> et <math>b=\sqrt2</math> conviennent ;

• si Modèle:Mvar est fausse alors les irrationnels <math>a= \sqrt2^{\sqrt2}</math> et <math>b=\sqrt2</math> conviennent, puisque <math>a^b=(\sqrt2^{\sqrt2})^{\sqrt2}=\sqrt2^{\sqrt2\times\sqrt2}=\sqrt2^2=2</math> 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 Modèle:Mvar est vraie ou fausse). En fait, Modèle:Mvar est faux car d'après le théorème de Gelfond-Schneider, Modèle:Sqrt^Modèle:Sqrt est même transcendant.

Formulations équivalentes

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 :

• <math> \neg \neg p \Rightarrow p</math>, élimination de la double négation,
• <math> ((p \Rightarrow q) \Rightarrow p) \Rightarrow p </math>, loi de Peirce,
• <math> (p \Rightarrow q) \Rightarrow (\neg p \vee q) </math>, implication vue comme une disjonction,
• <math> \neg (\neg p \wedge \neg q) \Rightarrow (p \vee q)</math>, loi de De Morgan.
• <math> (\neg p \Rightarrow \neg q) \Rightarrow (q \Rightarrow p)</math>, contraposition.

En revanche, la proposition <math> (p \Rightarrow q) \vee (q \Rightarrow p)</math>, est une tautologie (classique), non démontrable en logique intuitionniste, et plus faible que le tiers-exclu.

Voir aussi

Articles connexes

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

Bibliographie

• 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.
• Modèle:Ouvrage