The Drinker’s Paradox: A Tale of Three Paradoxes (reposted)

[Dan Christensen]

The Drinker’s Theorem: Consider the set of all drinkers in the world, and the set of all people in a given pub. Then there exists a person who, if he or she is drinking, then everyone in that pub is drinking.

It doesn’t matter how many people are there. Or how many are drinking. Or how few. No one needs to be taking their cues from some “lead drinker,” but in every pub, in every town and village, it just happens! How is this possible?

There are several possible approaches to this problem. Here, we will turn to British philosopher and mathematician, Bertrand Russell (1872 – 1970). His famous Paradox is the key.

See: https://dcproof.wordpress.com/2014/06/03/the-drinkers-paradox/

Dan

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

[Mostowski Collapse]

Is this some sort of reference that our wonky man is always drunk?
Especially when he claims he posses some "right" definition?

[Dan Christensen]

On Wednesday, October 5, 2022 at 6:11:20 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 5. Oktober 2022 um 22:15:15 UTC+2:
> > The Drinker’s Theorem: Consider the set of all drinkers in the world, and the set of all people in a given pub. Then there exists a person who, if he or she is drinking, then everyone in that pub is drinking.
> >
> > It doesn’t matter how many people are there. Or how many are drinking. Or how few. No one needs to be taking their cues from some “lead drinker,” but in every pub, in every town and village, it just happens! How is this possible?
> >
> > There are several possible approaches to this problem. Here, we will turn to British philosopher and mathematician, Bertrand Russell (1872 – 1970). His famous Paradox is the key.
> >
> > See: https://dcproof.wordpress.com/2014/06/03/the-drinkers-paradox/
> >

> Is this some sort of reference that our wonky man is always drunk?
> Especially when he claims he posses some "right" definition?

You really seem to have a hard time with predicate abbreviations in math, Jan Burse. I suggest you avoid abbreviations if at all possible. They add another step in proofs that you just can't seem to get right. One too many complications, I guess.

[Mostowski Collapse]

I really enjoy your DC Spoiled proof tool. It is no applications
in mathematics whatever so far. But its a funny contraption to

refute all your nonsense claims, wonky man!

LMAO!

[Mostowski Collapse]

Except that your formalization is wrong. On the web you have:

EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]]
http://www.dcproof.com/DrinkersThm1.htm

Shouldn't this be?

EXIST(x):[x e pub & [x e drinkers => ALL(a):[a e pub => a e drinkers]]]
https://en.wikipedia.org/wiki/Drinker_paradox

Which has a counter model, when pub can be empty:

∃x(px ∧ (dx → ∀a(pa → da))) is invalid.
https://www.umsu.de/trees/#~7x%28p%28x%29~1%28d%28x%29~5~6a%28p%28a%29~5d%28a%29%29%29%29

But otherwise is generally valid:

∃xpx → ∃x(px ∧ (dx → ∀a(pa → da))) is valid.
https://www.umsu.de/trees/#~7xp%28x%29~5~7x%28p%28x%29~1%28d%28x%29~5~6a%28p%28a%29~5d%28a%29%29%29%29

Nothing to do with Set Theory, Universal Set or Russel Paradox.
Since it is valid for classes, I guess it is also valid for sets.

[Mostowski Collapse]

You can use it to show that FOL assume a non-empty
universe of discourse, at least it is consistent with
the fact that this is also generally valid in FOL:

∃x(dx → ∀ada) is valid.
https://www.umsu.de/trees/#~7x%28d%28x%29~5~6ad%28a%29%29

It has also a dual:

∀z(dz → ∃xdx) → ∀z∃x(dz → dx) is valid.
https://www.umsu.de/trees/#~6z%28dz~5~7xdx%29~5~6z~7x%28dz~5dx%29

The two above possibly not provable in DC Spooky, right?

LoL

See also:

The Drinker Paradox and its Dual - 2018
Warren L, Diener H and McKubre-Jordens M
https://ir.canterbury.ac.nz/bitstream/handle/10092/16234/1805.06216v1.pdf

[Dan Christensen]

On Thursday, October 6, 2022 at 11:22:25 AM UTC-4, Mostowski Collapse wrote:
> Except that your formalization is wrong. On the web you have:
>
> EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]]
> http://www.dcproof.com/DrinkersThm1.htm
>
> Shouldn't this be?
>
> EXIST(x):[x e pub & [x e drinkers => ALL(a):[a e pub => a e drinkers]]]
> https://en.wikipedia.org/wiki/Drinker_paradox
>

"x e pub" is redundant. The logic works for ANY drinker, whether in the pub or not. Maybe this was historically a feature of the original non-set-theoretical presentation of DP. The logic will also work for an empty pub.

> Which has a counter model, when pub can be empty:
>
> ∃x(px ∧ (dx → ∀a(pa → da))) is invalid.
> https://www.umsu.de/trees/#~7x%28p%28x%29~1%28d%28x%29~5~6a%28p%28a%29~5d%28a%29%29%29%29
>
> But otherwise is generally valid:
>
> ∃xpx → ∃x(px ∧ (dx → ∀a(pa → da))) is valid.
> https://www.umsu.de/trees/#~7xp%28x%29~5~7x%28p%28x%29~1%28d%28x%29~5~6a%28p%28a%29~5d%28a%29%29%29%29
>
> Nothing to do with Set Theory, Universal Set or Russel Paradox.

See the posting at my math blog. I use the non-existence of a universal set in proofs.

> Since it is valid for classes, I guess it is also valid for sets.

This is all strictly set theory. No "proper classes."

[Mostowski Collapse]

I wouldn't know that x e pub is redundant. The tree tool tells me
that it is not redundant. I get, for the crucial fact:

∃x(px ∧ (dx → ∀a(pa → da))) is invalid.
https://www.umsu.de/trees/#~7x%28p%28x%29~1%28d%28x%29~5~6a%28p%28a%29~5d%28a%29%29%29%29

But then:

∃x(dx → ∀a(pa → da)) is valid.
https://www.umsu.de/trees/#~7x(d(x)~5~6a(p(a)~5d(a)))

So nyet, x e pub is not redundant. If you think so, then there is
a bug somewhere in your blog. Or the problem is that

DC Spooky isn't FOL.

[Dan Christensen]

On Wednesday, October 5, 2022 at 4:15:15 PM UTC-4, Dan Christensen wrote:
> The Drinker’s Theorem: Consider the set of all drinkers in the world, and the set of all people in a given pub. Then there exists a person who, if he or she is drinking, then everyone in that pub is drinking.
>
> It doesn’t matter how many people are there. Or how many are drinking. Or how few. No one needs to be taking their cues from some “lead drinker,” but in every pub, in every town and village, it just happens! How is this possible?
>
> There are several possible approaches to this problem. Here, we will turn to British philosopher and mathematician, Bertrand Russell (1872 – 1970). His famous Paradox is the key.
>

I don't know if this is a truly novel approach to DP, but, on Google right now, after 8 years, my blog posting seems to be the only online connection between the two paradoxes.

From Wikipedia: "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 they are drinking, then everyone in the pub is drinking."
https://en.wikipedia.org/wiki/Drinker_paradox

My version of DP is based on set theory. It does not require the "lead drinker" to be in the pub. In fact, anything whatsoever is implied by his/her very existence. How cool is that???

It is a theorem of basic set theory that for any set S and ANY proposition Q, we have EXIST(x):[x in S => Q]. See....

[Ross A. Finlayson]

Says right there on the Wiki "material implication is lazy and erroneous",
or rather "in the modality of the passage of time in a pub, either one person
drinks last, or multiple people drink last, or they had no business that day".

[Ross A. Finlayson]

If you like Occam's razor you might enjoy Schaffer's laser.

[Mostowski Collapse]

One really wonders what wonky many was smoking when he
did the Drinker paradox. It doesn't follow Occams razor,
its just some backed nonsense. You use some withess x

such that ~(x e drinkers) to show. Which you first draw
from Rusells paradox it seems:

EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]]
http://www.dcproof.com/DrinkersThm1.htm

But the proof here:

∃x(Exd → ∀a(Eap → Ead)) is valid.
https://www.umsu.de/trees/#~7x%28Exd~5~6a%28Eap~5Ead%29%29

Proceeds the same way like the proof here, the second a e pub is redundant:

∃x(Exd → ∀aEad) is valid.
https://www.umsu.de/trees/#~7x%28Exd~5~6aEad%29

Both proofs succeeds because they lead to:
~Ebd , Ebd

Noting to do with really deriving ~(x e drinkers) first from
some Russel paradox as you do. Thats utter nonsense. The drinker
paradox is LEM together with some quantifier rules.

p v ~p
https://en.wikipedia.org/wiki/Law_of_excluded_middle

[Mostowski Collapse]

Interestingly both proofs use also contraction.
But they don't need Russells paradox per se.
The original statement is copied twice.

Although some versions of Russells paradox
and also some versions of Currys paradox, also
depend on contraction. So maybe you have a small

point. But Russells paradox uses x e x, which I
don't see in the Drinker paradox. Is there somewhere
drinker e drinker or x e x or pub e pub? No, not at all!

What an utter nonsense!

[Mostowski Collapse]

Here is a proof of the Drinker paradox, that doesn't
use first Russells Paradox. Namely I find speedily,
even in DC Spoiled:

