Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

You can be replaced by this computer.

tech / sci.math / Revisiting Smullyan's Drinker's Paradox

SubjectAuthor
* Revisiting Smullyan's Drinker's ParadoxDan Christensen
+- Re: Revisiting Smullyan's Drinker's ParadoxDan Christensen
+- Re: Revisiting Smullyan's Drinker's ParadoxDan Christensen
`* Re: Revisiting Smullyan's Drinker's ParadoxDan Christensen
 `- Re: Revisiting Smullyan's Drinker's ParadoxMostowski Collapse

1
Revisiting Smullyan's Drinker's Paradox

<9a7c1fe6-036b-4bc3-87b3-ffc62526d1e1n@googlegroups.com>

  copy mid

https://www.novabbs.com/tech/article-flat.php?id=129786&group=sci.math#129786

  copy link   Newsgroups: sci.math
X-Received: by 2002:a05:620a:c06:b0:745:ad92:8887 with SMTP id l6-20020a05620a0c0600b00745ad928887mr4071684qki.13.1679108486412;
Fri, 17 Mar 2023 20:01:26 -0700 (PDT)
X-Received: by 2002:aca:2810:0:b0:384:ef1:3467 with SMTP id
16-20020aca2810000000b003840ef13467mr3897036oix.4.1679108486095; Fri, 17 Mar
2023 20:01:26 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Fri, 17 Mar 2023 20:01:25 -0700 (PDT)
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <9a7c1fe6-036b-4bc3-87b3-ffc62526d1e1n@googlegroups.com>
Subject: Revisiting Smullyan's Drinker's Paradox
From: Dan_Chri...@sympatico.ca (Dan Christensen)
Injection-Date: Sat, 18 Mar 2023 03:01:26 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 2822
 by: Dan Christensen - Sat, 18 Mar 2023 03:01 UTC

Back from vacation! In honour of St. Patrick's Day, here is an alternative version of Smullyan's proof of the Drinker's Paradox/Principle, which he states as follows:

"[T]here exists someone such that whenever he (or she) drinks, everybody drinks."
--Raymond Smullyan, "What is the name of this book?" 1978, p. 209

Subsequent versions include mention of a pub, e.g.

"There is someone in THE PUB such that, if he or she is drinking, then everyone in THE PUB is drinking."
https://en.wikipedia.org/wiki/Drinker_paradox

I follow this trend in the version presented here. I begin by making the reasonable assumption that there exists a drinker that is NOT found in a given pub.

EXIST(a):[Drinker(a) & ~InPub(a)]

Where:

Drinker(x) means x is a drinker
InPub(x) means x is in that pub

From this innocent assumption, I then prove using a version of natural deduction that:

EXIST(b):[Drinker(b) & InPub(b) => ALL(c):[InPub(c) => Drinker(c)]]

PROOF

Suppose there exists a drinker that is not in a given pub

1. EXIST(a):[Drinker(a) & ~InPub(a)]
Premise

2. Drinker(x) & ~InPub(x)
E Spec, 1

3. ~InPub(x)
Split, 2

Suppose to the contrary that x is a drinker in that pub

4. Drinker(x) & InPub(x)
Premise

5. InPub(x)
Split, 4

6. ~InPub(x) => ALL(c):[InPub(c) => Drinker(c)]
Arb Cons, 5

It is vacuously true that...

7. ALL(c):[InPub(c) => Drinker(c)]
Detach, 6, 3

As Required:

8. Drinker(x) & InPub(x)
=> ALL(c):[InPub(c) => Drinker(c)]
Conclusion, 4

As Required:

9. EXIST(a):[Drinker(a) & ~InPub(a)]
=> EXIST(b):[Drinker(b) & InPub(b)
=> ALL(c):[InPub(c) => Drinker(c)]]
Conclusion, 1

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

Re: Revisiting Smullyan's Drinker's Paradox

<8d107b68-b820-4cd9-8f76-1b6ffe6bccd0n@googlegroups.com>

  copy mid

