Loading AI tools
De Wikipédia, l'encyclopédie libre
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?[1].
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 :
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 :
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 : , 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 .
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[1] (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.
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) :
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[3]. 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[4].
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.[réf. souhaitée]
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
si et seulement si, P est non vide.
Ou en d'autres termes :
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.