The drinker paradox (also known as the drinker's theorem, the drinker's principle, or the drinking principle) is a theorem of classical predicate logic that can be stated as "There is someone in the pub such that, if he or she is drinking, then everyone in the pub is drinking." It was popularised by the mathematical logician Raymond Smullyan, who called it the "drinking principle" in his 1978 book What Is the Name of this Book? The apparently paradoxical nature of the statement comes from the way it is usually stated in natural language. It seems counterintuitive both that there could be a person who is causing the others to drink, or that there could be a person such that all through the night that one person were always the last to drink. The first objection comes from confusing formal "if then" statements with causation (see Correlation does not imply causation or Relevance logic for logics that demand relevant relationships between premise and consequent, unlike classical logic assumed here). The formal statement of the theorem is timeless, eliminating the second objection because the person the statement holds true for at one instant is not necessarily the same person it holds true for at any other instant. The formal statement of the theorem is where D is an arbitrary predicate and P is an arbitrary nonempty set. Proofs The proof begins by recognizing it is true that either everyone in the pub is drinking, or at least one person in the pub is not drinking. Consequently, there are two cases to consider: Suppose everyone is drinking. For any particular person, it cannot 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. Otherwise at least one person is not drinking. For any nondrinking person, the statement if that particular person is drinking, then everyone in the pub is drinking is formally true: its antecedent ("that particular person is drinking") is false, therefore the statement is true due to the nature of material implication in formal logic, which states that "If P, then Q" is always true if P is false. (These kinds of statements are said to be vacuously true.) A slightly more formal way of expressing the above is