https://www.novabbs.com/tech/article-flat.php?id=129795&group=sci.math#129795

  copy link   Newsgroups: sci.math
X-Received: by 2002:a05:620a:20c2:b0:745:7bfe:bbf6 with SMTP id f2-20020a05620a20c200b007457bfebbf6mr4733566qka.9.1679116311145;
Fri, 17 Mar 2023 22:11:51 -0700 (PDT)
X-Received: by 2002:a05:6871:4d01:b0:17a:b1ef:1c3f with SMTP id
ug1-20020a0568714d0100b0017ab1ef1c3fmr288057oab.6.1679116310828; Fri, 17 Mar
2023 22:11:50 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Fri, 17 Mar 2023 22:11:50 -0700 (PDT)
In-Reply-To: <9a7c1fe6-036b-4bc3-87b3-ffc62526d1e1n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
References: <9a7c1fe6-036b-4bc3-87b3-ffc62526d1e1n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <8d107b68-b820-4cd9-8f76-1b6ffe6bccd0n@googlegroups.com>
Subject: Re: Revisiting Smullyan's Drinker's Paradox
From: Dan_Chri...@sympatico.ca (Dan Christensen)
Injection-Date: Sat, 18 Mar 2023 05:11:51 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 3599
 by: Dan Christensen - Sat, 18 Mar 2023 05:11 UTC

On Friday, March 17, 2023 at 11:01:30 PM UTC-4, Dan Christensen wrote:
> Back from vacation! In honour of St. Patrick's Day, here is an alternative version of Smullyan's proof of the Drinker's Paradox/Principle, which he states as follows:
>
> "[T]here exists someone such that whenever he (or she) drinks, everybody drinks."
> --Raymond Smullyan, "What is the name of this book?" 1978, p. 209
>
> Subsequent versions include mention of a pub, e.g.
>
> "There is someone in THE PUB such that, if he or she is drinking, then everyone in THE PUB is drinking."
> https://en.wikipedia.org/wiki/Drinker_paradox
>
> I follow this trend in the version presented here. I begin by making the reasonable assumption that there exists a drinker that is NOT found in a given pub.
>
> EXIST(a):[Drinker(a) & ~InPub(a)]
>
> Where:
>
> Drinker(x) means x is a drinker
> InPub(x) means x is in that pub
>
> From this innocent assumption, I then prove using a version of natural deduction that:
>
> EXIST(b):[Drinker(b) & InPub(b) => ALL(c):[InPub(c) => Drinker(c)]]
>
> PROOF
>
> Suppose there exists a drinker that is not in a given pub
>
> 1. EXIST(a):[Drinker(a) & ~InPub(a)]
> Premise
>
> 2. Drinker(x) & ~InPub(x)
> E Spec, 1
>
> 3. ~InPub(x)
> Split, 2
>
> Suppose to the contrary that x is a drinker in that pub
>
> 4. Drinker(x) & InPub(x)
> Premise
>
> 5. InPub(x)
> Split, 4
>
> 6. ~InPub(x) =>
> Arb Cons, 5

The key point here is that the above consequent ALL(c):[InPub(c) => Drinker(c)] is completely arbitrary. It could be ANY expression in x, whatsoever, even the negation ~ALL(c):[InPub(c) => Drinker(c)].

>
> It is vacuously true that...
>
> 7. ALL(c):[InPub(c) => Drinker(c)]
> Detach, 6, 3
>
> As Required:
>
> 8. Drinker(x) & InPub(x)
> => ALL(c):[InPub(c) => Drinker(c)]
> Conclusion, 4
>
> As Required:
>
> 9. EXIST(a):[Drinker(a) & ~InPub(a)]
> => EXIST(b):[Drinker(b) & InPub(b)
> => ALL(c):[InPub(c) => Drinker(c)]]
> Conclusion, 1
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Re: Revisiting Smullyan's Drinker's Paradox

