The Drinker Paradox and its Dual

arXiv1805.06216MaRDI QIDQ6301642FDOQ6301642

Authors: Louis Warren, Hannes Diener, Maarten McKubre-Jordens 

Publication date: 16 May 2018

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 �ig(varphi ightarrow forall y varphi[x/y]�ig) . ] 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 ightarrow exists x psi vdash exists x (varphi ightarrow 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.

This page was built for publication: The Drinker Paradox and its Dual

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6301642)