Smullyan's Drinking Principle/Formal Proof

Formal Exposition of Smullyan's Drinking Principle

Let the universe of discourse be the non-empty set of people in the pub.

Let $\map D x$ be interpreted as the statement "$x$ is drinking".

Then:

$\exists x : \paren {\map D x \implies \forall y : \map D y}$

Proof

We have two choices:

$\forall y : \map D y$

and

$\neg \forall y : \map D y$

Suppose $\forall y : \map D y$.

By True Statement is implied by Every Statement:

$\map D x \implies \forall y : \map D y$

By Existential Generalisation:

$\exists x : \paren {\map D x \implies \forall y : \map D y}$

Now suppose:

$\neg \forall y : \map D y$

By De Morgan's Laws (Predicate Logic)/Denial of Universality:

$\exists y : \neg \map D y$

Switch the variable $y$ with $x$.

Thus, for some $x$:

$\neg \map D x$

By False Statement implies Every Statement, we have:

$\map D x \implies \forall y : \map D y$

By Existential Generalisation:

$\exists x : \paren {\map D x \implies \forall y : \map D y}$

Thus, $\exists x : \paren {\map D x \implies \forall y : \map D y}$ holds both when:

$\forall y : \map D y$

and when:

$\neg \forall y : \map D y$

concluding the proof.

$\blacksquare$

Source of Name

This entry was named for Raymond Merrill Smullyan.