21 ALL(d):EXIST(x):[x ε d => ALL(a):a ε d]
Rem DNeg, 20

But it has a twist, it indeed leads to some Russells
like d e d (sic!). But this happens out of sheer lack
to invent new variables during a proof,

other proof tools don't need this trick. If I have time
I will show such a proof tool. I wasn't successfull with
the Wolfgang Schwartz tree tool, it also falls back to

d e d, see this GitHub issue:

Strange tendency to turn the Drinker Paradox into a Russell Paradox
https://github.com/wo/tpg/issues/21

One can also look at the proofs here, none of the
proofs does some Russell stuff like for example P(P),
which would be the analogue if you are not in set theory,

so maybe Dan Christensen has become slave of his tool?
Not master of logic anymore, but slave of what the tool
dictates, including some Russell nonsense?

Proof of Drinker paradox [duplicate]
https://math.stackexchange.com/questions/807092/proof-of-drinker-paradox

--------------------------- begin proof ---------------------

1 ~EXIST(x):[x ε d => ALL(a):a ε d]
Premise

2 ~~ALL(x):~[x ε d => ALL(a):a ε d]
Quant, 1

3 ALL(x):~[x ε d => ALL(a):a ε d]
Rem DNeg, 2

4 ~[d ε d => ALL(a):a ε d]
U Spec, 3

5 ~~[d ε d & ~ALL(a):a ε d]
Imply-And, 4

6 d ε d & ~ALL(a):a ε d
Rem DNeg, 5

7 d ε d
Split, 6

8 ~ALL(a):a ε d
Split, 6

9 ~~EXIST(a):~a ε d
Quant, 8

10 EXIST(a):~a ε d
Rem DNeg, 9

11 ~b ε d
E Spec, 10

12 ~[b ε d => ALL(a):a ε d]
U Spec, 3

13 ~~[b ε d & ~ALL(a):a ε d]
Imply-And, 12

14 b ε d & ~ALL(a):a ε d
Rem DNeg, 13

15 b ε d
Split, 14

16 ~ALL(a):a ε d
Split, 14

17 ~b ε d & b ε d
Join, 11, 15

18 ~EXIST(d):~EXIST(x):[x ε d => ALL(a):a ε d]
Conclusion, 1

19 ~~ALL(d):~~EXIST(x):[x ε d => ALL(a):a ε d]
Quant, 18

20 ALL(d):~~EXIST(x):[x ε d => ALL(a):a ε d]
Rem DNeg, 19

21 ALL(d):EXIST(x):[x ε d => ALL(a):a ε d]
Rem DNeg, 20

--------------------------- end proof ---------------------

[Dan Christensen]

Well done, Jan Burse! Line 4 with "d in d" bothers me a bit, but it works.

Now prove the more general case, given any proposition Q and set s to obtain EXIST(b):[b in s => Q]. I think you will need RP for that.

Then DP will simply be a special case of this mind-blowing little theorem.

[Ross A. Finlayson]

That has a direct counterexample in that "in our pub you drink when you want".

[Mostowski Collapse]

The proof looks different if you use this:
Naoyuki Tamura seqprover for classical first-order logic.

------------- Ax
d(Z) --> d(Z)
--------------- R#
d(Z) --> Y#d(Y)
----------------- R->
--> d(Z)->Y#d(Y)
--------------------- R@
--> X@(d(X)->Y#d(Y))
------------------------ Ltop
top --> X@(d(X)->Y#d(Y))
https://www.vidal-rosset.net/g4-prover/g4action.php?formula=top+--%3E+X%40%28d%28X%29-%3EY%23d%28Y%29%29&sysopt=g4c&output=pretty

It invents a new variable Z, no need for d(d).
Thats the normal way to prove the Drinker paradox,

there is something strange going on with
Wolfgrang Schwartz tree tool.

[Mostowski Collapse]

The proof is also contraction free, and therefore shorter.
The original formula is only used once, and not twice.
In DC Spoiled I didn't manage to use the original formula

only once, I made the negated original formula a premis
to carry out the proof. But I had to use the original formula
twice. Is there a DC Spoiled proof which is as short as

the sequent calculus proof?

[Mostowski Collapse]

Oops, I guess I confused ALL() and EXISTS(),
but still no Russell Paradox, which would read d(d):

------------------------------------------- Ax-c
d(X1),d(Z) --> d(X1),d(Y1),X#(d(X)->Y@d(Y))
-------------------------------------------- R@
d(X1),d(Z) --> d(X1),Y@d(Y),X#(d(X)->Y@d(Y))
--------------------------------------------- R->
d(Z) --> d(X1),d(X1)->Y@d(Y),X#(d(X)->Y@d(Y))
--------------------------------------------- R#-c
d(Z) --> d(X1),X#(d(X)->Y@d(Y))
-------------------------------- R@
d(Z) --> Y@d(Y),X#(d(X)->Y@d(Y))
---------------------------------- R->
--> d(Z)->Y@d(Y),X#(d(X)->Y@d(Y))
---------------------------------- R#-c
--> X#(d(X)->Y@d(Y))
------------------------ Ltop
top --> X#(d(X)->Y@d(Y))

https://www.vidal-rosset.net/g4-prover/g4action.php?formula=top+--%3E+X%23%28d%28X%29-%3EY%40d%28Y%29%29+&sysopt=g4c&output=pretty

Contraction is still there!
And it invents a little more variables, Z, X1, Y1

[Dan Christensen]

On Friday, October 7, 2022 at 1:03:35 PM UTC-4, Mostowski Collapse wrote:
> Oops, I guess I confused ALL() and EXISTS(),
> but still no Russell Paradox, which would read d(d):
>
> ------------------------------------------- Ax-c
> d(X1),d(Z) --> d(X1),d(Y1),X#(d(X)->Y@d(Y))
> -------------------------------------------- R@
> d(X1),d(Z) --> d(X1),Y@d(Y),X#(d(X)->Y@d(Y))
> --------------------------------------------- R->
> d(Z) --> d(X1),d(X1)->Y@d(Y),X#(d(X)->Y@d(Y))
> --------------------------------------------- R#-c
> d(Z) --> d(X1),X#(d(X)->Y@d(Y))
> -------------------------------- R@
> d(Z) --> Y@d(Y),X#(d(X)->Y@d(Y))
> ---------------------------------- R->
> --> d(Z)->Y@d(Y),X#(d(X)->Y@d(Y))
> ---------------------------------- R#-c
> --> X#(d(X)->Y@d(Y))
> ------------------------ Ltop
> top --> X#(d(X)->Y@d(Y))
>
> https://www.vidal-rosset.net/g4-prover/g4action.php?formula=top+--%3E+X%23%28d%28X%29-%3EY%40d%28Y%29%29+&sysopt=g4c&output=pretty
>

Have you been able to prove that, for any proposition Q, we have:

ALL(s):[Set(s) => EXIST(a):[a in s => Q]]?

Or ALL(s):EXIST(a):[a in s => Q]? (Without my Set predicate).

That's the really interesting part of all this. DP then becomes just a special case of this theorem.

[Ross A. Finlayson]

That's called "non-empty domains".

[Mostowski Collapse]

Its not relevant to the drinker paradox. You are completely
on the wrong track about the drinker paradox. Who
led you on this nonsense track wonky man? Let me explain.

Obviously when you prove the below sequent calculus proof,
and the sequent calculus uses contraction:

------------------------ Ltop
top --> X#(d(X)->Y@d(Y))

Which is equivalent to proving:

-------------------------------------------
EXIST(x):[d(x) => ALL(y):d(y)]

The because the proof uses contraction, this is a sign
that there is some PROOF BY CASES going on. There
are these two cases namely:

Case 1: EXIST(x):~d(x), or lets say ~d(x0) and x0
is the witness. We then have ex falso quodlibet,
we can choose for the x in EXIST(x) the value x0,

and then get:

~d(x0) => ALL(y):d(y)

Which is true since ~d(x0) true. Simple
material implication. It is row 1. and 2. here:

A B A => B
1. 0 0 1
2. 0 1 1
3. 1 0 0
4. 1 1 1

Case 2: ~EXIST(x):~d(x), this logically equivalent
to ALL(y):d(y). We then have verum stays verum. So
the contrary case to case 1, is case 2 where ALL(y):d(y)

is true and we get again, now irrelevant what z is:

~d(z) => ALL(y):d(y)

Which is true since ALL(y):d(y) is true. Simple
material implication. It is row 2. and 4. here:

A B A => B
1. 0 0 1
2. 0 1 1
3. 1 0 0
4. 1 1 1

Got it? Do you understand the Drinker Paradox now?

[Mostowski Collapse]

Your nonsense proof here is not the Drinker Paradox:
http://www.dcproof.com/DrinkersThm1.htm

It doesn't have contraction, i.e. this inference rule:

A v A
---------------------------- (Contr)
A

which would be a sign that the formula A is needed from
two different angles. You start with some nonsense

EXIST(a):~a e drinkers
Detach, 4, 2

Which is only case 1, but there are two cases,

Case 1: EXIST(x):~d(x)

Case 2: ~EXIST(x):~d(x)

Both make the Drinker Paradox formula true.
Since they are opposite cases, you can use proof
by cases as a proof method, basically this here:

(A => B) & (~B => A) => A

How old is your Drinker Pradox? Damn wonky
man, do you want to tell us you wasted 18 years
also here, its not only the function spaces,

but also the Drinker Paradox which challenges
you already for years and years? Congratulations
you are a true crank, much worse than AP brain farto.

[Mostowski Collapse]

I doubt that your set theoretic take is still the drinker
paradox. What is the ambivalence of the drinker paradox,
if you have anyway a non-drinker? There is no ambivalence

anymore, there is no paradoxical situation, in that contrary
situations lead to the same out come. Youcan go about
the internet, and easily find the approach to "resolve" the

drinker paradox, in that one proves this ambivalence, by
proof by cases, in pratically all corners of the internet,
like for example here, the case 2 and case 1 explaind:

"Proof of the paradox
The proof begins by recognising it is true that either everyone
in the pub is drinking (in this particular round of drinks), or
at least one person in the pub isn't drinking."
https://paradox.fandom.com/wiki/Drinker_paradox

[Mostowski Collapse]

You can then go further, for experts only, and draw
from it further didactic value, quite different from
your marriage in hell between Russell and Smullyan,

"This proof illustrates several properties of classical
predicate logic which do not always agree with
ordinary language.
Non-Empty Domain
Excluded Middle"
https://paradox.fandom.com/wiki/Drinker_paradox

[Dan Christensen]

> Its not relevant to the drinker paradox. You are completely
> on the wrong track about the drinker paradox.

[snip]

Wrong again, Jan Burse. If you let s be the set of all drinkers and Q be the proposition that everyone in the pub in question is a drinker, then you get the required result (requires RP AFAIK). Get it? Didn't think so. Oh, well...

[Mostowski Collapse]

Show us a DC Spoiled proof of your nonsense, and we will
be able to pinpoint more clearly what goes wrong. Its always
the same game, circle of life of DC Spoiled, a lot of bla bla and

then some retract. It is not the desired result. You dont understand
paradoxes, and if they use phrases such as:

- Drinker Paradox: The people in a pub ...
- Liar Paradox: The people on an island ...
- Etc... Etc...

You don't understand what this means right? Thats only another
way to say domain of discourse. You showed yourself that
there is no universal set, but if pub stands for the domain of discourse,

how can you say for example this here:

EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]]
http://www.dcproof.com/DrinkersThm1.htm

