The Drinker Paradox and its Dual

TL;DR

This paper investigates the logical implications and independence of the Drinker Paradox and its dual within minimal logic, exploring their relationships with classical principles like the law of excluded middle and Markov's Principle.

Contribution

It demonstrates the independence of these principles from classical logic and analyzes their connections to other well-known logical principles through proofs and semantic models.

Findings

The principles are independent of the law of excluded middle.

They are also independent of each other.

Connections to Markov's Principle are established.

Abstract

The Drinker Paradox is as follows. In every nonempty tavern, there is a person such that if that person is drinking, then everyone in the tavern is drinking. Formally, \[ \exists x \big(\varphi \rightarrow \forall y \varphi[x/y]\big) \ . \] Due to its counterintuitive nature it is called a paradox, even though it actually is a classical tautology. However, it is not minimally (or even intuitionistically) provable. The same can be said of its dual, which is (equivalent to) the well-known principle of \emph{independence of premise}, \[ \varphi \rightarrow \exists x \psi \ \vdash \ \exists x (\varphi \rightarrow \psi) \] where $x$ is not free in $\varphi$. In this paper we study the implications of adding these and other formula schemata to minimal logic. We show first that these principles are independent of the law of excluded middle and of each other, and second how these schemata relate to other well-known principles, such as Markov's Principle of unbounded search, providing proofs and semantic models where appropriate.