<00ab1721-4702-4ced-9a59-db9420938060n@googlegroups.com>

  copy mid

https://www.novabbs.com/tech/article-flat.php?id=129827&group=sci.math#129827

  copy link   Newsgroups: sci.math
X-Received: by 2002:ad4:4ae3:0:b0:56e:a7d5:7c75 with SMTP id cp3-20020ad44ae3000000b0056ea7d57c75mr6646183qvb.3.1679178457055;
Sat, 18 Mar 2023 15:27:37 -0700 (PDT)
X-Received: by 2002:a4a:ba0a:0:b0:52e:17e2:7d4c with SMTP id
b10-20020a4aba0a000000b0052e17e27d4cmr1013314oop.1.1679178456760; Sat, 18 Mar
2023 15:27:36 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!diablo1.usenet.blueworldhosting.com!85.12.63.48.MISMATCH!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Sat, 18 Mar 2023 15:27:36 -0700 (PDT)
In-Reply-To: <9a7c1fe6-036b-4bc3-87b3-ffc62526d1e1n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
References: <9a7c1fe6-036b-4bc3-87b3-ffc62526d1e1n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <00ab1721-4702-4ced-9a59-db9420938060n@googlegroups.com>
Subject: Re: Revisiting Smullyan's Drinker's Paradox
From: Dan_Chri...@sympatico.ca (Dan Christensen)
Injection-Date: Sat, 18 Mar 2023 22:27:37 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 3342
 by: Dan Christensen - Sat, 18 Mar 2023 22:27 UTC

On Friday, March 17, 2023 at 11:01:30 PM UTC-4, Dan Christensen wrote:
> Back from vacation! In honour of St. Patrick's Day, here is an alternative version of Smullyan's proof of the Drinker's Paradox/Principle, which he states as follows:
>
> "[T]here exists someone such that whenever he (or she) drinks, everybody drinks."
> --Raymond Smullyan, "What is the name of this book?" 1978, p. 209
>
> Subsequent versions include mention of a pub, e.g.
>
> "There is someone in THE PUB such that, if he or she is drinking, then everyone in THE PUB is drinking."
> https://en.wikipedia.org/wiki/Drinker_paradox
>
> I follow this trend in the version presented here. I begin by making the reasonable assumption that there exists a drinker that is NOT found in a given pub.
>
> EXIST(a):[Drinker(a) & ~InPub(a)]
>
> Where:
>
> Drinker(x) means x is a drinker
> InPub(x) means x is in that pub
>
> From this innocent assumption, I then prove using a version of natural deduction that:
>
> EXIST(b):[Drinker(b) & InPub(b) => ALL(c):[InPub(c) => Drinker(c)]]
>

Less restrictive, shorter and more preferable may be:
Prove: EXIST(a):~Drinker(a) => EXIST(b):[Drinker(b) => ALL(c):[InPub(c) => Drinker]]
Where:
Drinker(x) means x is a drinker
InPub(x) means x is in the pub
Suppose there exists at least one non-drinker

1. EXIST(a):~Drinker(a)
Premise

Let x be a non-drinker, not necessarily one in the pub

2. ~Drinker(x)
E Spec, 1

Introduce arbitrary disjunction on RHS

3. ~Drinker(x) | ALL(c):[InPub(c) => Drinker(c)]
Arb Or, 2

Apply definition of '=>'

4. ~~Drinker(x) => ALL(c):[InPub(c) => Drinker(c)]
Imply-Or, 3

5. Drinker(x) => ALL(c):[InPub(c) => Drinker(c)]
Rem DNeg, 4

As Required:

6. EXIST(a):~Drinker(a)
=> EXIST(b):[Drinker(b) => ALL(c):[InPub(c) => Drinker(c)]]
Conclusion, 1

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

Re: Revisiting Smullyan's Drinker's Paradox

<671f1195-1de9-4106-a226-131994c930e5n@googlegroups.com>

  copy mid