Its utter nonsense. You turn the domain of discourse pub into a set.
That will not work, its already the wrong modelling. On the other hand
a predicate P(_) could have the extension of the domain of discourse,

but _ e pub cannot have the extension of the domain of discourse. Here
is a proof that pub cannot have the extension of the domain of discourse,
using your own previouse result:

/* Previous Result http://www.dcproof.com/UniversalSet.htm */
1 ALL(s):[Set(s) => EXIST(a):~a ε s]
Axiom

2 Set(pub)
Axiom

3 Set(pub) => EXIST(a):~a ε pub
U Spec, 1

4 EXIST(a):~a ε pub
Detach, 3, 2

[Dan Christensen]

On Friday, October 7, 2022 at 7:39:35 PM UTC-4, Mostowski Collapse wrote:

> > Wrong again, Jan Burse. If you let s be the set of all drinkers and Q be the proposition that everyone in the pub in question is a drinker, then you get the required result (requires RP AFAIK). Get it? Didn't think so. Oh, well...

> Show us a proof ....

Thought you would never ask! See http://www.dcproof.com/STGeneralizedDrinkersThm.htm

There, I proved that

ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]

Don't be confused by the arguments "(x,s)." It could as easily have been simply Q on line 6.

[snip nonsense]

> Here
> is a proof that pub cannot have the extension of the domain of discourse,
> using your own previouse result:
>
> /* Previous Result http://www.dcproof.com/UniversalSet.htm */

> 1 ALL(s):[Set(s) => EXIST(a):~a ε s] <---- Every set excludes something, i.e. there exists no set of all things in set theory.

> Axiom
>
> 2 Set(pub)
> Axiom
>
> 3 Set(pub) => EXIST(a):~a ε pub
> U Spec, 1
>
> 4 EXIST(a):~a ε pub
> Detach, 3, 2

Wrong again, Jan Burse. This just proves that there exists something that is not an element of the set pub. (From Russell's Paradox.)

Get it? Didn't think so. Oh, well...

Dan

[Fritz Feldhase]

On Wednesday, October 5, 2022 at 10:15:15 PM UTC+2, Dan Christensen wrote:

> The Drinker’s [Paradox].

Rather a quite trivial observation. In the context of FOPL we have:

Ex(Dx -> Ay(Py -> Dy)).

There are two reasons, why this theorem holds in the context of FOPL:

1. the "paradoxical" properties of implication (->)
2. the fact that the domain of discourse in FOPL is non-empty

In fact, in propositional logic there is the well know tautology

A -> (B -> A).

(It holds because of 1.)

Now in the context of predicate logic we may substitute the predicates Dx and Px for A and B, resp. The generalization of the resuling formula gives the theorem

AxAy(Dx -> (Py -> Dy)).

Now it's well known that we can "shift" the quantifier "Ay" in this case, leading to the theorem

Ax(Dx -> Ay(Py -> Dy)).

Finally, in FOPL we have the theoem schema

AxPhi[x] -> ExPhi[x]

because the domain of FOPL is non-empty. (Hence if ALL objects in the domain of discourse have a certain property, say Phi, then at least one objects in the domain of discourse has that property.)

This way we get the theorem

Ex(Dx -> Ay(Py -> Dy)).

Nuff said.

------------------------------------------------------------------------------------------------------------------------------

Intuitively: [For the sake of the argument we will restrict our considerations to persons. Hence it's clear that our "universe of discourse" is not empty.]

Assume that all persons in the bar are drinkers. This means that

Ay(Py -> Dy)

is true. But then (by the properties of ->)

Da -> Ay(Py -> Dy)

is [trivially] true [see the TT of ->] for any person a [no matter if Da is true or not]. Hence we get:

Ex(Dx -> Ay(Py -> Dy)).

Now assume that not all persons in the bar are drinkers. This means that there is at least one person, let's call it b, such that

Db

is false. In this case the statement

Db -> Ay(Py -> Dy) ,

is [vacuously] true [see the TT of ->].

Hence again we get

Ex(Dx -> Ay(Py -> Dy)).

Hence in any case,

Ex(Dx -> Ay(Py -> Dy)).

qed

[Dan Christensen]

On Saturday, October 8, 2022 at 5:16:33 AM UTC-4, Fritz Feldhase wrote:
> On Wednesday, October 5, 2022 at 10:15:15 PM UTC+2, Dan Christensen wrote:
>
> > The Drinker’s [Paradox].
>
> Rather a quite trivial observation. In the context of FOPL we have:
>
> Ex(Dx -> Ay(Py -> Dy)).
>
> There are two reasons, why this theorem holds in the context of FOPL:
>
> 1. the "paradoxical" properties of implication (->)
> 2. the fact that the domain of discourse in FOPL is non-empty
>

[snip]

No need for a non-empty domain of discourse. From ordinary set theory, for any set s and proposition Q, we have: EXIST(x):[x in s => Q]

Proof

Let s be any set and let Q be any proposition (be it true or false).

From the resolution of Russell's Paradox, there cannot exist a set of all things, i.e. every set must exclude something. So, we must have x such that ~(x in s)

Introducing disjunction, we have: ~(x in s) | Q <----- ('|' = OR-operator in DC Proof)

Generalizing, we have: EXIST(x):[~(x in s) | Q], or equivalently EXIST(x):[x in s => Q] as required.

Example

If we let s = the set of all drinkers in the world, p = the set of all people in a given pub, and let Q be ALL(y):[y in p => y in s] , then, applying the above result, we can obtain the drinkers paradox/theorem. It is just a special case the above theorem.

[Fritz Feldhase]

On Saturday, October 8, 2022 at 4:01:27 PM UTC+2, Dan Christensen wrote:
> On Saturday, October 8, 2022 at 5:16:33 AM UTC-4, Fritz Feldhase wrote:
> > On Wednesday, October 5, 2022 at 10:15:15 PM UTC+2, Dan Christensen wrote:
> > >
> > > The Drinker’s [Paradox].
> > >
> > Rather a quite trivial observation. In the context of FOPL we have:
> >
> > Ex(Dx -> Ay(Py -> Dy)).
> >
> > There are two reasons, why this theorem holds in the context of FOPL:
> >
> > 1. the "paradoxical" properties of implication (->)
> > 2. the fact that the domain of discourse in FOPL is non-empty
> >
> [snip]
>
> No need for a non-empty domain of discourse.

Shut up, idiot. You are too dumb for any form of math.

[Dan Christensen]

Still in denial, I see. Oh, well....

[Fritz Feldhase]

On Saturday, October 8, 2022 at 4:26:29 PM UTC+2, Dan Christensen wrote:

> Still in denial, I see. Oh, well....

Yeah whatever.

[Mostowski Collapse]

About Dan Christensens Schrödinger Drinking Paradox:

You produced generalized nonsense. You will be possibly remembered
as the most schizophrenic crank on sci.math and sci. logic. First
you start with this nonsense:
1) Sets are Bad 1: Sets are bad, because with ordinals we
would have 3 e 4, i.e. less than becomes membership.
2) Sets are Bad 2: Sets are bad, because as far as I (wonky man)
can tell, mathe text books don't use set theory.
3) What else from the mouth of Dan Christensen (wonky man)?

