Paradoxe du buveur

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 :

1. 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.
2. 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[2].

On a la déclaration formelle du théorème, en une formule logique du premier ordre : ${\displaystyle \phi =\exists x\in P.\ [D(x)\Rightarrow \forall y\in P.\ D(y)]}$, et on veut montrer que cette formule est valide.

Soit ${\displaystyle S,\sigma }$ arbitraires. Montrons que ${\displaystyle S,\sigma \models \phi }$. On veut donc trouver ${\displaystyle a\in D_{s}}$ tel que ${\displaystyle S,\sigma (x\rightarrow a)\models D(x)\Rightarrow (\forall y\in P.D(y))}$. On note ${\displaystyle D_{s}}$ l’ensemble des clients qui boivent (c’est-à-dire les ${\displaystyle x\in P.D(x)}$.

• Si ${\displaystyle D_{s}=P}$, on a ${\displaystyle S,\sigma \models \forall x\in P.D(x)}$. Pour ${\displaystyle a\in P}$, ${\displaystyle S,\sigma (x\mapsto a)\models D(x)}$, donc ${\displaystyle S,\sigma (x\mapsto a)\models D(x)\Rightarrow (\forall y\in P.D(y))}$.
• Sinon, on prend ${\displaystyle a\in P\setminus D_{s}(\not =\emptyset )}$. Alors, ${\displaystyle S,\sigma (x\mapsto a)\not \models D(x)}$, donc on a l’implication ${\displaystyle S,\sigma (x\mapsto a)\models D(x)\Rightarrow (\forall y\in P.D(y))}$.

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

Un ensemble P satisfait

${\displaystyle \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.