# 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 : « Dans toute pièce non vide, il existe une personne ayant la propriété : Si cette personne boit, tout le monde dans la pièce boit. »
Il a été popularisé par le mathématicien logicien Raymond Smullyan, qui l'a appelé le drinking principle dans son livre de 1978 What Is the Name of This Book?.
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 :
    $\exists x\in P.\ [D(x)\Rightarrow \forall y\in P.\ D(y)]$
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 : $\phi =\exists x\in P.\ [D(x)\Rightarrow \forall y\in P.\ D(y)]$, et on veut montrer que cette formule est valide.
Soit $S,\sigma$ arbitraires. Montrons que $S,\sigma \models \phi$. On veut donc trouver $a\in D_{s}$ tel que $S,\sigma (x\rightarrow a)\models D(x)\Rightarrow (\forall y\in P.D(y))$. On note $D_{s}$ l’ensemble des clients qui boivent (c’est-à-dire les $x\in P.D(x)$.
* Si $D_{s}=P$, on a $S,\sigma \models \forall x\in P.D(x)$. Pour $a\in P$, $S,\sigma (x\mapsto a)\models D(x)$, donc $S,\sigma (x\mapsto a)\models D(x)\Rightarrow (\forall y\in P.D(y))$.
* Sinon, on prend $a\in P\setminus D_{s}(\not =\emptyset )$. Alors, $S,\sigma (x\mapsto a)\not \models D(x)$, donc on a l’implication $S,\sigma (x\mapsto a)\models D(x)\Rightarrow (\forall y\in P.D(y))$.

## 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é $A\Rightarrow B$ 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 $A\Rightarrow B$ est équivalente, en logique classique, à $\lnot A\lor B$ (ce qui n'est pas vrai en logique intuitionniste, on a seulement $\lnot A\lor B$ implique $A\Rightarrow B$).
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 « Drinking Principle » à 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 « The quest for correctness » (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.
Le logicien Jean-Louis Krivine présente ce paradoxe dans des écrits informels comme le plus simple des théorèmes non triviaux. La forme qu'il en donne est : dans un bar il y a toujours quelqu'un qui, s'il boit, tout le monde boit.

### 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 :
   Un ensemble P satisfait
       $\exists x\in P.\ [D(x)\Rightarrow \forall y\in P.\ D(y)]\,$
   si et seulement si, P est non vide.
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.