As soon as one has rubbed his eyes to see the above nonsense
more cleary, Dan Christensen turns around the corner and claims
the contrary, namely:
4) We need Sets 1: If you tell him we work in the natural numbers,
he turns around the corner yes, but you need to use x e N.
5) We need Sets 2: Although Drinker Paradox is a FOL paradox,
he now believes its a FOL+SET paradox.
6) What else from the mouth of Dan Christensen?

Whats next, the moon is made out of green cheese and
I (wonky man) am a Cat and not a Cat?

[Mostowski Collapse]

To the best of my knowledge the Drinker Paradox is a FOL
paradox and not a FOL+SET paradox, you can read here:

"Proof of the paradox
The proof begins by recognising it is true that either everyone
in the pub is drinking (in this particular round of drinks), or
at least one person in the pub isn't drinking."
https://paradox.fandom.com/wiki/Drinker_paradox

And if you would dig deeper, it would even reveal some
miractles about the below topics, I have highlighted the
phrase **classical predicate logic** aka FOL.

"This proof illustrates several properties of **classical
predicate logic** which do not always agree with

ordinary language.
Non-Empty Domain
Excluded Middle"
https://paradox.fandom.com/wiki/Drinker_paradox

The term FOL alone doesn't imply that we look at FOL+SET.
But you need to leave classical predicate logic for a deeper
understanding, which you are completely lacking, since you

look at FOL+SET. On the quantifier side this could be free
logic (for the Non-Empty Domain issue). But of course non-
classicality in the propositional connectives might also be

interesting to dig deeper (for the Excluded Middle issue).
How the later is done, you might want to consult this here:

The Drinker Paradox and its Dual - Louis Warren et al., 2018
https://ir.canterbury.ac.nz/bitstream/handle/10092/16234/1805.06216v1.pdf

[Dan Christensen]

On Saturday, October 8, 2022 at 11:03:45 AM UTC-4, Mostowski Collapse wrote:
> About Dan Christensens Schrödinger Drinking Paradox:
>
> You produced generalized nonsense.

Sadly, for you, you could find no actual fault in my proofs here. You are reduced to lashing out at me personally. Pathetic.

[snip childish abuse]

> 1) Sets are Bad 1:

[snip]

As you can see from the above proof, I make extensive use of set theory. Did you notice the Sets Menu in DC Proof?

> 2) Sets are Bad 2: Sets are bad, because as far as I

> can tell, mathe text books don't use set theory.

As I have repeated pointedly out to you, they, too, make extensive use of set theory, but you don't like that they make your "dark elements" impossible. You might also have a look at my blog posting, "The Barber Paradox Revisited: Why we need set theory."

> If you tell him we work in the natural numbers,
> he turns around the corner yes, but you need to use x e N.

Only if you also want to have subsets, Cartesian products, functions, etc.

> 5) We need Sets 2: Although Drinker Paradox is a FOL paradox,
> he now believes its a FOL+SET paradox.

[snip more childish abuse]

I use the same rules of logic and set theory that are implicitly used in most math textbooks. Hint: Not standard FOL or ZFC theory. Deal with it, Jan Burse.

[Dan Christensen]

On Saturday, October 8, 2022 at 11:17:19 AM UTC-4, Mostowski Collapse wrote:
> To the best of my knowledge the Drinker Paradox is a FOL
> paradox and not a FOL+SET paradox, you can read here:

Pay attention, Jan Burse. Recall that I wrote in my original posting here: "There are several possible approaches to this problem. Here, we will turn to British philosopher and mathematician, Bertrand Russell (1872 – 1970). His famous Paradox is the key."

AFAICT this is an original approach. It makes use of the theorem: For any set S and proposition Q, we have EXIST(x):[x in S => Q].

[Fritz Feldhase]

On Saturday, October 8, 2022 at 11:16:33 AM UTC+2, Fritz Feldhase wrote:
>
> Rather a quite trivial observation. In the context of FOPL we have:
>
> Ex(Dx -> Ay(Py -> Dy)).
>

> There are [three] reasons [it seems], why this theorem holds in the context of FOPL [i.e. classical logic]:

>
> 1. the "paradoxical" properties of implication (->)
> 2. the fact that the domain of discourse in FOPL is non-empty

3. excluded middle.

[Mostowski Collapse]

Bertrand Russell never approached the Drinker Paradox.
You are crazy. His Russell Paradox is from 1901, at
that time classical predicate logic wasn't even completely

born. On the other hand the Drinker Paradox is from
1978 and from Raymond Smullyan, where people already
knew more about classical predicate logic, what we

nowadays call FOL. So how should have Russell
have adressed Smullyan. Did Time flow backwards?

You are a nuthead!

[Mostowski Collapse]

The current FOL is from Frege and Gödel. For example
Gödel clearly explains how predicate logic can properly
deal with empty domains, whereas the Aristotelean

Logic Lectures: Gödel's Basic Logic Course at Notre Dame
https://arxiv.org/abs/1705.02601

Term Logic often had existential import. The current
FOL setting is from around 1950s after Bertrand Russell.
That FOL is possible to cover both empty domains

and non empty domains is easily seen by this switchero.

Empty Domains Off:

/* Provable in FOL */
∃x(D(x) => ∀yD(y))

Empty Domains On:

/* Not Provable in FOL */
∃x(P(x) & (D(x) => ∀y(P(y) => D(y)))

The problem is that your DC Spoiled is also some nonsense
from before 1950. You have even botched it over the time
more, since for example you have tweeked some quantifier

rules, and what horror connected it to sets! What a complete
utter nonsense. Your DC Spoiled can even not handle FOL
properly. And your conflation of Russel and Smullyan has

the only goal to write some blog, although DC Spoiled
has nothing to contribute to the Drinker Paradox, since it
is not properly FOL, it can even not prove:

/* Not Provable in DC Spoiled, but Provable in FOL */
∃x(D(x) => ∀xD(x))

[Dan Christensen]

See my reply just now to your identical posting at sci.math

Dan

On Saturday, October 8, 2022 at 4:34:15 PM UTC-4, Mostowski Collapse wrote:
> Bertrand Russell never approached the Drinker Paradox.
> You are crazy. His Russell Paradox is from 1901, at
> that time classical predicate logic wasn't even completely
>

[snip]

[Mostowski Collapse]

So you cannot proof in FOL with DC Proof:

/* Drinker Paradox, Not Provable in DC Proof, but Provable in FOL */
∃x(D(x) => ∀yD(y))

Right? Well I thought so, that you botched it.

[Mostowski Collapse]

Dan Christensen halucinated even more Sonntag, 9. Oktober 2022 um 00:21:58 UTC+2:
> What's more, the consequent can be ANY proposition whatsoever
https://groups.google.com/g/sci.math/c/hEQjzBmQIIw/m/T35rYRp8BQAJ

Thats just utter nonsense that makes it even worse,
and shows that you didn't understand the drinker paradox,
it obviously doesn't work for the Drinker Paradox.

You can try yourself:

∃x(Dx→Q) is invalid.
https://www.umsu.de/trees/#~7x%28D%28x%29~5Q%29

The point of the drinker paradox is exactly that Q is
not arbitary. Just check out the usual proof by cases,
where two cases are used. One of the cases needs that

Q is not arbitrary. What the hell are you doing wonky man?

For the two cases see here:

"The proof begins by recognising it is true that either
everyone in the pub is drinking (in this particular round
of drinks), or at least one person in the pub isn't drinking."
https://paradox.fandom.com/wiki/Drinker_paradox

[Dan Christensen]

See my replies just now to your last 2 identical postings at sci.math

Dan

On Saturday, October 8, 2022 at 6:45:12 PM UTC-4, Mostowski Collapse wrote:
> So you cannot proof in FOL with DC Proof:
>
> /* Drinker Paradox, Not Provable in DC Proof, but Provable in FOL */
> ∃x(D(x) => ∀yD(y))
>

[snip]

[Mostowski Collapse]

ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is not the Drinker
paradox, you bilstering idiot. Its only the Russel paradox, so
that it shows an outside element, you need subset axiom

to prove it, you just replaced negation by more general => Q:

∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) → ∀s(Ss → ∃a¬Eas) is valid.
https://www.umsu.de/trees/#~6k~7u%28Su~1~6a%28Eau~4%28Eak~1~3Eaa%29%29%29~5~6s%28Ss~5~7a~3Eas%29

∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) → ∀s(Ss → ∃a(Eas → Qxs)) is valid.
https://www.umsu.de/trees/#~6k~7u%28Su~1~6a%28Eau~4Eak~1~3Eaa%29%29~5~6s%28Ss~5~7a%28Eas~5Qxs%29%29

S = your Set
E = your Membership
∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) = instance of Subset Axiom
∀s(Ss → ∃a¬Eas) = outside element
∀s(Ss → ∃a(Eas → Qxs)) = outside element again

It needs the Subset Axiom from some SET theory.
So its a proof in FOL+SET, you cannot prove it without SET, in FOL only:

∀s(Ss → ∃a¬Eas) is invalid.
https://www.umsu.de/trees/#~6s%28Ss~5~7a~3Eas%29

∀s(Ss → ∃a(Eas → Qxs)) is invalid.
https://www.umsu.de/trees/#~6s%28Ss~5~7a%28Eas~5Qxs%29%29

