Voir la source de 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 (logique mathématique)|prédicat]]) qui peut être énoncé ainsi : {{citation|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 [[Logique mathématique|logicien]] [[Raymond Smullyan]], qui l'a appelé le ''{{Langue|en|drinking principle}}'' dans son livre de 1978 ''{{Langue|en|What Is the Name of This Book?}}''<ref name="Smullyan">{{Ouvrage|auteur1=[[Raymond Smullyan]]|titre=What is the Name of this Book?|sous-titre=The Riddle of Dracula and Other Logical Puzzles|éditeur=[[Prentice Hall]]|année=1978|pages totales=chapter 14. How to Prove Anything. (topic) 250. The Drinking Principle. pp. 209-211|isbn=0-13-955088-7}}.</ref>.

La nature apparemment [[Paradoxe|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 [[Cum hoc ergo propter hoc|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 :

:<math>\exists x\in P.\ [D(x) \Rightarrow \forall y\in P.\ D(y)] </math>

où D est un [[Prédicat (logique mathématique)|prédicat]] arbitraire et P est un ensemble non vide arbitraire.

Ceci découle de la [[Logique_mathématique#Propriétés_moins_intuitives|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 (logique)|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)|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<ref name="Cameron1999">{{Ouvrage|auteur1=[[Peter Cameron (mathématicien)|Peter J. Cameron]]|titre=Sets, Logic and Categories|éditeur=Springer|année=1999|pages totales=182|passage=91|isbn=978-1-85233-056-9|lire en ligne=https://books.google.com/books?id=sDfdbBQ75MQC&pg=PA91}}</ref>.

=== Preuve formelle ===
{{Article connexe|Calcul des prédicats}}
On a la déclaration formelle du théorème, en une formule logique du premier ordre : <math>\phi = \exists x\in P.\ [D(x) \Rightarrow \forall y\in P.\ D(y)] </math>, et on veut montrer que cette formule est valide.

Soit <math>S, \sigma</math> arbitraires. Montrons que <math>S, \sigma \models \phi</math>. On veut donc trouver <math>a \in D_s </math> tel que <math>S, \sigma(x \rightarrow a) \models D(x) \Rightarrow (
\forall y \in P . D(y)) </math>. On note <math>D_s</math> l’ensemble des clients qui boivent (c’est-à-dire les <math>x \in P. D(x)</math>.

* Si <math>D_s = P</math>, on a <math>S, \sigma \models \forall x \in P. D(x)</math>. Pour <math>a \in P</math>, <math>S, \sigma (x \mapsto a) \models D(x)</math>, donc <math>S, \sigma (x \mapsto a) \models D(x) \Rightarrow (\forall y \in P. D(y))</math>.
* Sinon, on prend <math>a \in P \setminus D_s (\not = \emptyset)</math>. Alors, <math>S, \sigma (x \mapsto a) \not \models D(x)</math>, donc on a l’implication <math>S, \sigma (x \mapsto a) \models D(x) \Rightarrow (\forall y \in P. D(y))</math>.

== Explication de paradoxe ==
Le paradoxe est finalement fondé sur le [[Principe du tiers exclu#En mathématiques|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é <math>A \Rightarrow B</math> est vrai dès que A est faux, c'est-à-dire que toute déclaration découle d'une fausse déclaration<ref name="Smullyan" /> (''[[Principe d'explosion|ex falso quodlibet]]'').

Ce qui est important pour le paradoxe, c'est que l'implication logique <math>A \Rightarrow B</math> est équivalente, en logique classique, à <math>\lnot A \lor B</math> (ce qui n'est pas vrai en [[logique intuitionniste]], on a seulement <math>\lnot A \lor B</math> implique <math>A \Rightarrow B</math>).

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 « ''{{Langue|en|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 », [[Henk Barendregt|H. P. Barendregt]] en fait mention dans l'article « {{Langue|en|The quest for correctness}} » (1996), accompagné par une série de preuves<ref name="Images of SMC Research 1996">{{Ouvrage|auteur1=H. P. Barendregt|titre=Images of SMC Research 1996|éditeur=Stichting Mathematisch Centrum|année=1996|pages totales=54–55|isbn=978-90-6196-462-9|lire en ligne=http://oai.cwi.nl/oai/asset/13544/13544A.pdf|titre chapitre=The quest for correctness }}.</ref>. Depuis lors, ce paradoxe a fait des apparitions régulières à titre d'exemple dans les publications à propos du [[Raisonnement automatisé|raisonnement automatique]] ; il est parfois utilisé pour contraster l'expressivité des [[Assistant de preuve|assistants de preuve]]<ref>{{en}} Freek Wiedijk. 2001. [http://www.cs.ru.nl/~freek/mizar/miz.pdf « {{Langue|en|Mizar Light for HOL Light}} »] {{pdf}}. In Proceedings of the {{14th}} International Conference on Theorem Proving in Higher Order Logics (TPHOLs '01), Richard J. Boulton and Paul B. Jackson (Eds.). Springer-Verlag, London, UK, 378-394.</ref>.

{{refsou|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<ref>{{Lien web|langue=anglais|titre=Searchable Sets, Dubuc-Penon Compactness, Omniscience Principles, and the Drinker Paradox|url=http://www.cs.bham.ac.uk/~mhe/papers/dp.pdf|site=|date=|consulté le=}}.</ref> :

{{Énoncé|Un ensemble P satisfait 
:<math>\exists x\in P.\ [D(x) \Rightarrow \forall y\in P.\ D(y)] \, </math>
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''.

== Voir aussi ==
* [[Liste de paradoxes]]
* [[Logique temporelle]]

== Références ==
{{Références}}

{{Portail|mathématiques}}

[[Catégorie:Paradoxe en mathématiques|Buveur]]