Talk:Drinker paradox

From Wikipedia, the free encyclopedia

The first step of the proof, stating that either everybody drinks

or someone doesn't drink, is an application of the principle of  
excluded middle, so the paradox is true only in classical logic 
but false in intuitionistic logic; 

I don't agree. This is valid in intuitionistic logic. The set of people in a bar is finite (!) and it should be decidable by direct observation whether someone is drinking or not^*. No appeal to the law of the excluded middle is needed.

The last step of the proof uses the notion of material 
implication, according to which a hypothetical statement in the  
form if A then B is always true if A is false. 

This seems to be the essence of the paradox. It's about fallacies of relevance, not constructivism.

Paradoxes of this kind are used by the intuitionist school in the
philosophy of mathematics to argue against the the laws of 
classical logic.

I'm curious about that. Does one of the references cited argue this way?

-Dan 13:49, 17 May 2006 (UTC)

It is true that excluded middle is not needed because the set of drinkers is finite, but the logical formula doesn't assume finiteness. Since finiteness is not formalizable in first order logic, the only way to prove the paradox is to use excluded middle.

(Anyway, I like your hospital example even better than the drinker. We could add it to the page, but the paradox is commonly known as the drinker paradox.)

About its relevance to intuitionism, maybe that's a silly part of the article. Some intuitionists argued in that way to me, but it is not to be found in any published work. So it probably must be deleted.

Eubulide 14:04, 17 May 2006 (UTC)

No, it's not the only way to prove it. We can still do without LEM.

• For a bar/hospital: every customer/patient is a human. The human population is less than one trillion (true now, almost certainly true in my lifetime, and can be increased as desired). "Less than one trillion" is formalizable in first-order logic.
• For prime numbers: we can talk about finite sequences of natural numbers in Heyting arithmetic just fine. I do believe the sentence "in every finite non-empty sequence of natural numbers there is a number which, if it is prime, all numbers in the sequence are prime" is expressible in HA and is a theorem!

I would never make this argument against LEM, and I consider myself a constructivist. Now I don't consider myself an intuitionist, still, Brouwer himself considered LEM to be something from our experience of finite space and time (and used improperly in discussing the infinite), so presumably he would not like this argument either. Please hit your intuitionist friends over the head! -Dan 16:09, 17 May 2006 (UTC)

It just occurred to me how your hospital interpretation actually shows the paradox to be essentially classic. Just change your interpretation a little: "In every hospital there is a patient such that, if he recovers, all the patients recover". So the doctors only need to cure that one patient! Of course, it is undecidable which one that patient is. Eubulide 14:21, 17 May 2006 (UTC)

A medical breakthrough! -Dan 16:09, 17 May 2006 (UTC)

[edit] Infinite undecidable drunken health care

Speaking of Ralph Klein, is there a version of this which a) is classically (but not constructively) equivalent to the original statement that every non-empty hospital has a patient who, if cured, everyone is cured, and b) is constructively provable, even without assuming that the hospital is finite, or that death is decidable?

Answer: Yes. If, in a hospital, there isn't a patient who dies if any patient dies, then that hospital has no patients at all.

Proof: exercise for the reader :-) -Dan 19:44, 18 May 2006 (UTC)

[edit] LME Redux

The paradox can be stated with less parentheses, i.e. (Ex) Drink(x) -> (x) Drink(x). Further, the argument seems to rely on the closed world assumption, and not on the excuded middle.

The Coq prover page uses sets and that goes beyond the scope of logic. So, in order to be certain, can somebody give a derivation of the paradox in classical logic, and if possible, in intuitionistic logic? Actually, I wonder if either is possible. If it is not possible, please correct the claims on the page. -- 129.247.247.238 16:37, 22 May 2006 (UTC)

I'm not sure that's a good way to write that, as it might be read rather than . As for a proof, alright:

SOLUTION TO QUESTION POSED ABOVE

In constructive free logic:

Which was my statement above. I trust you can take it from here to classical logic. Bonus points: where is the paradox of material implication (aka fallacy of relevance)? -Dan 20:17, 22 May 2006 (UTC)

I admit I am confused now. I have a straightforward proof using game semantics showing that (Ex) (Drink(x) -> (y) Drink(y)) is neither intuitionistically nor classically derivable:

  0                       (Ex) (Drink(x) -> (y) Drink(y))
  1  0?                   Drink(n) -> (y) Drink(y)
  2  1? Drink(n)          (y) Drink(y)
  3  2? m                 Drink(m)
  4  3?

Am I missing something badly? I think we have a case of hidden axioms which are needed to prove the proposition. -- 129.247.247.238 10:02, 23 May 2006 (UTC)

Yes, I was missing something -- there is a condition, in any non-empty-bar... This makes the domain non-empty and closes the domain of discourse, too. What is wrong, is that the formal version does not list these conditions formally.

The article should be modified accordingly. And the claim, that the proof relies on LME can be deleted, as shown by Dan. -- 129.247.247.238 14:15, 23 May 2006 (UTC)