https://www.novabbs.com/tech/article-flat.php?id=129873&group=sci.math#129873

  copy link   Newsgroups: sci.math
X-Received: by 2002:a05:622a:1a15:b0:3de:6674:4778 with SMTP id f21-20020a05622a1a1500b003de66744778mr1166457qtb.2.1679240461661;
Sun, 19 Mar 2023 08:41:01 -0700 (PDT)
X-Received: by 2002:a25:9384:0:b0:afa:d8b5:8e82 with SMTP id
a4-20020a259384000000b00afad8b58e82mr3517203ybm.6.1679240461378; Sun, 19 Mar
2023 08:41:01 -0700 (PDT)
Path: i2pn2.org!i2pn.org!diablo1.usenet.blueworldhosting.com!usenet.blueworldhosting.com!85.12.63.49.MISMATCH!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Sun, 19 Mar 2023 08:41:01 -0700 (PDT)
In-Reply-To: <9a7c1fe6-036b-4bc3-87b3-ffc62526d1e1n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
References: <9a7c1fe6-036b-4bc3-87b3-ffc62526d1e1n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <671f1195-1de9-4106-a226-131994c930e5n@googlegroups.com>
Subject: Re: Revisiting Smullyan's Drinker's Paradox
From: Dan_Chri...@sympatico.ca (Dan Christensen)
Injection-Date: Sun, 19 Mar 2023 15:41:01 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 4532
 by: Dan Christensen - Sun, 19 Mar 2023 15:41 UTC

On Friday, March 17, 2023 at 11:01:30 PM UTC-4, Dan Christensen wrote:
> Back from vacation! In honour of St. Patrick's Day, here is an alternative version of Smullyan's proof of the Drinker's Paradox/Principle, which he states as follows:
>
> "[T]here exists someone such that whenever he (or she) drinks, everybody drinks."
> --Raymond Smullyan, "What is the name of this book?" 1978, p. 209
>

Here I explicitly make the "domain of discourse" to be the inhabitants of a given pub. This seems to be the implicit, unstated case in Smullyan's proof.

THEOREM
EXIST(a):InPub(a)
=> EXIST(b):[InPub(b)& [Drinker(b) => ALL(c):[InPub(c) => Drinker(c)]]]

PROOF
Suppose...

1. EXIST(a):InPub(a)
Premise

Two cases to consider:

2. ALL(c):[InPub(c) => Drinker(c)] | ~ALL(c):[InPub(c) => Drinker(c)]
Or Not

Case 1

Suppose...

3. ALL(c):[InPub(c) => Drinker(c)]
Premise

Define x:

4. InPub(x)
E Spec, 1

Applying the Arbitrary Antecedent Rule...

5. Drinker(x) => ALL(c):[InPub(c) => Drinker(c)]
Arb Ante, 3

6. InPub(x)
& [Drinker(x) => ALL(c):[InPub(c) => Drinker(c)]]
Join, 4, 5

7. EXIST(b):[InPub(b)
& [Drinker(b) => ALL(c):[InPub(c) => Drinker(c)]]]
E Gen, 6

Case 1
As Required:

8. ALL(c):[InPub(c) => Drinker(c)]
=> EXIST(b):[InPub(b)
& [Drinker(b) => ALL(c):[InPub(c) => Drinker(c)]]]
Conclusion, 3

Case 2

Suppose...

9. ~ALL(c):[InPub(c) => Drinker(c)]
Premise

10. ~~EXIST(c):~[InPub(c) => Drinker(c)]
Quant, 9

11. EXIST(c):~[InPub(c) => Drinker(c)]
Rem DNeg, 10

12. EXIST(c):~~[InPub(c) & ~Drinker(c)]
Imply-And, 11

13. EXIST(c):[InPub(c) & ~Drinker(c)]
Rem DNeg, 12

14. InPub(y) & ~Drinker(y)
E Spec, 13

Define: y

15. InPub(y)
Split, 14

16. ~Drinker(y)
Split, 14