On the other hand the Drinker paradox works in FOL only:

∃a(Da → ∀bDb) is valid.
https://www.umsu.de/trees/#~7a%28Da~5~6bDb%29

Got it moron?

[Mostowski Collapse]

But the original Russell Paradox was not like this, it
wasn't using the non-naive set-builder. It used the naive
set-builder, and was communicated as such to Frege,

showing the Frege system inconsistent. You can also
use the naive set-builder to derive the outside element
theorem. But calling the non-naive version Drinker

Paradox, is of course a wonky man fallacy:

∃u∀a(Eau ↔ ¬Eaa) → ∀s∃a¬Eas is valid.
https://www.umsu.de/trees/#~7u~6a%28Eau~4~3Eaa%29~5~6s~7a~3Eas

But more shockingly for Frege, you can derive:

∀a(Eau ↔ ¬Eaa) → (Euu ∧ ¬Euu) is valid.
https://www.umsu.de/trees/#~6a%28Eau~4~3Eaa%29~5Euu~1~3Euu

See also here:

"Russell discovered the paradox in May or June 1901.
By his own account in his 1919 Introduction to Mathematical
Philosophy, he "attempted to discover some flaw in Cantor's

proof that there is no greatest cardinal. In a 1902 letter, he
announced the discovery to Gottlob Frege of the paradox
in Frege's 1879 Begriffsschrift."
https://en.wikipedia.org/wiki/Russell's_paradox#History

But he communicated a version with functions, how is this done?

[Mostowski Collapse]

Ha Ha, thats a wooping 23 years:

In a 1902 letter, he announced the discovery to Gottlob Frege
of the paradox in Frege's 1879 Begriffsschrift."
https://en.wikipedia.org/wiki/Russell's_paradox#History

Still more than the 18 years that wonky man is wasting
with DC Proof! Problems problems like with function spaces,
and from when is his Drinker Paradox blog?

So I guess wonky man will not surrender, we will still hear
more nonsense from wonky man, for quite some time!

[Dan Christensen]

See my reply just now to your identical posting at sci.math

Dan

On Sunday, October 9, 2022 at 4:57:36 AM UTC-4, Mostowski Collapse wrote:
> ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is not the Drinker
> paradox, you bilstering idiot. Its only the Russel paradox, so
> that it shows an outside element, you need subset axiom
>
> to prove it, you just replaced negation by more general => Q:
>

[snip]

[Ross A. Finlayson]

Subset or proper subset?


Here "Hartogs is the Pope, not Russell, ..., who is also not the Pope".

"Is Hartogs even Catholic?"

"Russell, is not the Pope."

[Mostowski Collapse]