I do not understand this. If , then holds. Why must the bar be non-empty?

[edit] Nonintuitive

Shouldn't it be mentioned that while the original definition seems counter-intuitive, the contrapositive makes perfect sense (that is, if not (everybody drinks) then (someone doesn't drink))? Or am I wrong about that? MagiMaster

Contraposition is not an equivalence in intuitionistic logic. Precisely, holds, but the reverse, , doesn't. Therefore, the drinker's principle only implies your preferred contrapositive version in all logics. I have no opinion on which version of the classical statement is more "intuitive" because I tend to find classical logic non-intuitive. — Kaustuv Chaudhuri 03:24, 16 July 2006 (UTC)

Actually, I don't think that's even the correct contrapositive. The implication occurs inside the existential quantifier. The contrapositive of should be , which is (non-constructively) equivalent to . That is, "there exists someone who, if anyone doesn't drink, he also doesn't drink." 192.75.48.150 12:58, 17 July 2006 (UTC)

Hmm, I think the original comment was essentially correct. I interpreted the statement as talking about the body of the outer . — Kaustuv Chaudhuri 13:47, 17 July 2006 (UTC)

Ah, never mind, I see what you're getting at. Yeah, is only implied by the contrapositive of the drinker principle. The original statement was imprecise because "someone doesn't drink" can be interpreted as an . — Kaustuv Chaudhuri 14:20, 17 July 2006 (UTC)

Sorry, I forgot to sign my first comment. This is what I was thinking about when I wrote that though. I wasn't sure if it was right, because I don't remember exactly how negating qualifiers works. (Also, I don't know much about intuistionistic logic. I'm a computer scientist, so I studied classical logic.) MagiMaster 19:58, 17 July 2006 (UTC)

[edit] laymen

Could someone write out the reasoning in plain speech as opposed to latex? I'm not familiar with all the logic symbols, and furthermore, I prefer, as many probably do, the construction of natural language.

I hope this helps. 192.75.48.150 15:37, 14 August 2006 (UTC)

I guess not. We got a {{technical}} tag again. Please feel free to ask questions here. We don't bite. 192.75.48.150 21:06, 17 August 2006 (UTC)

(transcribed from WP:RfF --192.75.48.150 19:17, 28 August 2006 (UTC))

• It would be unwise for any newcomers to logic to leap straight in at this point, so the application of the technical tag is probably not appropriate. It is certainly a lot more accessible than certain other articles in this subject area. That said, there are a couple of points that could be cleared up:
  • In the proof section, I don't think it would be redundant to re-explain the proof (although I'm struggling to come up with alternate phrasing).
  • The proof diagram is scary - perhaps move it to its own subsection in the proof section, so readers can see that they don't need to be able to decipher that to understand the concept.
  • The reference to Goldbach's conjecture is awkward - you should make clear that it is unsolved, can not be solved like this because this reasoning is invalid, and introduce the section more clearly, something like "For instance, it would allow us to solve Goldbach's conjecture which has taxed mathematicians for hundreds of years...".
  • I'd always explain in English before using notations: the section "Material versus indicative conditional" in particular, would probably read better if the order of the sentences was changed and the notation explained.
  • In some cases you might like to point readers to appropriate connected themes explicitly rather than just a wikilink.
  • I also have a feeling that the title may draw an unintended audience, so some stress in the lead that it has nothing to do with pub culture or drinking games (or rather, overstressing the connection to first order logic) won't hurt.

Hope this helps. Yomangani^talk 11:03, 25 August 2006 (UTC)

I have simply removed the proof diagrams as in the present form they add no clarity to the article. I disagree with nearly all of the mumbo jumbo that was added as the logical issue seems fairly shallow to me, but I'll leave it be. — Kaustuv Chaudhuri 12:56, 3 September 2006 (UTC)

The paradox is less paradoxical and easier to understand when it is explained the following way: assume there is a person who would be the last to start drinking. If and when this person drinks, then everybody drinks.

While reminiscent of Zorn's Lemma, one need not delve into set theory at this point. Although the connection might be used in order to explain why the "paradox" need not arise in intuitionistic logic. -- Zz 13:13, 5 September 2006 (UTC)

Eh. I can see where you're headed with the last person to drink, but I'm not seeing the connection to Zorn's lemma. 192.75.48.150 17:27, 5 September 2006 (UTC)

The connection lies in the maximal element existing for every non-empty partially ordered set (e.g. the last one to drink). For finite sets the existence of such an element is obvious. For infinite sets, however, the argument presented might fail, unless the lemma guarantees the existence of this element. This echoes the objection listed for intuitionistic logic - for finite sets, the drinker paradox is provable (see above), for potentially infinite sets, this need not be so. -- Zz 02:09, 6 September 2006 (UTC)

Sorry Kaustuv, did you mean your only objection to the mumbo-jumbo is that it is unneeded, because the issue is shallow? Or was there something else? 192.75.48.150 17:27, 5 September 2006 (UTC)