Drinker Paradox - Proofs of The Paradox

Proofs of The Paradox

The proof begins by recognizing it is true that either everyone in the pub is drinking, or at least one person in the pub isn't drinking. Consequently, there are two cases to consider:

  1. Suppose everyone is drinking. For any particular person, it can't be wrong to say that if that particular person is drinking, then everyone in the pub is drinking — because everyone is drinking. Because everyone is drinking, then that one person must drink because when ' that person ' drinks ' everybody ' drinks, everybody includes that person.
  2. Suppose that at least one person is not drinking. For any particular nondrinking person, it still cannot be wrong to say that if that particular person is drinking, then everyone in the pub is drinking — because that person is, in fact, not drinking. In this case the condition is false, so the statement is vacuously true due to the nature of material implication in formal logic, which states that "If P, then Q" is always true if P (the condition or antecedent) is false.

Either way, there is someone in the pub such that, if he is drinking, everyone in the pub is drinking. A slightly more formal way of expressing the above is to say that if everybody drinks then anyone can be the witness for the validity of the theorem. And if someone doesn't drink, then that particular non-drinking individual can be the witness to the theorem's validity.

The proof above is essentially model-theoretic (can be formalized as such). A purely syntactic proof is possible and can even be mechanized (in Otter for example), but only for an equisatisfiable rather than a equivalent negation of the theorem. Namely, the negation of the theorem is

which is equivalent with the prenex normal form

By Skolemization the above is equisatisfiable with

The resolution of the two clauses and results in an empty set of clauses (i.e. a contradiction), thus proving the negation of the theorem is unsatisfiable. The resolution is slightly non-straightforward because it involves a search based on Herbrand's theorem for ground instances that are propositionally unsatisfiable. The bound variable x is first instantiated with a constant d (making use of the assumption that the domain is non-empty), resulting in the Herbrand universe:

One can sketch the following natural deduction:


\cfrac {\cfrac {\cfrac {\forall x .\ \, } {D(d) \wedge \neg D(f(d))} \forall_E } {\neg D(f(d))} \wedge_E \qquad \cfrac {\cfrac {\forall x .\ \, } {D(f(d)) \wedge \neg D(f(f(d)))} \forall_E } {D(f(d))} \wedge_E } {\bot}\ \Rightarrow_E

Or spelled out:

  1. Instantiating x with d yields which implies
  2. x is then instantiated with f(d) yielding which implies .

Observe that and unify syntactically in their predicate arguments. An (automated) search thus finishes in two steps:

The proof by resolution given here uses the law of excluded middle, the axiom of choice, and non-emptiness of the domain as premises.

Read more about this topic:  Drinker Paradox

Famous quotes containing the words proofs of, proofs and/or paradox:

    I do not think that a Physician should be admitted into the College till he could bring proofs of his having cured, in his own person, at least four incurable distempers.
    Philip Dormer Stanhope, 4th Earl Chesterfield (1694–1773)

    A man’s women folk, whatever their outward show of respect for his merit and authority, always regard him secretly as an ass, and with something akin to pity. His most gaudy sayings and doings seldom deceive them; they see the actual man within, and know him for a shallow and pathetic fellow. In this fact, perhaps, lies one of the best proofs of feminine intelligence, or, as the common phrase makes it, feminine intuition.
    —H.L. (Henry Lewis)

    The paradox of education is precisely this—that as one begins to become conscious one begins to examine the society in which he is being educated.
    James Baldwin (1924–1987)