Paradoxe du buveur

Le paradoxe du buveur (aussi connu comme le théorème du buveur, le principe du buveur) est un théorème de logique mathématique (prédicat) qui peut être énoncé ainsi :  

Il a été popularisé par le mathématicien logicien Raymond Smullyan, qui l'a appelé le  dans son livre de 1978 .

La nature apparemment paradoxale de l'énoncé tient à la façon dont il est habituellement formulé en langage naturel. Il semble contre-intuitif à la fois qu'il pourrait y avoir une personne qui fait boire les autres, ou qu'il pourrait y avoir une personne telle que, tout au long de la nuit, cette personne a toujours été la dernière à boire. La première objection vient de la confusion entre les énoncés formels « si alors » et la causalité (voir corrélation n'implique pas de lien de causalité ou logique de pertinence pour les logiques qui exigent des relations pertinentes entre prémisse et conséquences, contrairement à la logique classique présumée ici). L'énoncé formel du théorème est intemporel, éliminant la deuxième objection parce que la personne qui rend l'énoncé vrai à un instant n'est pas nécessairement la même personne à un autre instant.

La déclaration formelle du théorème est :

où D est un prédicat arbitraire et P est un ensemble non vide arbitraire.

Ceci découle de la formule valide du calcul des prédicats :

 (∃x Px ⇒ A) ⇔ ∀x (Px ⇒ A)

Preuves

Preuve informelle 
La preuve commence par la reconnaissance du fait que tout le monde dans le bar est en train de boire ou qu'au moins une personne dans le pub ne boit pas. Par conséquent, il y a deux cas à considérer :
 Supposons que tout le monde soit en train de boire. Pour une personne en particulier dans ce bar, il est vrai de dire que si cette personne en particulier boit, alors tout le monde dans le pub boit - parce que tout le monde est en train de boire.
 Sinon, au moins une personne ne boit pas. L'affirmation selon laquelle si cette personne en particulier boit, alors tout le monde dans le bar boit est formellement vraie : son antécédent (« cette personne en particulier est en train de boire ») est faux, donc la proposition est vraie en raison de l'implication logique en logique classique : « Si P, alors Q » est toujours vraie si P est fausse.

Une façon un peu plus formelle d'exprimer ce qui précède est de dire que, si tout le monde boit, alors n'importe qui peut être le témoin de la validité du théorème. Et si quelqu'un ne boit pas, alors l'individu non buveur peut être témoin de la validité du théorème.

Preuve formelle 

On a la déclaration formelle du théorème, en une formule logique du premier ordre : , et on veut montrer que cette formule est valide.

Soit  arbitraires. Montrons que . On veut donc trouver  tel que . On note  l’ensemble des clients qui boivent (c’est-à-dire les .

 Si , on a . Pour , , donc .
 Sinon, on prend . Alors, , donc on a l’implication .

Explication de paradoxe 
Le paradoxe est finalement fondé sur le tiers-exclus (tout le monde boit ou il existe une personne qui ne boit pas) et sur le principe de la logique formelle selon lequel l'énoncé  est vrai dès que A est faux, c'est-à-dire que toute déclaration découle d'une fausse déclaration (ex falso quodlibet).

Ce qui est important pour le paradoxe, c'est que l'implication logique  est équivalente, en logique classique, à  (ce qui n'est pas vrai en logique intuitionniste, on a seulement  implique ).

D'autre part, en langage naturel, typiquement « si… alors… » est utilisé comme un conditionnel indicatif.

Histoire et variantes 
Smullyan dans son livre de 1978 attribue l'appellation du «  » à ses étudiants de master. Il discute également des variantes (obtenues en remplaçant D par d'autres prédicats plus dramatiques) :
 « il y a une femme sur Terre telle que, si elle devient stérile, toute la race humaine s'éteindra » ; Smullyan écrit que cette formulation est née d'une conversation qu'il a eue avec le philosophe John Bacon ;
 une version « duale » du Principe est la suivante : « il y a au moins une personne telle que si n'importe qui d'autre boit, elle en fait autant ».

Apparaissant comme le « principe des buveurs de Smullyan » ou tout simplement « principe des buveurs », H. P. Barendregt en fait mention dans l'article «  » (1996), accompagné par une série de preuves. Depuis lors, ce paradoxe a fait des apparitions régulières à titre d'exemple dans les publications à propos du raisonnement automatique ; il est parfois utilisé pour contraster l'expressivité des assistants de preuve.

Domaine non vide 
Dans le contexte où les domaines vides sont autorisés, le paradoxe du buveur doit être formulé autrement, par exemple comme suit :

Ou en d'autres termes :
 Si et seulement s'il y a quelqu'un dans le bar, il y a quelqu'un dans le bar de telle sorte que, s'il boit, tout le monde dans le bar boit.

Voir aussi 
 Liste de paradoxes
 Logique temporelle

Références 

Buveur