How should ALL(s):[Set(s) => EXIST(x):[x in s => Q] even relate
to the Drinker Paradox when Q is not ALL(y):D(y) and x in s is not D(x)?

If it were a Russel Paradox as well, it would be listed here:

-The barber with "shave".
-The Grelling–Nelson paradox with "describer":
-Richard's paradox with "denote":
- "I am lying.", namely the liar paradox and Epimenides paradox,
- Russell–Myhill paradox
-The Burali-Forti paradox,
-The Kleene–Rosser paradox,
-Curry's paradox
-The smallest uninteresting integer paradox
-Girard's paradox
https://en.wikipedia.org/wiki/Russell's_paradox#Related_paradoxes

I don't see any Drinker Paradox in this list.

LMAO!

[Dan Christensen]

On Sunday, October 9, 2022 at 4:24:21 PM UTC-4, Mostowski Collapse wrote:
> How should ALL(s):[Set(s) => EXIST(x):[x in s => Q] even relate
> to the Drinker Paradox when Q is not ALL(y):D(y) and x in s is not D(x)?
>

Perhaps you didn't know, but it is often possible to formalize a problem in more than one way. Really! DP can be formalized with sets (as I have shown), predicates or a combination of both .

> If it were a Russel Paradox as well, it would be listed here:
>
> -The barber with "shave".
> -The Grelling–Nelson paradox with "describer":
> -Richard's paradox with "denote":
> - "I am lying.", namely the liar paradox and Epimenides paradox,
> - Russell–Myhill paradox
> -The Burali-Forti paradox,
> -The Kleene–Rosser paradox,
> -Curry's paradox
> -The smallest uninteresting integer paradox
> -Girard's paradox
> https://en.wikipedia.org/wiki/Russell's_paradox#Related_paradoxes
>
> I don't see any Drinker Paradox in this list.
>

AFAIK this purely set-theoretic resolution of DP is an original insight. Not a very profound insight, but original nevertheless.

Have you ever had an original insight, Jan Burse?

[Mostowski Collapse]

Perhaps you didn't know, but it is most often not possible to

formalize a problem in more than one way. Really!

For example set theory has no universal set, whereas
an universal predicate is not inconsistent:

ALL(x):U(x)

Doesn't lead to an inconsistency. It has a simple
model, namely U = V.

[Mostowski Collapse]

Finally, after a painful search, found a counter
example to Dan Christensens Drinker Paradox,

where he proofs that there is at least one non-drinker:

5 EXIST(a):~a e drinkers
Detach, 4, 2
http://www.dcproof.com/DrinkersThm1.htm

In this pub, I guess everybody is drinking:

Kerch Bridge on fire na na na na na
https://www.youtube.com/watch?v=xjy0vRvUsi8

[Julio Di Egidio]

On Wednesday, 5 October 2022 at 22:15:15 UTC+2, Dan Christensen wrote:

> The Drinker’s Theorem:
> Consider the set of all drinkers in the world,

Already wrong: drinkers are those people in the pub who are
drinking! Not per chance the informal statement given on
WP starts with "There is someone *in the pub* such that" (my
emphasis), and the formal statement starts with 'Ex in P s.t.'.

So something like:

Assume: set(P)
Assume: set(D) s.t. D subset P (improper)
Theorem: Exists(x in P) : [ (x in D) -> [ All(y in P) : (y in D) ] ]

or, for short:

Theorem: Exists(x in P) : [ (x in D) -> [ D = P ] ]

> and the set of all people in a given pub. Then there exists a person
> who, f he or she is drinking, then everyone in that pub is drinking.
>
> It doesn’t matter how many people are there.

It does: the theorem is false if there are no people at all.
Indeed, it's rather:

Assume: set(P) s.t. P =/= {}

> There are several possible approaches to this problem. Here, we will
> turn to British philosopher and mathematician, Bertrand Russell (1872
< – 1970). His famous Paradox is the key.

> See: https://dcproof.wordpress.com/2014/06/03/the-drinkers-paradox/

Since, as seen above, you botch the very statement of the
theorem, your entire line of reasoning is nonsense: take
already step 4, which is simply false re the actual theorem
statement, in case in fact everybody happens to be drinking
in the pub.

Back to the drawing board...

HTH,

Julio

[Mostowski Collapse]

Unfortunately it doesn't work with D = P:

∃xPx → ∃x(Px ∧ (Dx → ∀y(Dy ↔ Py))) is invalid.
https://www.umsu.de/trees/#~7xP%28x%29~5~7x%28P%28x%29~1%28D%28x%29~5~6y%28D%28y%29~4P%28y%29%29%29%29

Try P ⊆ D instead, that is the translation of All(y in P) : (y in D) .
Or alternatively would work if the side condition were no
only P =/= {} , but also D ⊆ P, we then have indeed a theorem,

some of the two formalization options that work, are thus:

∃xPx → ∃x(Px ∧ (Dx → ∀y(Py → Dy))) is valid.
https://www.umsu.de/trees/#~7xP%28x%29~5~7x%28P%28x%29~1%28D%28x%29~5~6y%28P%28y%29~5D%28y%29%29%29%29

∃xPx → (∀z(Dz → Pz) → ∃x(Px ∧ (Dx → ∀y(Dy ↔ Py)))) is valid.
https://www.umsu.de/trees/#~7xP%28x%29~5~6z%28D%28z%29~5P%28z%29%29~5~7x%28P%28x%29~1%28D%28x%29~5~6y%28D%28y%29~4P%28y%29%29%29%29

[Dan Christensen]

On Monday, October 10, 2022 at 5:37:40 AM UTC-4, Mostowski Collapse wrote:
> Perhaps you didn't know, but it is most often not possible to
> formalize a problem in more than one way. Really!
> For example set theory has no universal set, whereas
> an universal predicate is not inconsistent:
>
> ALL(x):U(x)
>
> Doesn't lead to an inconsistency. It has a simple
> model, namely U = V.

First-order predicate logic is apparently insufficient for some problems, even for something as mundane as the Barber Paradox. See my blog posting at https://dcproof.wordpress.com/2017/01/11/the-barber-paradox-revisited-why-we-need-sets/

Most of my blog postings provide what I think are probably original insights into common problems that plague students.

[Julio Di Egidio]

On Monday, 10 October 2022 at 15:19:21 UTC+2, Mostowski Collapse wrote:

> Unfortunately it doesn't work with D = P:
> ∃xPx → ∃x(Px ∧ (Dx → ∀y(Dy ↔ Py))) is invalid.

As you snip all assumptions, of course it doesn't work, you
spamming retard and another example of lying with "logic".

*Plonk*

Julio

[Julio Di Egidio]

On Monday, 10 October 2022 at 16:14:17 UTC+2, Dan Christensen wrote:
> On Monday, October 10, 2022 at 5:37:40 AM UTC-4, Mostowski Collapse wrote:
> > Perhaps you didn't know, but it is most often not possible to
> > formalize a problem in more than one way. Really!
> > For example set theory has no universal set, whereas
> > an universal predicate is not inconsistent:
> >
> > ALL(x):U(x)
> >
> > Doesn't lead to an inconsistency. It has a simple
> > model, namely U = V.
>
> First-order predicate logic is apparently insufficient for some problems, even for something as mundane as the Barber Paradox. See my blog posting at https://dcproof.wordpress.com/2017/01/11/the-barber-paradox-revisited-why-we-need-sets/
>
> Most of my blog postings provide what I think are probably original insights into common problems that plague students.

ESAD, you fucking moron and liar...

*Plonk*

Julio

[Dan Christensen]

On Monday, October 10, 2022 at 6:46:01 AM UTC-4, ju...@diegidio.name wrote:
> On Wednesday, 5 October 2022 at 22:15:15 UTC+2, Dan Christensen wrote:
>
> > The Drinker’s Theorem:
> > Consider the set of all drinkers in the world,
>
> Already wrong: drinkers are those people in the pub who are
> drinking!

This set is in lieu of an "is-a-drinker" (D) predicate.

" Not per chance the informal statement given on
> WP starts with "There is someone *in the pub* such that" (my
> emphasis), and the formal statement starts with 'Ex in P s.t.'.
>
> So something like:
>
> Assume: set(P)
> Assume: set(D) s.t. D subset P (improper)
> Theorem: Exists(x in P) : [ (x in D) -> [ All(y in P) : (y in D) ] ]
>
> or, for short:
>
> Theorem: Exists(x in P) : [ (x in D) -> [ D = P ] ]
>
> > and the set of all people in a given pub. Then there exists a person
> > who, f he or she is drinking, then everyone in that pub is drinking.
> >
> > It doesn’t matter how many people are there.
>
> It does: the theorem is false if there are no people at all.

For ANY sets "drinkers" (D) and "pub" (P), the theorem states, EXIST(x):[x in drinkers => ALL(a):[a in pub => a in drinkers]]

It would be vacuously true for empty P.

> Indeed, it's rather:
>
> Assume: set(P) s.t. P =/= {}

Not necessary.

> > There are several possible approaches to this problem. Here, we will
> > turn to British philosopher and mathematician, Bertrand Russell (1872
> < – 1970). His famous Paradox is the key.
> > See: https://dcproof.wordpress.com/2014/06/03/the-drinkers-paradox/
>
> Since, as seen above, you botch the very statement of the
> theorem,

Wrong again. See above.

> your entire line of reasoning is nonsense: take
> already step 4, which is simply false re the actual theorem
> statement, in case in fact everybody happens to be drinking
> in the pub.
>

Step 4 is proven at the link on line 1 using the logic of Russell's Paradox. Deal with it, Julio.

[Julio Di Egidio]

On Monday, 10 October 2022 at 17:03:04 UTC+2, Dan Christensen wrote:
> On Monday, October 10, 2022 at 6:46:01 AM UTC-4, ju...@diegidio.name wrote:
> > On Wednesday, 5 October 2022 at 22:15:15 UTC+2, Dan Christensen wrote:
> >
> > > The Drinker’s Theorem:
> > > Consider the set of all drinkers in the world,
> >
> > Already wrong: drinkers are those people in the pub who are
> > drinking!
>
> This set is in lieu of an "is-a-drinker" (D) predicate.

You still altogether miss the point. You are given a problem,
per se *not* about sets, *whose* domain of discourse is
"people in a pub" and nothing else, and to that the is-a-drinker
predicate applies. You then go on and formalize/encode that
in a set theory, but now the universe of discourse *of the set
theory* is all the possible sets for that theory, not just a set
of "people in a pub who may possibly be drinking", so the
original "universe" of the problem here maps to a specific set,
say P, and, along the same line, a set D, as encoding the notion
of "people in the pub who are in fact drinking", is and can only
be a subset of P!

> " Not per chance the informal statement given on
> > WP starts with "There is someone *in the pub* such that" (my
> > emphasis), and the formal statement starts with 'Ex in P s.t.'.

(Of course you couldn't care less for any existing
literature and how immediately wrong you are on
just that account already.)

> > > It doesn’t matter how many people are there.
> >
> > It does: the theorem is false if there are no people at all.
>
> For ANY sets "drinkers" (D) and "pub" (P), the theorem states,
> EXIST(x):[x in drinkers => ALL(a):[a in pub => a in drinkers]]

So, NO, that's NOT the theorem, you moron and liar, that's your
fucked-up rendition that has fuck-all to do with the given problem.

> > your entire line of reasoning is nonsense: take
> > already step 4, which is simply false re the actual theorem
> > statement, in case in fact everybody happens to be drinking
> > in the pub.
> >
> Step 4 is proven at the link on line 1 using the logic of Russell's
> Paradox. Deal with it, Julio.

Again: step 4, as the rest of your gibberish, has fuck-all to do
with the Drinker's Paradox!

You deal with it, you fucking moron and piece of lying shit who
dare talk of education and can't even get the very basics straight!!

EOD.

Julio

[Ross A. Finlayson]

Yes, ESAD.

[Julio Di Egidio]

> Yes, ESAD.

You guys are a fucking calamity.

Yes, ESAD for real, you fucking sociopaths.

*Plonk*

Julio

[Dan Christensen]

On Monday, October 10, 2022 at 11:32:15 AM UTC-4, ju...@diegidio.name wrote:
> On Monday, 10 October 2022 at 17:03:04 UTC+2, Dan Christensen wrote:
> > On Monday, October 10, 2022 at 6:46:01 AM UTC-4, ju...@diegidio.name wrote:
> > > On Wednesday, 5 October 2022 at 22:15:15 UTC+2, Dan Christensen wrote:
> > >
> > > > The Drinker’s Theorem:
> > > > Consider the set of all drinkers in the world,
> > >
> > > Already wrong: drinkers are those people in the pub who are
> > > drinking!
> >
> > This set is in lieu of an "is-a-drinker" (D) predicate.
> You still altogether miss the point. You are given a problem,
> per se *not* about sets, *whose* domain of discourse is
> "people in a pub" and nothing else, and to that the is-a-drinker
> predicate applies.

My proof works whether or not D is subset or a superset of P. And whether or not the "lead drinker" is in the pub of not. Is this sense, it might be seen as a generalization of the original proof that used only predicate logic.

> You then go on and formalize/encode that
> in a set theory, but now the universe of discourse *of the set
> theory* is all the possible sets for that theory,

There is no need for any overarching "universe of discourse" in mathematical proofs. Different quantifiers in a proof, even with the same statement, can have different, even disjoint domains. And they can even be empty. In set theory, there is not set of all sets either.

[snip childish abuse]

[Mostowski Collapse]

Your proof proves nonsense. For example:

5 EXIST(a):~a e drinkers
Detach, 4, 2
http://www.dcproof.com/DrinkersThm1.htm

There is nowhere an assumption of this kind in the Drinker Paradox.

Get lost wonky man.

[Dan Christensen]

On Monday, October 10, 2022 at 2:30:43 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 10. Oktober 2022 um 18:56:33 UTC+2:
> > On Monday, October 10, 2022 at 11:32:15 AM UTC-4, ju...@diegidio.name wrote:
> > > On Monday, 10 October 2022 at 17:03:04 UTC+2, Dan Christensen wrote:
> > > > On Monday, October 10, 2022 at 6:46:01 AM UTC-4, ju...@diegidio.name wrote:
> > > > > On Wednesday, 5 October 2022 at 22:15:15 UTC+2, Dan Christensen wrote:
> > > > >
> > > > > > The Drinker’s Theorem:
> > > > > > Consider the set of all drinkers in the world,
> > > > >
> > > > > Already wrong: drinkers are those people in the pub who are
> > > > > drinking!
> > > >
> > > > This set is in lieu of an "is-a-drinker" (D) predicate.
> > > You still altogether miss the point. You are given a problem,
> > > per se *not* about sets, *whose* domain of discourse is
> > > "people in a pub" and nothing else, and to that the is-a-drinker
> > > predicate applies.
> > My proof works whether or not D is subset or a superset of P. And whether or not the "lead drinker" is in the pub of not. Is this sense, it might be seen as a generalization of the original proof that used only predicate logic.
> > > You then go on and formalize/encode that
> > > in a set theory, but now the universe of discourse *of the set
> > > theory* is all the possible sets for that theory,
> > There is no need for any overarching "universe of discourse" in mathematical proofs. Different quantifiers in a proof, even with the same statement, can have different, even disjoint domains. And they can even be empty. In set theory, there is not set of all sets either.
> >
> > [snip childish abuse]

> Your proof proves nonsense. For example:
> 5 EXIST(a):~a e drinkers

Nothing "nonsensical" about that, Jan Burse. Here, "drinkers" is a set. Since no set can include everything (from RP), there must exist something that is NOT an element of "drinkers." Get it now, Jan Burse??? Did think so. Oh, well...

[Mostowski Collapse]

Its nonsensical to think that the Barber Paradox implies
that there is a barber that is not a man. This would be this
first order quantifier logic fallacy:

¬∃x(L(x)∧M(x))→∃x¬M(x)
https://www.umsu.de/trees/#~3~7x%28L%28x%29~1M%28x%29%29~5~7x~3M%28x%29

Your phrasing in http://www.dcproof.com/BP12.htm
might suggest that you are subject to this fallacy.
So you got tricked by what Wikipedia

calls a loaded question:

The question is a loaded question that assumes the existence
of the barber, which is false. A loaded question is a form of
complex question that contains a controversial assumption.
https://en.wikipedia.org/wiki/Loaded_question

Trying to solve a loaded question, and not point out that it is
loaded with some assumption that cannot be solved, is
of course not a very smart move.

[Mostowski Collapse]

¬∃x(Lx ∧ Mx) → ∃x¬Mx is invalid.
https://www.umsu.de/trees/#~3~7x%28L%28x%29~1M%28x%29%29~5~7x~3M%28x%29

Its not generally valid.

[Mostowski Collapse]

I guess wonky man is subject to a similar confusion
concerning the Drinker Paradox, just some fallacious

thinking when the paradox involves first order quantifier
logic, because quantfier dislexia, similar to WM.

[Ross A. Finlayson]

Drinkers forget every thing except drinking.

[Dan Christensen]

> Its nonsensical to think that the Barber Paradox implies
> that there is a barber that is not a man.

[snip nonsense]

Huh??? I have proven the following:

ALL(v):ALL(barber):ALL(m):[Set(v)
& barber in v
& Set(m)
& ALL(a):[a in m => a in v]

=> [EXIST(s):[ALL(a):ALL(b):[(a,b) in s => a in v & b in v]
& ALL(a):[a in m => [(barber,a) in s <=> ~(a,a) in s]]]

<=> ~barber in m]]

where

v = the set of all villagers

m = the set of all men in the village

s = the shaving relation on v, a set of ordered pairs, (x,y) in s means x shaves y

See: http://www.dcproof.com/BP12.htm

If there is even one invalid inference there, please point it out. Or, if you can prove the first-order equivalent of the above theorem, please do so. Can you even state its first-order equivalent?

[Mostowski Collapse]

Not a smart move, trying to prove a loaded question.
You lost your mind already years ago wonky man.

[Dan Christensen]

"Loaded question???" (HA, HA!)

Very evasive, Jan Burse. But thanks for confirming that you can do neither of these things. Oh, well...

Dan

[Mostowski Collapse]

You were never the smartes shed in the box.
This here is probably the biggest perversion
anybody has done to a paradox:

http://www.dcproof.com/BP12.htm

Its just useless garbage. There is no set m, in
the original paradox. Its just villagers. And
of course barber e v. Now please redo

your nonsense theorem.

(Hint woman don't need to shave, at least
for this paradox shave would mean to cutoff
a beard from a man, since the profession of

a barber is defined:

A barber is a person whose occupation is mainly
to cut, dress, groom, style and shave **men's** and
**boys'** hair or beards.
https://en.wikipedia.org/wiki/Barber

also in the present context the barber is a man
of course. So you don't need to go into gender
studies, and invent a Pink Unicorn,

there is just V = M and M(b), to arrive at or consider
~M(b) is obviously inconsistent garbage)

[Mostowski Collapse]

You are really a moron Dan Christensen, you don't understand
the verb shave, you state nonsense such as:

EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]
http://www.dcproof.com/BP12.htm

So in your take shave has domain and codomain V villagers,
which in your setting can have males and femals? Thats already
wrong, how can you deposit nonsense like EXIST(s):[ALL(a):

ALL(b):[(a,b) e s => a e v & b e v]. Or in words the moron Dan
Christensen might understand. The shave relation is a relation
where the codomain is men. The verb "shave" applies to men only!

cod(S) = { y | EXIST(x): (x,y) e S } = M

And since the paradox asks also about the shaving of
the barber himself, which hints that he is also a man,
there is something fishy with an answer such as:

"that barber is not a man."
http://www.dcproof.com/BP12.htm

Its just plain crazy nonsense.

[Dan Christensen]

> You were never the smartes shed in the box.

Umm.... OK.

:^P

> This here is probably the biggest perversion
> anybody has done to a paradox:
>
> http://www.dcproof.com/BP12.htm
>
> Its just useless garbage.

[snip more silliness]

Just admit you can't prove this basic result using only FOL. You really do need something like set theory.

[Mostowski Collapse]

You are so brain damaged wonky man, that you
don't see the analogue between these two?

- No Barber (Barber Paradox)
- No Universal Set (Russel Paradox)

You got carried away by a loaded question. The
Barber Pardox is a loaded question that assumes

the existence of the barber, which is false.

https://en.wikipedia.org/wiki/Barber_paradox

Not a smart move to follow the wrong lead of
a loaded question instead of dismissing it on
grounds of a wrong lead.

Not a smart move at all.

[Mostowski Collapse]

How to get to the Universal Set from the Barber,
just replace shaving Sxy with Set membership Eyx,
you get that this Universal Set cannot exist:

¬∃x∀y(Eyx ↔ ¬Eyy) is valid.
https://www.umsu.de/trees/#~3~7x~6y%28Eyx~4~3Eyy%29

The above ∀y(Eyx ↔ ¬Eyy) can be read that x would
be the Universal Set of all simply regular sets, i.e.
all sets y such that y e y. Works also with a

potentially empty domain. Unlike the Drinker Paradox
which requires a non-empty domain:

¬∃x(Dx ∧ ∀y(Dy → (Eyx ↔ ¬Eyy))) is valid.
https://www.umsu.de/trees/#~3~7x%28Dx~1~6y%28Dy~5%28Eyx~4~3Eyy%29%29%29

[Dan Christensen]

On Wednesday, October 12, 2022 at 12:26:02 PM UTC-4, Mostowski Collapse wrote:
> How to get to the Universal Set from the Barber,
> just replace shaving Sxy with Set membership Eyx,
> you get that this Universal Set cannot exist:
>

From the non-existence of the universal set (Russell): For any set S and proposition Q (be it true or false), we can obtain: EXIST(x):[x in S => Q]
http://www.dcproof.com/STGeneralizedDrinkersThm.htm

Again, if S is the set of drinkers, P is the set of people in a given pub and Q is ALL(a):[a in P => a in S], we have a set-theoretic version of DP.

[Mostowski Collapse]

Sound very crankish, to bring in the Drinker Paradox again.
Its like with Ellipses and Ovals, in the case of Archimedes
Plutonium, you might of course believe that the Drinker

Paradox is "solved" by some misterious set theory and
some always existing mysterious drinker? Where is he?
Is he in the pub? What is he, a Pink Unicorn? In the same

way that Archimedes Plutonium believes conic sections
are Ovals. Nevermind. Yolo, if you are happy as a crank?

[Mostowski Collapse]

Corr:.: Typo
some always existing mysterious non-drinker?

DC Proofs and Dan Christensense crank career:

How it started:
- Lets write a blog about Russell Paradox
- Lets also write a little bit about Drinker Paradox

How its going:
- Pink Unicorn in the Russell Paradox
~barber e m
http://www.dcproof.com/BP12.htm

- Pink Unicorn in the Drinker Paradox:
~a e drinkers
http://www.dcproof.com/DrinkersThm1.htm

I guess there is a system to this madness.

[Dan Christensen]

On Wednesday, October 12, 2022 at 1:54:47 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 12. Oktober 2022 um 19:40:45 UTC+2:

> > From the non-existence of the universal set (Russell): For any set S and proposition Q (be it true or false), we can obtain: EXIST(x):[x in S => Q]
> > http://www.dcproof.com/STGeneralizedDrinkersThm.htm
> >
> > Again, if S is the set of drinkers, P is the set of people in a given pub and Q is ALL(a):[a in P => a in S], we have a set-theoretic version of DP.

[snip childish abuse]

> you might of course believe that the Drinker
>
> Paradox is "solved" by some misterious set theory and
> some always existing mysterious drinker?

It may be mysterious to someone like you, Jan Burse, but it's really quite simple if you understand what a subset is.

See http://www.dcproof.com/DrinkersThm1.htm

> Where is he?
> Is he in the pub?

Unlike the original predicate-logic version of DP, there is no requirement that the supposed "lead drinker" be in the pub:

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

The proof works either way. Must be frustrating as hell for you, Jan Burse!

[Mostowski Collapse]

To the best of my knowledge there is no entailment ∃x~Dx:

∃x(Dx → ∀yDy) → ∃x¬Dx is invalid.
https://www.umsu.de/trees/#~7x%28Dx~5~6yDy%29~5~7x~3Dx

So where does this Pink Unicorn come from?
Ist this some new LGBT joke? Are you a wokeist?

[Mostowski Collapse]

I guess you are stretching it too much with your
prejudice and discrimination critique, especially
what concerns paradoxes. I mean I have

already heard people calling mathematics racist:

Modern Mathematics Confronts Its White, Patriarchal Past
https://www.scientificamerican.com/article/modern-mathematics-confronts-its-white-patriarchal-past/

But that you create Paradox variants with Pink
Unicorns one after the other, maybe go to a doctor
and check your bowels?

This Unicorn Changed the Way I Poop
https://www.youtube.com/watch?v=YbYWhdLO43Q

[Dan Christensen]

On Wednesday, October 12, 2022 at 2:30:40 PM UTC-4, Mostowski Collapse wrote:
> To the best of my knowledge there is no entailment ∃x~Dx:
>
> To the best of my knowledge there is no entailment ∃x~Dx:
>

[snip]

In DC Proof, we can prove: ALL(s):[Set(s) => EXIST(a):~a in s]

See http://www.dcproof.com/UniversalSet.htm

It makes use of the Subset Axiom. Easy. Only 28 lines.

[Mostowski Collapse]

Where do you see a subset axiom here:

∃x(Dx → ∀yDy) → ∃x¬Dx is invalid.
https://www.umsu.de/trees/#~7x%28Dx~5~6yDy%29~5~7x~3Dx

Don't under estimate your users. Its not a smart
move to turn paradoxes into travesties:

"Sissi - Das kluge Volk!"
https://www.youtube.com/watch?v=bSXcTovkF-o

[Dan Christensen]

On Wednesday, October 12, 2022 at 3:47:48 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen wrote:
> > On Wednesday, October 12, 2022 at 2:30:40 PM UTC-4, Mostowski Collapse wrote:
> >> To the best of my knowledge there is no entailment ∃x~Dx:
> >>
> >> To the best of my knowledge there is no entailment ∃x~Dx:
> >>
> > [snip]
> >
> > In DC Proof, we can prove: ALL(s):[Set(s) => EXIST(a):~a in s]
> >
> > See http://www.dcproof.com/UniversalSet.htm
> >
> > It makes use of the Subset Axiom. Easy. Only 28 lines.
> >

> Where do you see a subset axiom here:

Pay attention, Jan Burse. See line 4 at the above link:

4. EXIST(sub):[Set(sub) & ALL(a):[a in sub <=> a in u & ~a in a]]
Subset, 2

Any more questions?

[Mostowski Collapse]

Why should I pay attention to your nonsense?
You cannot prove this here:

∃x(Dx → ∀yDy) → ∃x¬Dx

Also not this here:

SET ∧ ∃x(Dx → ∀yDy) → ∃x¬Dx

What SET should work when D is a predicate symbol?
You are completely crazy.

Maybe Quines new foundation would work.

[Mostowski Collapse]

To have a SET that works for the Drinker Paradox,
you would need to have a concept of collection in
your SET that is more potent than predicate symbols.

So that ALL(x):D(x) would be not anymore a possibly
consistent assumption. I don't know many set theories
that go that far, that the concept of collection inside

the set theory is more powerful than predicates. Its
rather the other way around. But Quines new foundation
has more mention in connection with the Russell Paradox,

and not with the Drinker Paradox. Not sure whether
Quines new foundation would have any application for
the Drinker Paradox at all.

[Mostowski Collapse]

So what can be done to have the Drinker Paradox "solved"
in a new way via ∃x¬Dx , without turning it into a travesity,
i.e. taking it seriously that Dx is a predicate?

Maybe Tangled Type Theory (TTT) is the answer. Even
sci.logic visitors like Zuhair have picked up TTT:
https://mathoverflow.net/q/427351

In the above question you see also the provenance of
TTT, its from this paper here, by Randall Holmes,
which was submitted 2015 but has a 2022 revision!?

In this paper we will present a proof of the consistency
of Quine's set theory "New Foundations" (hereinafter NF),
so-called after the title of the 1937 paper in which it was

introduced. This version takes the approach of building a
model of tangled type theory rather than a model of the
usual set theory without choice with a tangled web of cardinals.
https://arxiv.org/abs/1503.01406

[Dan Christensen]

On Wednesday, October 12, 2022 at 4:57:47 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 12. Oktober 2022 um 22:06:30 UTC+2:
> > On Wednesday, October 12, 2022 at 3:47:48 PM UTC-4, Mostowski Collapse wrote:
> >
> > > Dan Christensen wrote:
> > > > On Wednesday, October 12, 2022 at 2:30:40 PM UTC-4, Mostowski Collapse wrote:
> > > >> To the best of my knowledge there is no entailment ∃x~Dx:
> > > >>
> > > >> To the best of my knowledge there is no entailment ∃x~Dx:
> > > >>
> > > > [snip]
> > > >
> > > > In DC Proof, we can prove: ALL(s):[Set(s) => EXIST(a):~a in s]
> > > >
> > > > See http://www.dcproof.com/UniversalSet.htm
> > > >
> > > > It makes use of the Subset Axiom. Easy. Only 28 lines.
> > > >
> > > Where do you see a subset axiom here:
> > Pay attention, Jan Burse. See line 4 at the above link:
> >
> > 4. EXIST(sub):[Set(sub) & ALL(a):[a in sub <=> a in u & ~a in a]]
> > Subset, 2
> >

> Why should I pay attention to your nonsense?
> You cannot prove this here:
>
> ∃x(Dx → ∀yDy) → ∃x¬Dx
>
> Also not this here:
>
> SET ∧ ∃x(Dx → ∀yDy) → ∃x¬Dx
>

So what? I proved: ALL(s):[Set(s) => EXIST(a):~a e s]

See http://www.dcproof.com/UniversalSet.htm

Must be frustrating as hell for you, Jan Burse! Deal with it.

[Dan Christensen]

On Wednesday, October 12, 2022 at 5:06:40 PM UTC-4, Mostowski Collapse wrote:

> Mostowski Collapse schrieb am Mittwoch, 12. Oktober 2022 um 22:58:39 UTC+2:

> So what can be done to have the Drinker Paradox "solved"
> in a new way

A paradox that has been solved is just a theorem.

My Drinker Theorem: EXIST(x):[x in drinkers => ALL(a):[a in pub => a in drinkers]] where drinkers and pub are arbitrary sets.

It is a corollary of ALL(s):[Set(s) => EXIST(x):[x in s => Q]], which is, in turn, a corollary of ALL(s):[Set(s) => EXIST(a):~a e s] (from RP).

[Mostowski Collapse]

What you proved is not the Drinker Paradox.
It goes by a different name.

Russell's paradox can also be viewed as a positive result.
Lemma: 3.8.2 (ECST) For every set A there is
a set AR such that ~(AR e A).
https://www1.maths.leeds.ac.uk/~rathjen/book.pdf

So whats the official name of Lemma: 3.8.2?
You find it in many other books as well?

Oh you don't plow books.
Now everything makes sense.

[Dan Christensen]

On Wednesday, October 12, 2022 at 5:58:11 PM UTC-4, Mostowski Collapse wrote:
> What you proved is not the Drinker Paradox.

I will continue to call it what it is. You can make up your own name if it helps you deal with it.

[Mostowski Collapse]

Well its wrong. The Drinker Paradox is only proving this:

∃x(Dx → ∀yDy) is valid.
https://www.umsu.de/trees/#~7x%28D%28x%29~5~6yDy%29

Not your nonsense that entails ∃x¬Dx and uses sets to model Dx.

Thats nick nack born in a crazy mind of a crank.

[Dan Christensen]

On Wednesday, October 12, 2022 at 6:16:02 PM UTC-4, Mostowski Collapse wrote:
> Well its wrong. The Drinker Paradox is only proving this:
>
> ∃x(Dx → ∀yDy) is valid.

Did you not say that this requires a non-empty domain of discussion? Such things do not exist in most math textbooks. Deal with it.

[Mostowski Collapse]

You prove nonsense like:

5 EXIST(a):~a e drinkers

Detach, 4, 2
http://www.dcproof.com/DrinkersThm1.htm

Did he walk out of the pub? Can you also prove
EXIST(a):[a e pub & ~a e drinkers] ? I guess no?

Can you prove:

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

What do you need to prove this proper Drinker
Paradox. I expect Russell Paradox becomes irrelevant.

[Mostowski Collapse]

It works both in FOL and FOL+SET, no Russell Paradox needed,
Dx stands for drinker (in any pub), Px stands for in da house
(in our pub). First FOL only:

∃xPx → ∃x(Px ∧ (Dx → ∀y(Py → Dy))) is valid.
https://www.umsu.de/trees/#~7xPx~5~7x%28Px~1%28Dx~5~6y%28Py~5Dy%29%29%29

And now FOL+SET, but no Subset Axiom or Russell Paradox
used, only Dx replaced by membership Exd and Px replaced
by membershipt Exp:

∃xExp → ∃x(Exp ∧ (Exd → ∀y(Eyp → Eyd))) is valid.
https://www.umsu.de/trees/#~7xExp~5~7x%28Exp~1%28Exd~5~6y%28Eyp~5Eyd%29%29%29

[Dan Christensen]

On Wednesday, October 12, 2022 at 6:27:05 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 13. Oktober 2022 um 00:26:20 UTC+2:
> > On Wednesday, October 12, 2022 at 6:16:02 PM UTC-4, Mostowski Collapse wrote:
> > > Well its wrong. The Drinker Paradox is only proving this:
> > >
> > > ∃x(Dx → ∀yDy) is valid.

> > Did you not say that this requires a non-empty domain of discussion? Such things do not exist in most math textbooks. Deal with it.

> You prove nonsense like:
> 5 EXIST(a):~a e drinkers
> Detach, 4, 2
> http://www.dcproof.com/DrinkersThm1.htm
>

It is a direct result of the non-existence of the universal set (see Russell). Deal with it, Jan Burse.

> Did he walk out of the pub? Can you also prove
> EXIST(a):[a e pub & ~a e drinkers] ?

Not required.

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

Again, there is no requirement that x be in the pub.