Парадокс пьющего

Парадокс пьющего (также известный как теорема пьющего или принцип пьющих) — это теорема классической предикатной логики, которую можно сформулировать так: «В пабе есть человек, который, если он или она пьет, то все в пабе пьют». Она была популяризирована математическим логиком Раймондом Смульяном, который назвал ее «принципом пьющих» в своей книге 1978 года «Как называется эта книга?».

Парадокс пьющего

Парадоксальный характер утверждения проистекает из того, как оно обычно формулируется на естественном языке. Кажется нелогичным как то, что может существовать человек, который заставляет других пить, так и то, что может существовать человек, который всю ночь всегда оставался последним, кто пил. Первое возражение связано со смешением формальных утверждений типа «если-то» с причинно-следственной связью (см. «Корреляция не подразумевает причинно-следственную связь» или «Логика релевантности» для логик, требующих релевантных отношений между посылкой и следствием, в отличие от классической логики, предполагаемой здесь). Формальная формулировка теоремы является вневременной, что устраняет второе возражение, поскольку человек, для которого утверждение верно в один момент времени, не обязательно является тем же человеком, для которого оно верно в любой другой момент времени.

Доказательства

Доказательство начинается с признания того, что либо все в пабе пьют, либо хотя бы один человек в пабе не пьет. Следовательно, следует рассмотреть два случая:

• Предположим, все пьют. Для любого конкретного человека нельзя ошибочно сказать, что если этот конкретный человек пьет, то все в пабе пьют — потому что все пьют. Поскольку все пьют, то этот человек должен пить, потому что когда этот человек пьет, пьют все, включая этого человека.
• В противном случае, по крайней мере один человек не пьет. Для любого непьющего человека утверждение «если этот конкретный человек пьет, то все в пабе пьют» формально истинно: его антецедент («этот конкретный человек пьет») ложен, следовательно, утверждение истинно в силу природы материальной импликации в формальной логике, которая гласит, что «Если P, то Q» всегда истинно, если P ложно (такие утверждения называются пустоистинными).

Более формальным способом выразить вышесказанное является утверждение, что если все пьют, то любой может быть свидетелем справедливости теоремы. А если кто-то не пьет, то именно этот непьющий человек может быть свидетелем справедливости теоремы.

Объяснение парадоксальности

Парадокс в конечном итоге основан на принципе формальной логики, согласно которому утверждение А -> B истинно всякий раз, когда А ложно, т.е. любое утверждение следует из ложного утверждения (ex falso quodlibet).

Важно понимать парадокс, поскольку условное утверждение в классической (и интуиционистской) логике является материальным условным утверждением. Оно обладает свойством, что А -> B истинно всякий раз, когда B правда или А ложно. В классической логике (но не в интуиционистской логике) это также необходимое условие: если А -> B правда, то B правда или А ложно.

Таким образом, в данном случае утверждение «если они пьют, то все пьют» было признано верным в одном случае, если все пьют, и в другом случае, если они не пьют — даже если их употребление алкоголя никак не связано с употреблением алкоголя другими.

История и вариации

Смульян в своей книге 1978 года приписывает название «Принцип питья» своим аспирантам. Он также обсуждает варианты (полученные заменой D другими, более выразительными предикатами):

• «На земле есть женщина, и если она станет бесплодной, весь человеческий род вымрет». Смульян пишет, что эта формулировка возникла из разговора, который он провел с философом Джоном Бэконом.
• «Двойная» версия Принципа: «есть по крайней мере один человек, такой, что если кто-то пьет, то он пьет».

Как «принцип пьющих Смульяна» или просто «принцип пьющих», он появляется в работе Х. П. Барендрегта «В поисках правильности» (1996) в сопровождении некоторых машинных доказательств. С тех пор он регулярно появляется в качестве примера в публикациях об автоматизированном рассуждении; иногда его используют для противопоставления выразительности систем автоматического доказательства.