THEOREM

*******

Consider the set of all drinkers in that world, and the set of all people in a given pub. Then there exists a person who, if her or she is drinking, then everyone in that pub is  drinking. More formally:

     EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]]

     (This proof was written with the aid of the author's DC Proof 2.0 software available

     at http://www.dcproof.com )

PREVIOUS RESULT

***************

From The Paradox of the Universal Set, we have the fact that every set excludes something:

1     ALL(s):[Set(s) => EXIST(a):~a e s]

      Axiom

DEFINITIONS

***********

Let drinkers be the set of all people in the world who are drinkers.

2     Set(drinkers)

      Axiom

Let pub be the set of all people in a given pub

3     Set(pub)

      Axiom

PROOF

*****

Applying the previous result that every set excludes something to drinkers...

4     Set(drinkers) => EXIST(a):~a e drinkers

      U Spec, 1

5     EXIST(a):~a e drinkers

      Detach, 4, 2

Define: x  (a non-drinker)

6     ~x e drinkers

      E Spec, 5

Apply Arbitrary-OR Rule

7     ~x e drinkers | ALL(a):[a e pub => a e drinkers]

      Arb Or, 6

8     ~~x e drinkers => ALL(a):[a e pub => a e drinkers]

      Imply-Or, 7

9     x e drinkers => ALL(a):[a e pub => a e drinkers]

      Rem DNeg, 8

As Required:

10    EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]]

      E Gen, 9