Введение
Парадокс пьющего (также известный как теорема пьющего, принцип пьющего или принцип питья) - теорема классической предикатной логики, которая может быть выражена как "Есть кто-то в пабе, так что, если он или она пьет, то все в пабе пьют". Это было популяризировано математическим логиком Рэймоном Смуллианом, который назвал его "принципом питья" в своей книге 1978 года "Как называется эта книга?" Очевидно парадоксальный характер утверждения происходит от того, как оно обычно высказывается на естественном языке. Кажется нелогичным, что может быть человек, который заставляет других пить, или что может быть такой человек, что всю ночь один человек всегда был последним, чтобы пить. Первое возражение исходит из путаницы формальных утверждений "если тогда" с причинностью (см. Корреляция не подразумевает причинности или логики релевантности для логики, которая требует соответствующих отношений между предпосылкой и следствием, в отличие от классической логики, принятой здесь). Формальное утверждение теоремы является бессрочным, устраняя второе возражение, потому что человек, для которого утверждение истинно в один момент, не обязательно является тем же человеком, для которого оно истинно в любой другой момент. Формальное утверждение теоремы заключается в том, что D является произвольным предикатом, а P - произвольным непустым множеством.
The drinker paradox (also known as the drinker's theorem, the drinker's principle, or the drinking principle) is a theorem of classical predicate logic that can be stated as "There is someone in the pub such that, if he or she is drinking, then everyone in the pub is drinking." It was popularised by the mathematical logician Raymond Smullyan, who called it the "drinking principle" in his 1978 book What Is the Name of this Book? The apparently paradoxical nature of the statement comes from the way it is usually stated in natural language. It seems counterintuitive both that there could be a person who is causing the others to drink, or that there could be a person such that all through the night that one person were always the last to drink. The first objection comes from confusing formal "if then" statements with causation (see Correlation does not imply causation or Relevance logic for logics that demand relevant relationships between premise and consequent, unlike classical logic assumed here). The formal statement of the theorem is timeless, eliminating the second objection because the person the statement holds true for at one instant is not necessarily the same person it holds true for at any other instant. The formal statement of the theorem is
where D is an arbitrary predicate and P is an arbitrary nonempty set.
Доказательства
Доказательство начинается с признания того, что все в пабе пьют, или, по крайней мере, один человек в пабе не пьет. Следовательно, следует рассмотреть два случая:
Объяснение парадоксальности
Парадокс в конечном счете основан на принципе формальной логики, что утверждение истинно всякий раз, когда A ложно, т. е. любое утверждение следует из ложного утверждения. С тех пор он регулярно появляется в качестве примера в публикациях об автоматизированных рассуждениях; иногда он используется для противопоставления выразительности помощников доказательства.