Suppose...

17. Drinker(y)
Premise

Applying the Arbitrary Consequent Rule...

18. ~Drinker(y) => ALL(c):[InPub(c) => Drinker(c)]
Arb Cons, 17

19. ALL(c):[InPub(c) => Drinker(c)]
Detach, 18, 16

As Required:

20. Drinker(y) => ALL(c):[InPub(c) => Drinker(c)]
Conclusion, 17

21. InPub(y)
& [Drinker(y) => ALL(c):[InPub(c) => Drinker(c)]]
Join, 15, 20

22. EXIST(b):[InPub(b)
& [Drinker(b) => ALL(c):[InPub(c) => Drinker(c)]]]
E Gen, 21

As Required:

23. ~ALL(c):[InPub(c) => Drinker(c)]
=> EXIST(b):[InPub(b)
& [Drinker(b) => ALL(c):[InPub(c) => Drinker(c)]]]
Conclusion, 9

24. [ALL(c):[InPub(c) => Drinker(c)]
=> EXIST(b):[InPub(b)
& [Drinker(b) => ALL(c):[InPub(c) => Drinker(c)]]]]
& [~ALL(c):[InPub(c) => Drinker(c)]
=> EXIST(b):[InPub(b)
& [Drinker(b) => ALL(c):[InPub(c) => Drinker(c)]]]]
Join, 8, 23

25. EXIST(b):[InPub(b)
& [Drinker(b) => ALL(c):[InPub(c) => Drinker(c)]]]
Cases, 2, 24

As Required:

26. EXIST(a):InPub(a)
=> EXIST(b):[InPub(b)
& [Drinker(b) => ALL(c):[InPub(c) => Drinker(c)]]]
Conclusion, 1

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

Re: Revisiting Smullyan's Drinker's Paradox

<8ed949b7-0750-4da7-b4cc-67c602d2ecbbn@googlegroups.com>

  copy mid

https://www.novabbs.com/tech/article-flat.php?id=133672&group=sci.math#133672

  copy link   Newsgroups: sci.math
X-Received: by 2002:ad4:4f13:0:b0:5ef:1718:2f7c with SMTP id fb19-20020ad44f13000000b005ef17182f7cmr2385565qvb.9.1683242424781;
Thu, 04 May 2023 16:20:24 -0700 (PDT)
X-Received: by 2002:a81:ae59:0:b0:54f:ae82:3f92 with SMTP id
g25-20020a81ae59000000b0054fae823f92mr2213229ywk.2.1683242424528; Thu, 04 May
2023 16:20:24 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!usenet.blueworldhosting.com!diablo1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Thu, 4 May 2023 16:20:24 -0700 (PDT)
In-Reply-To: <671f1195-1de9-4106-a226-131994c930e5n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.44; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.44
References: <9a7c1fe6-036b-4bc3-87b3-ffc62526d1e1n@googlegroups.com> <671f1195-1de9-4106-a226-131994c930e5n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <8ed949b7-0750-4da7-b4cc-67c602d2ecbbn@googlegroups.com>
Subject: Re: Revisiting Smullyan's Drinker's Paradox
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Thu, 04 May 2023 23:20:24 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 1730
 by: Mostowski Collapse - Thu, 4 May 2023 23:20 UTC

Very good. Why got this sacrified in favor of a Russell based proof?
Here is a challenge: Do you need Russell for the dual Drinker Paradox:

/* There is a guest if some guest drinks then this guest drinks */
16 ∃x:(∃y:d(y) ⊃ d(x))
▲ Conclusion 1,15

Dan Christensen schrieb am Sonntag, 19. März 2023 um 16:41:05 UTC+1:
> 26. EXIST(a):InPub(a)
> => EXIST(b):[InPub(b)
> & [Drinker(b) => ALL(c):[InPub(c) => Drinker(c)]]]
> Conclusion, 1

1
server_pubkey.txt

rocksolid light 0.9.81
clearnet tor