Smullyan's Proof of the Drinkers Principle V3

[Dan Christensen]

Revealed below are the full inner workings fo First Order Logic (FOL) as it pertains to Smullyan's Drinker Principle. Each quantifier is restricted by a unary predicate U implicit, though it is never formally specified in FOL proofs as it would be in DC Proof and most math textbooks. Here, we make the implicit explicit.

Following is my formal translation of Smullyan's informal proof of the Drinking Principle in the notation of DC Proof 2.0.

Smullyan writes:

"[T]here exists someone such that whenever he (or she) drinks, everybody drinks. It comes ultimately from the strange principle that a false proposition implies any proposition. [i.e. the principle of vacuous truth]

[Smullyan's informal proof:]

"Either it is true that everybody drinks or it isn't. Suppose it is true that everybody drinks. Then take any person-call him Jim. Since everybody drinks and Jim drinks, then it is true that if Jim drinks then everybody drinks. So there is at least one person namely Jim-such that if he drinks then everybody drinks.

"Suppose, however, that it is not true that everybody drinks; what then? Well, in that case there is at least one person-call him Jim-who doesn't drink. Since it is false that Jim drinks, then it is true that if Jim drinks,everybody drinks. So again there is a person--namely Jim--such that if he drinks, everybody drinks."

--"What is the name of this book?" pp. 209-210

****************************************************************************
Formal proof in the notation of DC Proof 2.0

Required to prove: EXIST(b):[U(b) & [Drinker(b) => ALL(a):[U(a) => Drinker(a)]]]

Assume a non-empty domain of discussion U

1. EXIST(a):U(a)
Axiom

"Either it is true that everybody drinks or it isn't."

2. ALL(a):[U(a) => Drinker(a)] | ~ALL(a):[U(a) => Drinker(a)]
Or Not

Case 1

"Suppose it is true that everybody drinks."

3. ALL(a):[U(a) => Drinker(a)]
Premise

"Then take any person-call him Jim."

Apply the existence of a non-empty domain of discussion

4. U(jim)
E Spec, 1

"Since everybody drinks and Jim drinks,[...]

5. U(jim) => Drinker(jim)
U Spec, 3

6. Drinker(jim)
Detach, 5, 4

"If Jim drinks then everybody drinks."

7. Drinker(jim)
Premise

8. ALL(a):[U(a) => Drinker(a)]
Copy, 3

9. Drinker(jim) => ALL(a):[U(a) => Drinker(a)]
Conclusion, 7

"So there is at least one person, namely Jim, such that if he drinks then everybody drinks."

10. U(jim) & [Drinker(jim) => ALL(a):[U(a) => Drinker(a)]]
Join, 4, 9

Case 1

As Required:

11. ALL(a):[U(a) => Drinker(a)]
=> EXIST(b):[U(b) & [Drinker(b) => ALL(a):[U(a) => Drinker(a)]]]
Conclusion, 3

Case 2

"Suppose, however, that it is not true that everybody drinks"

12. ~ALL(a):[U(a) => Drinker(a)]
Premise

13. ~~EXIST(a):~[U(a) => Drinker(a)]
Quant, 12

14. EXIST(a):~[U(a) => Drinker(a)]
Rem DNeg, 13

15. EXIST(a):~~[U(a) & ~Drinker(a)]
Imply-And, 14

16. EXIST(a):[U(a) & ~Drinker(a)]
Rem DNeg, 15

"Well, in that case there is at least one person, call him Jim, who doesn't drink."

17. U(jim) & ~Drinker(jim)
E Spec, 16

18. U(jim)
Split, 17

19. ~Drinker(jim)
Split, 17

"Since it is false that Jim drinks, then it is [vacuously] true that if Jim drinks, everybody drinks."

20. Drinker(jim)
Premise

21. ~Drinker(jim) => ALL(a):[U(a) => Drinker(a)]
Arb Cons, 20

Vacuously true:

22. ALL(a):[U(a) => Drinker(a)]
Detach, 21, 19

23. Drinker(jim) => ALL(a):[U(a) => Drinker(a)]
Conclusion, 20

24. U(jim)
& [Drinker(jim) => ALL(a):[U(a) => Drinker(a)]]
Join, 18, 23

Case 2

"So again there is a person, namely Jim, such that if he drinks, everybody drinks."

25. ~ALL(a):[U(a) => Drinker(a)]
=> EXIST(b):[U(b) & [Drinker(b) => ALL(a):[U(a) => Drinker(a)]]]
Conclusion, 12

Joining results for Cases Rule

26. [ALL(a):[U(a) => Drinker(a)]
=> EXIST(b):[U(b) & [Drinker(b) => ALL(a):[U(a) => Drinker(a)]]]]
& [~ALL(a):[U(a) => Drinker(a)]
=> EXIST(b):[U(b) & [Drinker(b) => ALL(a):[U(a) => Drinker(a)]]]]
Join, 11, 25

As Required:

By cases:

27. EXIST(b):[U(b) & [Drinker(b) => ALL(a):[U(a) => Drinker(a)]]]
Cases, 2, 26

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]

You did this already in 2014, with sets and not with predicates,
amazingly back then you had a version with case 1 and case 2 already:

Dan Christensen schrieb am Samstag, 24. Mai 2014 um 20:17:46 UTC+2:
> THEOREM (The Drinkers' Paradox) ('@' = epsilon, '|' = OR-operator)
> 27 ALL(p):ALL(d):[Set(p) & Set(d)
> => [EXIST(a):a @ p
> => EXIST(a):[a @ p & [a @ d => ALL(b):[b @ p => b @ d]]]]]
https://groups.google.com/g/sci.logic/c/0aXAP1wltew/m/W_MWAys434YJ

So it took you 8 years (EIGHT) to replace the sets by predicates?

LoL

P.S.: Works also in FOL, and you cannot omit the EXIST(a):U(a)

∃aUa → ∃b(Ub ∧ (Db → ∀a(Ua → Da))) is valid.
https://www.umsu.de/trees/#~7aUa~5~7b%28Ub~1%28Db~5~6a%28Ua~5Da%29%29%29

∃b(Ub ∧ (Db → ∀a(Ua → Da))) is invalid.
https://www.umsu.de/trees/#~7b%28Ub~1%28Db~5~6a%28Ua~5Da%29%29%29

Dan Christensen schrieb am Montag, 14. November 2022 um 20:45:16 UTC+1:
> 1. EXIST(a):U(a)
> Axiom

[Mostowski Collapse]

It took you 8 (EiGHT) years to comprehend the
proposal back then from Peter Percival?

Peter Percival schrieb am Donnerstag, 29. Mai 2014 um 18:10:13 UTC+2:
> (Ex)(X(x) & (D(x) -> (Uy)(X(y) -> D(y)))).
> Still only two quantifiers, and now just two predicates.
https://groups.google.com/g/sci.logic/c/0aXAP1wltew/m/658v-m0UebAJ

What did you do? What took you so long?
Did you first marry, have child, build a house,

and then return to logic?

[Dan Christensen]

On Monday, November 14, 2022 at 3:21:18 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 14. November 2022 um 20:45:16 UTC+1:
> > 1. EXIST(a):U(a)
> > Axiom
> > 27. EXIST(b):[U(b) & [Drinker(b) => ALL(a):[U(a) => Drinker(a)]]]
> > Cases, 2, 26

> You did this already in 2014, with sets and not with predicates,
> amazingly back then you had a version with case 1 and case 2 already:
>
> Dan Christensen schrieb am Samstag, 24. Mai 2014 um 20:17:46 UTC+2:
> > THEOREM (The Drinkers' Paradox) ('@' = epsilon, '|' = OR-operator)
> > 27 ALL(p):ALL(d):[Set(p) & Set(d)
> > => [EXIST(a):a @ p
> > => EXIST(a):[a @ p & [a @ d => ALL(b):[b @ p => b @ d]]]]]
> https://groups.google.com/g/sci.logic/c/0aXAP1wltew/m/W_MWAys434YJ
>
> So it took you 8 years (EIGHT) to replace the sets by predicates?
>

Nothing is "replaced", Jan Burse. I recently attached an FOL-like proof of Smullyan's proof to my original math blog posting as a historical footnote. The version posted here should make clear why standard FOL is not found in most textbook proofs in mathematics. Too much is hidden behind the "wizard's curtain" with those mysterious, unspecified domains of yours.

[Mostowski Collapse]

The problem is you still don't understand FOL. Mathematicians
do heavily use FOL for the following reason:

a) If a mathematician wants to produce a general result,
he/she can use predicates aka classes. They are more
general than sets:

a.1) For example there is a universal predicate "V", which
can be defined as ALL(x):V(x), which is not possible for a set,
leads to an antinomy.
https://mathworld.wolfram.com/RussellsAntinomy.html

a.2) You find many mathematics books where the author
uses a particular language, where he sometimes talks about
a set and sometimes about a class, for example "On", the
ordinal numbers, is a class respectively predicate, assuming
"On" a set would lead again to an antinomy.
https://archive-ouverte.unige.ch/unige:113777

a.3) The Drinker paradox is no exception, in its general form
it would have a predicate D (or Drinker), and not some set. The
struggle is seen that sets even lead to an abnormal solution
of the Drinker Paradox, for example what Dan Christensen published
when he married the Drinker Paradox with the Russell Paradox.

When you have a genral result for predicates aka classes,
you can still specialize it to sets. At least this is allowed for
FOL theorems since there is a so called transfer theorem.

Its relatively easy, if you have a theorem A(P1,..,Pn) using
predicates P1 ... Pn, which is provable, the transfer lemma says
that a rewritten theorem A'(p1,..,pn) where p1 .. pn are sets

does also hold. The converse direction doesn't hold,
when using some set theory to obtain A'(p1,..,pn):

/* Transfer Theorem */
|- A(P1,...,Pn) => |- A'(p1,..,pn)

/* There are Counter Examples */
SET |- A'(p1,..,pn) =/=> |- A(P1,...,Pn)

Proof =>: Replace every predicate Pj respective class, by
the class builder { x | x e pj }. In particular one will be
allowed to simplify Pj(t) to t e pj.

So you didn't FOL-ify something. You found the more
general solution to the Drinker Paradox. Here is a book
to plough, the transfer theorem should be also mentioned:

Basic Set Theory (Dover Books on Mathematics)
Azriel Levy (Author) - 1971
https://www.amazon.com/dp/0486420795

[Dan Christensen]

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

Dan

On Monday, November 14, 2022 at 6:56:49 PM UTC-5, Mostowski Collapse wrote:
> The problem is you still don't understand FOL. Mathematicians
> do heavily use FOL for the following reason:
>
> a) If a mathematician wants to produce a general result,
> he/she can use predicates aka classes. They are more
> general than sets:
>

[snip]

[Mostowski Collapse]

Thats the problem with you Wonky Man, you don't understand
FOL. This here is consistent (V the universal predicate):

ALL(z):V(z)

If you add such an axiom, and if V is a fresh predicate symbol,
there is no inconsistency.

So you can prove:

ALL(z):V(z) => ALL(x):[V(x) => EXIST(y):[V(y) => f(x)=y]]

∀zVz → ∀x(Vx → ∃y(Vy ∧ f(x)=y)) is valid.
https://www.umsu.de/trees/#~6zVz~5~6x%28Vx~5~7y%28Vy~1f%28x%29=y%29%29

Or omitting V like one would omit the pub in the Drinker paradox:

∀x∃yf(x)=y is valid.
https://www.umsu.de/trees/#~6x~7yf%28x%29=y

So FOL is able to express very general concepts, via
predicates. And the function symbols are also very
general, they map from the universe of discourse to

the universe of discourse. Which you seem to have barred
from DC Proof. This is because DC Proof abuses FOL function
symbols. It is neither fish nor fowl, the DC Proof function

symbols are utter nonsense. One can even not prove:

~f=g => ~dom(f)=dom(g) v EXIST(x):[x e dom(f) & ~f(x)=g(x)]

The above would be possible if f and g were set-like.

[Mostowski Collapse]

This is obviously a whole lot of a difference:

Dan Christensen schrieb am Dienstag, 15. November 2022 um 05:10:11 UTC+1:
> Using DC Proof set theory (the Subset Axiom), you can prove:
> ALL(drinkers):[Set(drinkers) => EXIST(a):[a in drinkers => ALL(b):[b in drinkers]]]
> Using DC Proof predicate logic to simulate standard FOL, you can prove:
> EXIST(a):U(a) => EXIST(a):[U(a) & [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]

For every body knowning that sets and predicates are
not the same, it is obvious that they do not express the
same thing, and that there is some difference.

But for an idiot like Dan Christensen, who has absolutely
no clue that there is a difference between:
- Predicates and set are not the same
- Function symbols and sets of pairs are not same

This is of course a big hurdle. Thats why he comes up
with all kind of silly claims what mathematicians do and
not do, and with silly ideas that this here could be wrong:

∀a∃bf(a)=b is valid.
https://www.umsu.de/trees/#~6a~7b(f(a)=b)

Why should it be wrong? A FOL function symbol BY ITS VERY
DEFINITION maps the domain of discourse to the domain of
discourse. This is widely documented, you also find it on Wikipedia:

- A domain of discourse D, usually required to be non-empty (see below).
- For every n-ary function symbol, an n-ary function from D to D
as its interpretation (that is, a function D^n → D).
https://en.wikipedia.org/wiki/Interpretation_%28logic%29#Interpretations_of_a_first-order_language

Whats wrong with you? Maybe see a doctor.

[Mostowski Collapse]

Holy cow, your analphabetism is quite severe. Never

seen a book from the inside. Look what Wikipedia writes:

"A domain of discourse D, usually required to be non-empty (see below).
- For every n-ary function symbol, an n-ary function from D to D
as its interpretation (that is, a function D^n → D)."
https://en.wikipedia.org/wiki/Interpretation_%28logic%29#Interpretations_of_a_first-order_language

Now how do you prove ∀x∃yf(x)=y in FOL. Can
you explain the proof? Well its not a FOL proof,
its a FOL=, i.e. FOL plus equality proof.

There are two variants of FOL:
- FOL without equality
- FOL with equality (needs more axioms and inference rules)

Can you explain the proof of ∀x∃yf(x)=y ?

P.S.: Here you see in the release notes that
Wolfgang Schwarz tree tool supports FOL=
since, not so long .

https://github.com/wo/tpg/commits/master

[Dan Christensen]

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

Dan

On Wednesday, November 16, 2022 at 3:39:28 PM UTC-5, Mostowski Collapse wrote:

[snip childish abuse]

> Look what Wikipedia writes:
>
> "A domain of discourse D, usually required to be non-empty (see below).
> - For every n-ary function symbol, an n-ary function from D to D
> as its interpretation (that is, a function D^n → D)."
> https://en.wikipedia.org/wiki/Interpretation_%28logic%29#Interpretations_of_a_first-order_language
> Now how do you prove ∀x∃yf(x)=y in FOL. Can
> you explain the proof? Well its not a FOL proof,

[snip]

[Mostowski Collapse]

When you learned logic reading air freshner in the toilet...
Anyway, who asked about ∃xDx -> ∀yDy as the Drinker Paradox,

a raccoon?

LoL

BTW: This here needs no domain D(x), D(y), D(z). The domain
is the domain of discourse, which doesn't need any predicate.

Assume that we have ∀x∃!y F(x,y),
Then these two are logically equivalent:

2) ∃z(F(x,z) & F(z,y))

3) ∀z(F(x,z) => F(z,y))

Even the tree tool can show that 2) and 3) are equivalent:

(∀x∃yFxy ∧ ∀x∀y∀z((Fxy ∧ Fxz) → y=z)) → ∀x∀y(∃z(Fxz ∧ Fzy) ↔ ∀z(Fxz → Fzy)) is valid.
https://www.umsu.de/trees/#~6x~7yF%28x,y%29~1~6x~6y~6z%28F%28x,y%29~1F%28x,z%29~5y=z%29~5~6x~6y%28~7z%28F%28x,z%29~1F%28z,y%29%29~4~6z%28F%28x,z%29~5F%28z,y%29%29%29

Can your raccoon show the same in DC Proof?

[Ross A. Finlayson]

Dig two holes.

Aw, snap.

[Dan Christensen]

On Monday, November 14, 2022 at 2:45:16 PM UTC-5, Dan Christensen wrote:

[snip]

>
> Smullyan writes:
>
> "[T]here exists someone such that whenever he (or she) drinks, everybody drinks.

[snip]

Here, I proved using only predicate logic that:

EXIST(a):[U(a) & [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]

Where the predicate U makes explicit the FOL non-empty domain of discourse.

https://dcproof.com/SmullyansDrinkerPrinciple.htm (28 lines)

More succinctly and more elegantly, however, would be:

EXIST(a):~Drinker(a) => EXIST(a):[Drinker(a) => ALL(b):Drinker(b)]

PROOF:

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

2. ~Drinker(x)
E Spec, 1

3. ~Drinker(x) | ALL(b):Drinker(b)
Arb Or, 2

4. ~~Drinker(x) => ALL(b):Drinker(b)
Imply-Or, 3

5. Drinker(x) => ALL(b):Drinker(b)
Rem DNeg, 4

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

Only 6 lines! And no proofs by cases. And no need for any FOL-like domain of discourse U.

But wait! We assumed (line 1) that there exists at least one non-drinker. And yet, in the conclusion we have: ALL(b):Drinker(b).

A contradiction? And inconsistency in DC Proof??? Nope. (Sorry, Jan Burse.)

On line 3, we introduced ALL(b):Drinker(b), but we could as easily have introduced its negation ~ALL(b):Drinker(b). The the conclusion would then have been:

EXIST(a):~Drinker(a) => EXIST(a):[Drinker(a) => ~ALL(b):Drinker(b)]

We could also have introduced a arbitrary proposition Q, be it true or false. Then the conclusion would be:

EXIST(a):~Drinker(a) => EXIST(a):[Drinker(a) => Q]

1. EXIST(a):~Drinker(a) <---- not every thing or person is a drinker (makes sense!)
Premise

2. ~Drinker(x)
E Spec, 1

3. ~Drinker(x) | Q <---- Introduces arbitrary proposition Q
Arb Or, 2

4. ~~Drinker(x) => Q
Imply-Or, 3

5. Drinker(x) => Q
Rem DNeg, 4

6. EXIST(a):~Drinker(a) => EXIST(a):[Drinker(a) => Q]
Conclusion, 1

How cool is that?

[Mostowski Collapse]

There is no such assumption EXIST(a):~D(a)
in Smullyans Drinker Paradox. You are confused.

Do you mean:

EXIST(a):U(a)

Non empty domain of discourse? You derived
EXIST(a):~D(a) from your Russell nonsense.

But its nowhere stated in Smullyans Drinker Paradox.

[Mostowski Collapse]

Your axiom violates EXIST(a):~D(a) what Smullyan assumes
as the Universe of Discourse. Universe of Discourse = The
Pub and the Drinkers. How many people are in the pub?

How many people are drinkers?

If pub = {jack,jill,jeff}, drinkers={}, this is some world.
Call it world 1.

If pub = {jack,jill}, drinkers={jack,jill}, this is some other world.
Call it world 2.

Note world 2 violates this axiom EXIST(a):~D(a),
so I guess you didn't do the modelling right.
On the other hand both world 1 and world 2

satisfy on the other hand:

EXIST(a):[D(a) => ALL(b):D(b)],

if the quantifiers range over the pub people. So the
therem is not wrong. But your axiom is utter nonsense.

[Mostowski Collapse]

Corr.: Word order
Your axiom EXIST(a):~D(a) violates what Smullyan assumes

as the Universe of Discourse. Universe of Discourse = The

[Dan Christensen]

On Saturday, February 4, 2023 at 10:06:49 AM UTC-5, Mostowski Collapse wrote:
> There is no such assumption EXIST(a):~D(a)
> in Smullyans Drinker Paradox.

[snip]

Here is my formal proof of Smullyan's original version of DP: http://dcproof.com/SmullyansDrinkerPrinciple.htm (only 28 lines)

Enjoy.

[Mostowski Collapse]

I am impressed, ChatGPT can paraphrase the two cases:

(ChatGPT Jan 30 Version. Free Research Preview.)

A: I apologize for the mistake in my previous answers. You are correct,
if "a" represents a non-drinker, then the antecedent D(a) of the implication
would be false, and the formula EXIST(a):[D(a) => ALL(b):D(b)] would be
vacuously true, meaning that the conclusion follows by default.

Q: And what is the other scenario?

A: The other scenario would be if all guests in the bar are drinking. In
this case, "a" would represent a drinker, and the antecedent D(a) of the
implication would be true. The conclusion ALL(b):D(b) would also be true,
as all guests are drinking. Therefore, the formula EXIST(a):[D(a) => ALL(b):D(b)]
would be true in this scenario.

ChatGPT being more smart than Dan-O-Matik. But I helped
it a little bit, injecting the non-empty domain assumption
into the interaction, thats why the interaction started running

along if "a" would be bla bka.

[Mostowski Collapse]

Come on Dan-O-Matik, you can do bettern than this:

28 EXIST(a):U(a) => EXIST(a):[U(a) & [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]
4 Conclusion, 1
http://dcproof.com/SmullyansDrinkerPrinciple.htm

I got this, formula is shorter, proof can be possibly
shortened a little bit:

35 EXIST(a):U(a) => EXIST(a):[D(a) => ALL(b):D(b)]
Conclusion, 1

So what are the possible worlds?

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

1 EXIST(a):U(a)
Premise

2 ALL(c):D(c)
Premise

3 ~EXIST(a):[D(a) => ALL(b):D(b)]
Premise

4 ~~ALL(a):~[D(a) => ALL(b):D(b)]
Quant, 3

5 ALL(a):~[D(a) => ALL(b):D(b)]
Rem DNeg, 4

6 U(u)
E Spec, 1

7 ~[D(u) => ALL(b):D(b)]
U Spec, 5

8 ~~[D(u) & ~ALL(b):D(b)]
Imply-And, 7

9 D(u) & ~ALL(b):D(b)
Rem DNeg, 8

10 D(u)
Split, 9

11 ~ALL(b):D(b)
Split, 9

12 ALL(c):D(c) & ~ALL(b):D(b)
Join, 2, 11

13 ~~EXIST(a):[D(a) => ALL(b):D(b)]
Conclusion, 3

14 EXIST(a):[D(a) => ALL(b):D(b)]
Rem DNeg, 13

15 ALL(c):D(c) => EXIST(a):[D(a) => ALL(b):D(b)]
Conclusion, 2

16 ~ALL(c):D(c)
Premise

17 ~EXIST(a):[D(a) => ALL(b):D(b)]
Premise

18 ~~ALL(a):~[D(a) => ALL(b):D(b)]
Quant, 17

19 ALL(a):~[D(a) => ALL(b):D(b)]
Rem DNeg, 18

20 ~~EXIST(c):~D(c)
Quant, 16

21 EXIST(c):~D(c)
Rem DNeg, 20

22 ~D(u)
E Spec, 21

23 ~[D(u) => ALL(b):D(b)]
U Spec, 19

24 ~~[D(u) & ~ALL(b):D(b)]
Imply-And, 23

25 D(u) & ~ALL(b):D(b)
Rem DNeg, 24

26 D(u)
Split, 25

27 ~ALL(b):D(b)
Split, 25

28 ~D(u) & D(u)
Join, 22, 26

29 ~~EXIST(a):[D(a) => ALL(b):D(b)]
Conclusion, 17

30 EXIST(a):[D(a) => ALL(b):D(b)]
Rem DNeg, 29

31 ~ALL(c):D(c) => EXIST(a):[D(a) => ALL(b):D(b)]
Conclusion, 16

32 ALL(c):D(c) | ~ALL(c):D(c)
Or Not

33 [ALL(c):D(c) => EXIST(a):[D(a) => ALL(b):D(b)]]
& [~ALL(c):D(c) => EXIST(a):[D(a) => ALL(b):D(b)]]
Join, 15, 31

34 EXIST(a):[D(a) => ALL(b):D(b)]
Cases, 32, 33

35 EXIST(a):U(a) => EXIST(a):[D(a) => ALL(b):D(b)]
Conclusion, 1

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

[Dan Christensen]

On Saturday, February 4, 2023 at 2:27:05 PM UTC-5, Mostowski Collapse wrote:
> Come on Dan-O-Matik, you can do bettern than this:
>
> 28 EXIST(a):U(a) => EXIST(a):[U(a) & [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]
> 4 Conclusion, 1
> http://dcproof.com/SmullyansDrinkerPrinciple.htm
>

I was translating Mullyans proof as closely as possible.

> I got this, formula is shorter, proof can be possibly
> shortened a little bit:
>
> 35 EXIST(a):U(a) => EXIST(a):[D(a) => ALL(b):D(b)]
> Conclusion, 1
>
> So what are the possible worlds?
>

[snip]

"Possible worlds???" You can't be serious.

Anyway, here is a modification of your proof. What do you think?

Suppose we have predicates D and P such that
D(x) = x is a drinker
P(x) = x is in the pub

1. ALL(a):[D(a) => P(a)] & EXIST(a):[~D(a) & P(a)]
Premise

2. EXIST(a):[~D(a) & P(a)]
Split, 1

3. ~D(x) & P(x)
E Spec, 2

4. ~D(x)
Split, 3

5. D(x)
Premise

6. ~D(x) => P(x) & ALL(b):[P(b) => D(b)]
Arb Cons, 5

7. P(x) & ALL(b):[P(b) => D(b)]
Detach, 6, 4

Vacuously true:

8. D(x) => P(x) & ALL(b):[P(b) => D(b)]
Conclusion, 5

9. EXIST(a):[D(a) => P(a) & ALL(b):[P(b) => D(b)]]
E Gen, 8

10. ALL(a):[D(a) => P(a)] & EXIST(a):[~D(a) & P(a)]
=> EXIST(a):[D(a) => P(a) & ALL(b):[P(b) => D(b)]]
Conclusion, 1

While that may seem outrageous at first glance, we have, equivalently...

11. ALL(a):[D(a) => P(a)] & EXIST(a):[~D(a) & P(a)]
=> EXIST(a):[~D(a) | P(a) & ALL(b):[P(b) => D(b)]]
Imply-Or, 10

Not even interesting now! After all, it was assumed from the beginning that there existed a non-drinker in the pub.

[Mostowski Collapse]

How got the below version lost, and supplanted by this nonsense:

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

Dan Christensen schrieb am Montag, 14. November 2022 um 20:51:18 UTC+1:
> 1. EXIST(a):U(a)
> Axiom

[Mostowski Collapse]

Now prove the other direction from 27 to 1. Can you do that
in DC Poop? Wikipedia tells me the other direction does also hold:

https://en.wikipedia.org/wiki/Drinker_paradox#Non-empty_domain

[Mostowski Collapse]

Well its a theorem:

Theorem 1: The Drinker Paradox
∃xPx entails ∃x(Px ∧ (Dx → ∀y(Py → Dy))).
https://www.umsu.de/trees/#~7xPx|=~7x(Px~1(Dx~5~6y(Py~5Dy)))

Theorem 2: The Drinker Paradox Reverse Direction2
∃x(Px ∧ (Dx → ∀y(Py → Dy))) entails ∃xPx.
https://www.umsu.de/trees/#~7x(Px~1(Dx~5~6y(Py~5Dy)))|=~7xPx

So you can. The reverse direction is also mentioned on Wikipedia:
https://en.wikipedia.org/wiki/Drinker_paradox#Non-empty_domain

Can you do the reverse direction in DC Poop?

[Mostowski Collapse]

Or in mathematical words:

Non-empty domain condition is not only sufficient,
but also necessary for the Drinker Paradox.

https://www.math3ma.com/blog/necessary-versus-sufficient

[Dan Christensen]

On Sunday, April 30, 2023 at 10:45:43 AM UTC-4, Mostowski Collapse wrote:
> Or in mathematical words:
>
> Non-empty domain condition is not only sufficient,
> but also necessary for the Drinker Paradox.
>

Wrong again, Mr. Collapse. Not if you use a set-theoretic model. Then you make use of fact that every set x excludes something (see Russell's Paradox). Then you can obtain:

EXIST(a):[ a in x => Q]

for ANY proposition Q, be it true or false. For DP, you have x = the set of drinkers and Q = ALL(b):[b in drinkers].

You can use a variation of this technique in predicate logic to obtain:

EXIST(a):~X(a) => EXIST(a) [X(a) => Q]

[Mostowski Collapse]

Well it shows that the you alleged "set -theoretic model" of the
Drinker Paradox is nothing else than utter bull shit. Why should
this be always true, if the pub can be empty?

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

The problem is you forgot one quantified group reference,
there is only one "pub" mention in your nonsense:

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

Nothing to do with set -theoretic model". Its another
error in modelling the Drinker Paradox. You can count yourself,
how many quantified group references are here and
how many "pub" mention you would need:

"As a running example in this paper, we will use the
so-called drinker’s principle. This says that in every group
of people one can point to one person in the group such that
if that person drinks then all the people in the group drink."
https://www.cs.ru.nl/~freek/mizar/miz.pdf

Quantified group reference 1:
"can point to one person in the group"
Quantified group reference 2:
"all the people in the group"

So "pub" needs to appear twice in a Drinker Paradox formula.

[Dan Christensen]

On Sunday, April 30, 2023 at 1:50:17 PM UTC-4, Mostowski Collapse wrote:
> Well it shows that the you alleged "set -theoretic model" of the
> Drinker Paradox is nothing else than utter bull shit. Why should
> this be always true, if the pub can be empty?
>

Do pay attention, Mr. Collapse. We have EXIST(a):[a in D => Q] for ANY set D (be it empty or not) and proposition Q (be it true or not). For a formal proof, scroll up. And do get a life!

[Mostowski Collapse]

We also don't have this here in the Drinker Paradox,
where D would mean drinking:

EXIST(x in D => Q)

You still don't get it, whats your blooper? Where
is the "pub", the part. Tell us Dan-O-Matik where
is the "pub" from:

"can point to one person in the group"

In your formula (Hint "can point" = "exist"):

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

Just read Freek Wiedijk spec of the Drinker Principle:

"As a running example in this paper, we will use the
so-called drinker’s principle. This says that in every group
of people one can point to one person in the group such that
if that person drinks then all the people in the group drink."
https://www.cs.ru.nl/~freek/mizar/miz.pdf

Dan Christensen schrieb:

[Dan Christensen]

See my reply just now to your identical posting elsewhere.

Dan

On Sunday, April 30, 2023 at 4:16:32 PM UTC-4, Mostowski Collapse wrote:
> We also don't have this here in the Drinker Paradox,
> where D would mean drinking:
>
> EXIST(x in D => Q)
>
> You still don't get it, whats your blooper? Where
> is the "pub", the part. Tell us Dan-O-Matik where
> is the "pub" from:
> "can point to one person in the group"

[snip]

[Jeff Barnett]

On 4/30/2023 1:35 PM, Dan Christensen wrote:
> On Sunday, April 30, 2023 at 1:50:17 PM UTC-4, Mostowski Collapse wrote:
>> Well it shows that the you alleged "set -theoretic model" of the
>> Drinker Paradox is nothing else than utter bull shit. Why should
>> this be always true, if the pub can be empty?
>>
>
> Do pay attention, Mr. Collapse. We have EXIST(a):[a in D => Q] for ANY set D (be it empty or not) and proposition Q (be it true or not). For a formal proof, scroll up. And do get a life!

Did you mean the similar looking EXIST(a):[a IN d] => Q ?
--
Jeff Barnett

[Dan Christensen]

No, I meant EXIST(a):[[a IN d] => Q]

Yes, it is somewhat "pathological." Usually you wouldn't put an existential quantifier on a conditional. Part of my motivation is to show why you might want to avoid such constructs. At the very least, "alarm bells" should go off when you come across them.

[Mostowski Collapse]

Its not part of the Drinker Paradox if you start using "pub" like here:

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

You have pub in the ALL. But you don't have pub the EXIST.
So the above formula is not the drinker paradox.

Thats not what is required by the drinker paradox, your
fomula in DrinkersThm1. Its just nonsense. If it were the

Drinker Paradox, you could prove:

EXIST(z):[z e pub] <=>

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

Just like Wikipedia does for their formula. But you
cannot do it with your formula, since it is not the Drinker paradox.

[Mostowski Collapse]

Thats possibly the reason why they kicked you out
of Wikipedia, when you wrote nonsense like:

> Why was my edit removed?
> possibly empty set P <<< nonsense
> -Danchristensen (talk) 12:43, 7 August 2015 (UTC)
https://en.wikipedia.org/wiki/Talk:Drinker_paradox#Why_was_my_edit_removed?

As every body knows non empty set P is not
only sufficient but also necessary condition for
the Drinker Paradox.

if and only if it is non-empty.
https://en.wikipedia.org/wiki/Drinker_paradox#Non-empty_domain

Again, what you prove and try to promote as
the Drinker Paradox, is not the Drinker Paradox.
Just only Vacuous Truth nonsense, from

some Russell nonsens. Further you have no clue
what sufficient vs necessary condition means:
https://www.math3ma.com/blog/necessary-versus-sufficient

[Dan Christensen]

On Sunday, April 30, 2023 at 8:21:37 PM UTC-4, Mostowski Collapse wrote:

> Its not part of the Drinker Paradox if you start using "pub" like here:
>
> As Required:
> 10 EXIST(x):[x e drinkers => ALL(y):[y e pub => y e drinkers]]

As you must know by, the consequent could be any proposition whatsoever. It may or may not refer to any pubs. It could even be ~x e drinkers.

> http://www.dcproof.com/DrinkersThm1.htm
>
> You have pub in the ALL. But you don't have pub the EXIST.
> So the above formula is not the drinker paradox.
>
> Thats not what is required by the drinker paradox, your
> fomula in DrinkersThm1. Its just nonsense. If it were the
>
> Drinker Paradox, you could prove:
>
> EXIST(z):[z e pub] <=>
> EXIST(x):[x e drinkers => ALL(y):[y e pub => y e drinkers]]

Since this is a set-theoretic model, you don't need a non-empty pub to prove EXIST(x):[x e drinkers => ALL(y):[y e pub => y e drinkers]]

Here the Q is simply ALL(y):[y e pub => y e drinkers].

But it could as easily have been the negation ~ALL(y):[y e pub => y e drinkers]

That's what is so "pathalogical" about this construct.

It that beginning to sink in yet, Mr. Collapse????

[Mostowski Collapse]

Where is your "jim"? Your combined formula is
utter nonsense. How do you want satisfy:

"As a running example in this paper, we will use the
so-called drinker’s principle. This says that in every group
of people one can point to one person in the group such that
if that person drinks then all the people in the group drink."
https://www.cs.ru.nl/~freek/mizar/miz.pdf

i.e. how do you want to satisfy "one can point to
one person in the group [the pub]"?

Can you tell us where is "jim" in your formula.

> As Required:
> 10 EXIST(x):[x e drinkers => ALL(y):[y e pub => y e drinkers]]

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

Basically because you use Russell, you operate
with "jim" that isn't a drinker, i.e. some x with
~x e drinker. But you forgezt that the Driner Paradox

nevertheless requires x e pub. Whats wrong with you?

[Mostowski Collapse]

Here an enhanced version of Freek Wiedijk very
precise phrasing, which is still not precise enough for
our dumbo Dan Christensen:

"As a running example in this paper, we will use the
so-called drinker’s principle. This says that in every group

of people one can point to one person [jim] in the
group [the pub] such that if that person drinks then all

the people in the group drink."
https://www.cs.ru.nl/~freek/mizar/miz.pdf

I inserted [jim] and [the pub]. Do you get the
Drinker Paradox now dumbo?

[Dan Christensen]

On Monday, May 1, 2023 at 5:15:13 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 1. Mai 2023 um 02:46:49 UTC+2:
> > On Sunday, April 30, 2023 at 8:21:37 PM UTC-4, Mostowski Collapse wrote:
> >
> > > Its not part of the Drinker Paradox if you start using "pub" like here:
> > >
> > > As Required:
> > > 10 EXIST(x):[x e drinkers => ALL(y):[y e pub => y e drinkers]]
> > As you must know by, the consequent could be any proposition whatsoever. It may or may not refer to any pubs. It could even be ~x e drinkers.
> > > http://www.dcproof.com/DrinkersThm1.htm
> > >
> > > You have pub in the ALL. But you don't have pub the EXIST.
> > > So the above formula is not the drinker paradox.
> > >
> > > Thats not what is required by the drinker paradox, your
> > > fomula in DrinkersThm1. Its just nonsense. If it were the
> > >
> > > Drinker Paradox, you could prove:
> > >
> > > EXIST(z):[z e pub] <=>
> > > EXIST(x):[x e drinkers => ALL(y):[y e pub => y e drinkers]]
> > Since this is a set-theoretic model, you don't need a non-empty pub to prove EXIST(x):[x e drinkers => ALL(y):[y e pub => y e drinkers]]
> >
> > Here the Q is simply ALL(y):[y e pub => y e drinkers].
> >
> > But it could as easily have been the negation ~ALL(y):[y e pub => y e drinkers]
> >
> > That's what is so "pathalogical" about this construct.
> >

> Where is your "jim"?

[snip]

It is introduced on line 4 in https://dcproof.com/SmullyansDrinkerPrinciple.htm

> How do you want satisfy:
> "As a running example in this paper, we will use the
> so-called drinker’s principle. This says that in every group
> of people one can point to one person in the group such that
> if that person drinks then all the people in the group drink."
> https://www.cs.ru.nl/~freek/mizar/miz.pdf

It seems different authors have different versions of DP. In my formalization (link above) Smullyan's original informal proof, he sets out to prove:

"There exists someone such that whenever he (or she) drinks, everybody drinks." (p.210 on his book)

No mention of any groups or pubs. In your "standard" FOL, the end result would be simply Ex[Dx => Ay D(y)].

In DC Proof, with the domain of discourse U made explicit on line 1, the end result is:

EXIST(a):U(a) => EXIST(a):[U(a) & [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]

[Mostowski Collapse]

A little bit unreflected is your claim that the Russell Paradox would
be key in your blog. Whats your proof of its necessity? Since this is
provable in FOL, without Russell Paradox or Subset Axiom:

Ex[Dx => Ay D(y)]

You can apply two principles:
a) Weakening principle, from Ay D(y) we can infer Ay (P(y) => D(y))
b) Transfer principle, if its valid for Predicates its also valid for Sets.

Judging from a) and b) it should be evident that your bullshit formula
is also provable without Russell Paradox or Subset Axiom. And
this is indeed the case, here is a DC Proof proof:

23 ~ALL(x):~[x ε drinkers => ALL(a):[a ε pub => a ε drinkers]]
Conclusion, 3

----------------------------------- cut here --------------------------------------------

1 Set(pub)
Axiom

2 Set(drinkers)
Axiom

3 ALL(x):~[x ε drinkers => ALL(a):[a ε pub => a ε drinkers]]
Premise

4 pub ε drinkers
Premise

5 v ε pub
Premise

6 ~v ε drinkers
Premise

7 ~[v ε drinkers => ALL(a):[a ε pub => a ε drinkers]]
U Spec, 3

8 v ε drinkers
Premise

9 u ε pub
Premise

10 ~u ε drinkers
Premise

11 ~v ε drinkers & v ε drinkers
Join, 6, 8

12 ~~u ε drinkers
Conclusion, 10

13 u ε drinkers
Rem DNeg, 12

14 ALL(a):[a ε pub => a ε drinkers]
Conclusion, 9

15 v ε drinkers => ALL(a):[a ε pub => a ε drinkers]
Conclusion, 8

16 ~[v ε drinkers => ALL(a):[a ε pub => a ε drinkers]]
& [v ε drinkers => ALL(a):[a ε pub => a ε drinkers]]
Join, 7, 15

17 ~~v ε drinkers
Conclusion, 6

18 v ε drinkers
Rem DNeg, 17

19 ALL(a):[a ε pub => a ε drinkers]
Conclusion, 5

20 pub ε drinkers => ALL(a):[a ε pub => a ε drinkers]
Conclusion, 4

21 ~[pub ε drinkers => ALL(a):[a ε pub => a ε drinkers]]
U Spec, 3

22 [pub ε drinkers => ALL(a):[a ε pub => a ε drinkers]]
& ~[pub ε drinkers => ALL(a):[a ε pub => a ε drinkers]]
Join, 20, 21

23 ~ALL(x):~[x ε drinkers => ALL(a):[a ε pub => a ε drinkers]]
Conclusion, 3

[Dan Christensen]

See my reply just now to your identical posting here.

Dan

On Monday, May 1, 2023 at 8:00:42 PM UTC-4, Mostowski Collapse wrote:
> A little bit unreflected is your claim that the Russell Paradox would
> be key in your blog. Whats your proof of its necessity? Since this is
> provable in FOL, without Russell Paradox or Subset Axiom:
> Ex[Dx => Ay D(y)]
> You can apply two principles:
> a) Weakening principle, from Ay D(y) we can infer Ay (P(y) => D(y))
> b) Transfer principle, if its valid for Predicates its also valid for Sets.
>
> Judging from a) and b) it should be evident that your bullshit formula
> is also provable without Russell Paradox or Subset Axiom. And
> this is indeed the case, here is a DC Proof proof:
>
> 23 ~ALL(x):~[x ε drinkers => ALL(a):[a ε pub => a ε drinkers]]
> Conclusion, 3
>
> ----------------------------------- cut here --------------------------------------------
>
> 1 Set(pub)
> Axiom
>
> 2 Set(drinkers)
> Axiom
>
> 3 ALL(x):~[x ε drinkers => ALL(a):[a ε pub => a ε drinkers]]
> Premise
>
> 4 pub ε drinkers
> Premise
>

[snip]

[Mostowski Collapse]

Would it be possibly to automatically generate a DC
Proof *.proof file? Is the format documented somewhere?
Now I added existential quantifier to my automated theorem

prover, which is not a proof writing system, but a proof
search system. It only writes a proof, to show what the
proof search found. The proof doesn't look much different

with the sugar coating of existential quantifier:

?- gentzen(∃x:(d(x) ⊃ ∀y:d(y)), N), !.
https://www.dogelog.ch/littab/doclet/docs/05_supplement/07_unicorn/example54/package.html

17 ∃x:(d(x) ⊃ ∀y:d(y))
▶ Conclusion 1,16

And the same proof more or less in DC Proof:

25 EXIST(x):[x ε d => ALL(y):y ε d]
Rem DNeg, 24

Still no Russell Paradox or Subset Axiom!

Ha Ha, Smullyan inspired me to give a name to my automated
theorem prover, it shall be "What is the Name of this Prover".
In analog to "What is the Name of this Book".

---- begin "What is the Name of this Prover" proof ---

1 ∀x: ¬ (d(x) ⊃ ∀y:d(y))
Premise

2 ¬ (d(_33664) ⊃ ∀y:d(y))
U Spec 1

3 d(_33664)
Premise

4 ¬d(v)
Premise

5 ¬ (d(v) ⊃ ∀y:d(y))
U Spec 1

6 d(v)
Premise

9 d(u)
▶ Reductio 7,8

10 ∀y:d(y)
U Gen 9

11 d(v) ⊃ ∀y:d(y)
▲ Conclusion 6,10

12 ⊥
Detach 5,11

13 d(v)
▲ Reductio 4,12

14 ∀y:d(y)
U Gen 13

15 d(_33664) ⊃ ∀y:d(y)
▲ Conclusion 3,14

16 ⊥
Detach 2,15

17 ∃x:(d(x) ⊃ ∀y:d(y))
▲ Conclusion 1,16

---- end "What is the Name of this Prover" proof ---

---------------- begin DC Proof proof -------------

1 Set(d)
Axiom

2 ALL(x):~[x ε d => ALL(y):y ε d]
Premise

3 d ε d
Premise

4 ~v ε d
Premise

5 ~[v ε d => ALL(y):y ε d]
U Spec, 2

6 v ε d
Premise

7 ~u ε d
Premise

8 ~v ε d & v ε d
Join, 4, 6

9 ~EXIST(y):~y ε d
Conclusion, 7

10 ~~ALL(y):~~y ε d
Quant, 9

11 ~~ALL(y):y ε d
Rem DNeg, 10

12 ALL(y):y ε d
Rem DNeg, 11

13 v ε d => ALL(y):y ε d
Conclusion, 6

14 ~[v ε d => ALL(y):y ε d] & [v ε d => ALL(y):y ε d]
Join, 5, 13

15 ~EXIST(y):~y ε d
Conclusion, 4

16 ~~ALL(y):~~y ε d
Quant, 15

17 ~~ALL(y):y ε d
Rem DNeg, 16

18 ALL(y):y ε d
Rem DNeg, 17

19 d ε d => ALL(y):y ε d
Conclusion, 3

20 ~[d ε d => ALL(y):y ε d]
U Spec, 2

21 [d ε d => ALL(y):y ε d] & ~[d ε d => ALL(y):y ε d]
Join, 19, 20

22 ~ALL(x):~[x ε d => ALL(y):y ε d]
Conclusion, 2

23 ~~EXIST(x):~~[x ε d => ALL(y):y ε d]
Quant, 22

24 EXIST(x):~~[x ε d => ALL(y):y ε d]
Rem DNeg, 23

25 EXIST(x):[x ε d => ALL(y):y ε d]
Rem DNeg, 24

---------------- end DC Proof proof -------------

[Mostowski Collapse]

With SET SPACES you cannot prove your "junk theorem".

/* Junk Theorem Currently Provable */
28 ALL(s):[Set(s) => EXIST(a):~a e s]
Rem DNeg, 27
http://www.dcproof.com/UniversalSet.htm

if you for example replace Set(s) by s ∈ 𝒫(U). Then what
would go through in Coq with properly typing would amount to.
You need to type the existential quantifier:

/* Junk Theorem Not Provable Anymore */
ALL(s):[s ∈ 𝒫(U) => EXIST(a):[U(a) & ~a e s]]

The above is not provable anymore. Sets s from 𝒫(U)
do not always have elements inside U that are outside
these sets. This is because we have that U ∈ 𝒫(U),

which then violates the above theorem. So the
Junk Theorem is not anymore provable if you
use properly SET SPACES as mathematicians do

one way or the other in most math books. Just
check out Terrence Tao what he writes. Or things
like sigma spaces in probability theory etc.. etc..

[Dan Christensen]

On Tuesday, May 2, 2023 at 9:50:05 AM UTC-4, Mostowski Collapse wrote:

[snip]

>
> 1 ∀x: ¬ (d(x) ⊃ ∀y:d(y))
> Premise
>
> 2 ¬ (d(_33664) ⊃ ∀y:d(y))
> U Spec 1
>

[snip]

There you go again, Mr. Collapse, introducing free variables by universal specification. You should know better by now. This isn't usually done in mathematical proofs. Let's just say it would raise a few eyebrows. It isn't allowed in DC Proof.

[Mostowski Collapse]

Your Set(_) is from some Naive set theory. And Russells
Paradox shows that it doesn't work the same way like
Russells Paradox showed Frege that is Naive comprehension

doesn't work as an axiom. Only your Set(_) doesn't
appear in an Axiom, but rather during modelling. So what
was the Frege fix by Zermelo:

Frege Naive Comprehension:
{ x | P(x) }
Zermelos Fix Non-Naive Comprehension:
{ x e A | P(x) }

Now there is an analogue problem with Dan-O-Matik now:

Dan-O-Matiks Naive Set Declaration:
Set(x)
What Mathematicians Use, i.e. "Types"
x e A

So I guess there is no escaping. Sooner or later
DC Poop would need to introduce Set Spaces as well,
and not only Function Spaces. The current approach by

DC Poop is surely doomed. And thats what the Russell
Paradox is all about, showing such bloopers.

[Dan Christensen]

On Thursday, May 4, 2023 at 2:47:31 AM UTC-4, Mostowski Collapse wrote:
> Your Set(_) is from some Naive set theory. And Russells
> Paradox shows that it doesn't work the same way like
> Russells Paradox showed Frege that is Naive comprehension
>
> doesn't work as an axiom. Only your Set(_) doesn't
> appear in an Axiom, but rather during modelling. So what
> was the Frege fix by Zermelo:
>
> Frege Naive Comprehension:
> { x | P(x) }
> Zermelos Fix Non-Naive Comprehension:
> { x e A | P(x) }
>

Example: In DC Proof, construct the subset of set x, a = {b in x : P(b)}

1 Set(x)
Axiom

2 EXIST(a):[Set(a) & ALL(b):[b in a <=> b in x & P(b)]]
Subset, 1

The Subset Axiom can only be invoked for objects declared to be a set (line 1). Nothing "naive" about that.

[Mostowski Collapse]

The Naive is here, the Set(s):

28 ALL(s):[Set(s) => EXIST(a):~a e s]
Rem DNeg, 27
http://www.dcproof.com/UniversalSet.htm

Do you think Terrence Tao would say, eh lets have a set Set(s)?

You can check yourself he gives an upper bound for X:

Exercise 10.3.5 from Analysis Vol.1 by Terence Tao.
Give an example of a subset X⊂R and a function f:X→R
which is differentiable on X, is such that f′(x)>0
for all x∈X, but f is not strictly monotone increasing.

[Dan Christensen]

On Thursday, May 4, 2023 at 11:41:22 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 4. Mai 2023 um 16:41:58 UTC+2:
> > On Thursday, May 4, 2023 at 2:47:31 AM UTC-4, Mostowski Collapse wrote:
> > > Your Set(_) is from some Naive set theory. And Russells
> > > Paradox shows that it doesn't work the same way like
> > > Russells Paradox showed Frege that is Naive comprehension
> > >
> > > doesn't work as an axiom. Only your Set(_) doesn't
> > > appear in an Axiom, but rather during modelling. So what
> > > was the Frege fix by Zermelo:
> > >
> > > Frege Naive Comprehension:
> > > { x | P(x) }
> > > Zermelos Fix Non-Naive Comprehension:
> > > { x e A | P(x) }
> > >
> > Example: In DC Proof, construct the subset of set x, a = {b in x : P(b)}
> >
> > 1 Set(x)
> > Axiom
> >
> > 2 EXIST(a):[Set(a) & ALL(b):[b in a <=> b in x & P(b)]]
> > Subset, 1
> >
> > The Subset Axiom can only be invoked for objects declared to be a set (line 1). Nothing "naive" about that.

> The Naive is here, the Set(s):
> 28 ALL(s):[Set(s) => EXIST(a):~a e s]
> Rem DNeg, 27
> http://www.dcproof.com/UniversalSet.htm

Wrong again, Mr. Collapse.

> Do you think Terrence Tao would say, eh lets have a set Set(s)?
>

[snip]

He has established that there are objects that are sets (e.g. the set of real numbers)) and some that are not (e.g. 4). If he was writing a formal proof using set theory, he would then have to formally indicate which objects are subject to the axioms of set theory (the sets). A predicate is a good way to do that.

[Mostowski Collapse]

Dang you are dumb, Dan-O-Matik, you even don't
know what Naive and Non-Naive Comprehension is?
And how Russell made Frege stumble?

Did you even go to school?

It seems you don't understand what is Naive and
what not. Here again in example of the subset axiom.
Its also naive if you use Set(_):

Naive [the b in x is missing]

1 Set(x)
Axiom

2 EXIST(a):[Set(a) & ALL(b):[b in a <=> P(b)]]
Subset, 1


Non-Naive [the b in x is there]

1 Set(x)
Axiom

2 EXIST(a):[Set(a) & ALL(b):[b in a <=> b in x & P(b)]]
Subset, 1

I am not objecting that you use Set(_). Why do
you think the usage of Set(_) is problematic?
Where did I say that. The Naive thing is using Set(_)

only, and not an upper bound as well [the b in x is missing].
The Non-Naive thing is using Set(_) and an upper bound.
[the b in x is there].

Now analyze this sentence by Terrence Tao:

Exercise 10.3.5 from Analysis Vol.1 by Terence Tao.
Give an example of a subset X⊂R and a function f:X→R
which is differentiable on X, is such that f′(x)>0
for all x∈X, but f is not strictly monotone increasing.

Does he say onle Set(X) or does he say more?

Dan Christensen schrieb:> Wrong again, Mr. Collapse.

>
>> Do you think Terrence Tao would say, eh lets have a set Set(s)?
>>
> [snip]
>
> He has established that there are objects that are sets (e.g. the set
of real numbers)) and some that are not (e.g. 4). If he was writing a
formal proof using set theory, he would then have to formally indicate
which objects are subject to the axioms of set theory (the sets). A
predicate is a good way to do that.

Mostowski Collapse schrieb:

[Mostowski Collapse]

A little History
The year was 1901. Just when the world of mathematics
had dealt with one set of paradoxes and foundational
crises regarding limits in calculus, a new batch had
emerged from set theory. Like many of his peers at
the time, young philosopher and mathematician Bertrand
Russell was hard at work trying to construct a firm
logical foundation for all of mathematics.

While working on the first of his books in the area,
the Principles of Mathematics, Russell came upon the
idea of a set of all sets which do not include
themselves. He soon realized that when you consider
whether this, in his words, "very peculiar class"
includes itself, "each alternative leads to its
opposite and there is a contradiction".
https://mathimages.swarthmore.edu/index.php/Russell's_Antinomy

In Naive Comprehension you could
deduce an Universal Set:

> 2 EXIST(a):[Set(a) & ALL(b):[b in a <=> P(b)]]
> Subset, 1

Just use for P(b) for example b=b. Thats the Zermelo
Fix, that Comprehension doesn't give the Universal Set
by introducing the side conditon b in x, and thus

that there is no contradiction with the
Russell Paradox. if you had Naive Comprehension,
you could deduce the Universal Set as follows:

2 EXIST(u):[Set(u) & ALL(b):[b in u <=> b=b]]
Subset, 1

Which is logically equivalent to:

2 EXIST(u):[Set(u) & ALL(b):[b in u]]
Subset, 1

And with the Russell Paradox this would
render your system inconsistent. In the old
times this inconsistency was called an Antinomy.

Mostowski Collapse schrieb:

> Dang you are dumb, Dan-O-Matik, you even don't
> know what Naive and Non-Naive Comprehension is?
> And how Russell made Frege stumble?
>
> Did you even go to school?
>
> It seems you don't understand what is Naive and
> what not. Here again in example of the subset axiom.
> Its also naive if you use Set(_):
>
> Naive [the b in x is missing]
>

[Mostowski Collapse]

While the Naive & Non-Naive distincintion is
usually applied to the Comprehension Axiom,
whether the type C e A is present or not:

/* C has a type */
{C ∈ A : P(C)} is a set
https://en.wikipedia.org/wiki/Axiom_schema_of_specification

We can also apply it how the Drinker Paradox
is modelled. A Drinker Paradox that uses
for example this Lemma here:

/* s doesn't have a type */

ALL(s):[Set(s) => EXIST(a):~a e s]

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

Is surely a naive rendering of the Drinker
Paradox. Since it does the same blunder like
in Naive comprehension. It doesn't bound

the set s. The variable is restricted to
a set. But otherwise its unrestricted.
It is unbounded, it can get a larger and

larger set. Leading to the anomaly that
using such a modelling of the Drinker Paradox,
a Naive modelling cannot cover this scenario:

Universe = {Anna, Bert, Carlo}
Drinkers = {Anna, Bert, Carlo}

Mostowski Collapse schrieb:

[Dan Christensen]

On Thursday, May 4, 2023 at 2:21:05 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb:> Wrong again, Mr. Collapse.
> >
> >> Do you think Terrence Tao would say, eh lets have a set Set(s)?
> >>
> > [snip]
> >
> > He has established that there are objects that are sets (e.g. the set
> > of real numbers)) and some that are not (e.g. 4). If he was writing a
> > formal proof using set theory, he would then have to formally indicate
> >which objects are subject to the axioms of set theory (the sets). A
> > predicate is a good way to do that.

[snip]

No comment? Not surprising.

>
> Naive [the b in x is missing]
>
> 1 Set(x)
> Axiom
>
> 2 EXIST(a):[Set(a) & ALL(b):[b in a <=> P(b)]]
> Subset, 1
>

Not from DC Proof.

>
> Non-Naive [the b in x is there]
> 1 Set(x)
> Axiom
>
> 2 EXIST(a):[Set(a) & ALL(b):[b in a <=> b in x & P(b)]]
> Subset, 1

[snip]

As from DC Proof. What is your point, Mr. Collapse?

[Mostowski Collapse]

I posted my point already see below, only your attention span
is the one of a squirel. Maybe buy some more memory
for your brains. I posted it here. You can replace Set(s)

by s ∈ 𝒫(U) or by Set(s) & s ∈ 𝒫(U) doesn't matter.
I am not critiquing your predicate Set(_). What makes
you think I am critiquing your predicate Set(_)?

Its from ZFCU? So what?

Mostowski Collapse schrieb am Donnerstag, 4. Mai 2023 um 01:16:39 UTC+2:
> With SET SPACES you cannot prove your "junk theorem".
>
> /* Junk Theorem Currently Provable */
> 28 ALL(s):[Set(s) => EXIST(a):~a e s]
> Rem DNeg, 27
> http://www.dcproof.com/UniversalSet.htm
>
> if you for example replace Set(s) by s ∈ 𝒫(U). Then what
> would go through in Coq with properly typing would amount to.
> You need to type the existential quantifier:
>
> /* Junk Theorem Not Provable Anymore */
> ALL(s):[s ∈ 𝒫(U) => EXIST(a):[U(a) & ~a e s]]
>
> The above is not provable anymore. Sets s from 𝒫(U)
> do not always have elements inside U that are outside
> these sets. This is because we have that U ∈ 𝒫(U),
>
> which then violates the above theorem. So the
> Junk Theorem is not anymore provable if you
> use properly SET SPACES as mathematicians do
>
> one way or the other in most math books. Just
> check out Terrence Tao what he writes. Or things
> like sigma spaces in probability theory etc.. etc..

https://groups.google.com/g/sci.logic/c/HQqQski92_Q/m/xr2vVMVwAwAJ

[Mostowski Collapse]

If you check out Terrence Tao he preferes s ⊆ U
over s ∈ 𝒫(U). This is also fine. Here you see a
usage of s ⊆ U by Terrence Tao, the X ⊆ R:

/* Terrence Tao rather uses s ⊆ U than s ∈ 𝒫(U) */

> Exercise 10.3.5 from Analysis Vol.1 by Terence Tao.
> Give an example of a subset X⊆R and a function f:X→R
> which is differentiable on X, is such that f′(x)>0
> for all x∈X, but f is not strictly monotone increasing.

We can also use s ⊆ U to erradicate your "junk theorem":

/* Junk Theorem Not Provable Anymore */

ALL(s):[s ⊆ U => EXIST(a):[a ∈ U & ~a e s]]

The above formula is what you would find in
a math text book. All sets that are quantified
are bounded. There are no undounded sets in it,

except for a "structure parameter" U.

[Dan Christensen]

On Thursday, May 4, 2023 at 2:32:51 PM UTC-4, Mostowski Collapse wrote:
> While the Naive & Non-Naive distincintion is
> usually applied to the Comprehension Axiom,
> whether the type C e A is present or not:
>
> /* C has a type */
> {C ∈ A : P(C)} is a set
> https://en.wikipedia.org/wiki/Axiom_schema_of_specification
>
> We can also apply it how the Drinker Paradox
> is modelled. A Drinker Paradox that uses
> for example this Lemma here:
>
> /* s doesn't have a type */
> ALL(s):[Set(s) => EXIST(a):~a e s]
> http://www.dcproof.com/UniversalSet.htm
>

Every set excludes something, i.e. there exist no set of everything. Nothing wrong with that. There are no "types" in ordinary set theory.

> Is surely a naive rendering of the Drinker
> Paradox.

Pathetic! Apparently you did not understand that this was just a lemma used in the proof of each of the following

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

Or

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

Or

EXIST(x):[x in drinkers => Q ]

> See:

Since it does the same blunder like
> in Naive comprehension. It doesn't bound
>
> the set s. The variable is restricted to
> a set.

More precisely, the variable being quantified is restricted by the unary predicate Set. No problem there.

> But otherwise its unrestricted.
> It is unbounded, it can get a larger and
>
> larger set. Leading to the anomaly that
> using such a modelling of the Drinker Paradox,
> a Naive modelling cannot cover this scenario:
>
> Universe = {Anna, Bert, Carlo}
> Drinkers = {Anna, Bert, Carlo}
>

You give different names to the same set. Why? What are you trying to prove?

[Mostowski Collapse]

Undeniable and possibly a little bit accidentatial you used a
lemma based on Russell Paradox in your proof.

Does the lemma also work 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

Or in DC Proof notation:

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

[Mostowski Collapse]

They have very similar proof structure, the
Drinker Paradox and its dual:

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

∃x(∃yDy → Dx) is valid.
https://www.umsu.de/trees/#~7x(~7yDy~5Dx)

So I guess to have them "set theoretic" instead
of using D(x) we would use x e drinkers, I guess
the "set theoretic" versions will both be based

on the little itzi bitzi tiny winy Russell lemma?
Since Russell is key for "set theoretic" versions?
Or is this not true and rather accidential?

[Dan Christensen]

Only if x previously introduced in an axiom or premise.

1. P(x)
Axiom

2. Set(drinkers)
Axiom

Lemma (see Russell's Paradox):

3. ALL(a):[Set(a) => EXIST(b):~b in a]
Axiom

4. Set(drinkers) => EXIST(b):~b in drinkers
U Spec, 3

5. EXIST(b):~b in drinkers
Detach, 4, 2

6. ~y in drinkers
E Spec, 5

7. ~y in drinkers | x in drinkers
Arb Or, 6

8. ~~y in drinkers => x in drinkers
Imply-Or, 7

9. y in drinkers => x in drinkers
Rem DNeg, 8

10. EXIST(a):[a in drinkers => x in drinkers]
E Gen, 9

11. EXIST(x):EXIST(a):[a in drinkers => x in drinkers]
E Gen, 10

[Mostowski Collapse]

Wrong placing of second EXIST, you proved:

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

But the dual Drinker Paradox is:

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

[Mostowski Collapse]

You can also lookup what is asked here (page 5):

The dual of the drinker paradox is the scheme
Hε(P x) := ∃y(∃xP x → P y) ,
https://arxiv.org/abs/1805.06216

[Dan Christensen]

On Thursday, May 4, 2023 at 8:09:16 PM UTC-4, Mostowski Collapse wrote:
> Wrong placing of second EXIST, you proved:
> EXIST(x):EXIST(a):[a in drinkers => x in drinkers]
> But the dual Drinker Paradox is:
> EXIST(x):[EXIST(a):[a in drinkers] => x in drinkers]

Translated Smullyan's proof of the dual Drinker Principle (26 lines in DC Proof):

EXIST(a):U(a)
=> EXIST(a):[U(a) & [EXIST(b):[U(b) & Drinker(b)] => Drinker(a)]]

Where U is the implicit "domain of discourse" in FOL.

More to follow.

[Mostowski Collapse]

Where Russells Paradox used? In a proof of this:

/* dual Drinker Paradox */

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

Hint: The dual of Russells Paradox would be:

Lemma (see dual Russell's Paradox):
3. ALL(a):[Set(a) => EXIST(b):b in a]
Axiom

Unless your set theory is inconsistent, it shouldn't
be provable. Since a counter example is the empty set.
So I guess your "More to follow" should say

"Nothing to follow" if you are honest and clever.

[Mostowski Collapse]

Two proofs, one found automatically, and one done manually
looking at the automatic proof. Interestingly for the manual
proof I needed the "Copy" inference rule in step 10.

How to find the automatic proof? Just type your query here:

?- gentzen(∃x:(∃y:d(y) ⊃ d(x)), N), !.
https://www.dogelog.ch/littab/doclet/docs/05_supplement/07_unicorn/example54/package.html

How to write a query? Check out this new tips:

Supported notation ⊥, A ⊃ B and ∀x:A.
Supported shorthands ¬ A = A ⊃ ⊥ and ∃x:A = ¬ ∀x: ¬ A.

-------------------- begin automatic proof --------------------------------

1 ∀x: ¬ (∃y:d(y) ⊃ d(x))
Premise

2 ¬ (∃y:d(y) ⊃ d(w))
U Spec 1

3 ∃y:d(y)
Premise

4 ¬d(w)
Premise

5 d(v)
Premise

6 ¬ (∃y:d(y) ⊃ d(v))
U Spec 1

7 ∃y:d(y)
Premise

8 ∃y:d(y) ⊃ d(v)
▲ Conclusion 7,5

9 ⊥
Detach 6,8

10 ¬d(v)
▲ Conclusion 5,9

11 ∀y: ¬d(y)
U Gen 10

12 ⊥
Detach 3,11

13 d(w)
▲ Reductio 4,12

14 ∃y:d(y) ⊃ d(w)
▲ Conclusion 3,13

15 ⊥
Detach 2,14

16 ∃x:(∃y:d(y) ⊃ d(x))
▲ Conclusion 1,15

-------------------- end automatic proof --------------------------------

-------------------- begin manual proof DC Proof --------------------------------

1 EXIST(z):z=z
Axiom

2 ALL(x):~[EXIST(y):D(y) => D(x)]
Premise

3 w=w
E Spec, 1

4 ~[EXIST(y):D(y) => D(w)]
U Spec, 2

5 EXIST(y):D(y)
Premise

6 ~D(w)
Premise

7 D(v)
Premise

8 ~[EXIST(y):D(y) => D(v)]
U Spec, 2

9 EXIST(y):D(y)
Premise

10 D(v)
Copy, 7

11 EXIST(y):D(y) => D(v)
Conclusion, 9

12 ~[EXIST(y):D(y) => D(v)] & [EXIST(y):D(y) => D(v)]
Join, 8, 11

13 ~EXIST(y):D(y)
Conclusion, 7

14 EXIST(y):D(y) & ~EXIST(y):D(y)
Join, 5, 13

15 ~~D(w)
Conclusion, 6

16 D(w)
Rem DNeg, 15

17 EXIST(y):D(y) => D(w)
Conclusion, 5

18 ~[EXIST(y):D(y) => D(w)] & [EXIST(y):D(y) => D(w)]
Join, 4, 17

19 ~ALL(x):~[EXIST(y):D(y) => D(x)]
Conclusion, 2

20 ~~EXIST(x):~~[EXIST(y):D(y) => D(x)]
Quant, 19

21 ~~EXIST(x):[EXIST(y):D(y) => D(x)]
Rem DNeg, 20

22 EXIST(x):[EXIST(y):D(y) => D(x)]
Rem DNeg, 21

-------------------- end proof DC Proof --------------------------------

[Mostowski Collapse]

Now still waiting for a proof of a set version
that makes essential use of Russell Paradox.
When will the "more to come" happen?

LMAO!

[Mostowski Collapse]

The Dan-O-Matik discorvery of how to apply Russells Paradox
in a generic way, amounts to this schema, where Dx is
a set membership relation:

∃x¬Dx → ∃x(Dx→Q) is valid.
https://www.umsu.de/trees/#~7x~3Dx~5~7x(Dx~5Q)

Intrestingly there exists the dual, which would indeed
resolve the dual Drinker Paradox:

∃xDx → ∃x(Q→Dx) is valid.
https://www.umsu.de/trees/#~7xDx~5~7x(Q~5Dx)

The only problem is, whereas Russells Paradox seems
to yield ∃x¬Dx where Dx is a set membership relation,
the Russells Paradox doesn't yield ∃xDx. The counter

example is D being empty. So I guess there is no chance
to apply the Russell Paradox in an essential way to
resolve the dual Drinker Paradox, which somehow also

shows that it is not relevant for the original Drinker
Paradox. If it were really key it would work for both
versions, dual and non-dual.

[Dan Christensen]

On Friday, May 5, 2023 at 6:35:02 AM UTC-4, Mostowski Collapse wrote:
> Where Russells Paradox used?

It is not required in the proof of the dual of DP.

[Mostowski Collapse]

The finite complete boolean lattice for the

Universe = {Anna, Bert}

isn't a moon walk, you can depict it asfollows, it
shows the possible Drinkers configurations:

____{Anna, Bert}
___/ ____________\
{Anna}________{Bert}
___\____________/
_________{}

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

So that Dan Christensen can apply the Russell Paradox
to the Drinker Paradox, is because of his error that
he doesn't take Drinkers from a complete lattice (Set(_)

isn't a complete lattice). The fix isn't that difficult though.

[Dan Christensen]

On Sunday, May 7, 2023 at 5:41:18 AM UTC-4, Mostowski Collapse wrote:
> The finite complete boolean lattice for the
>
> Universe = {Anna, Bert}
>
> isn't a moon walk, you can depict it asfollows, it
> shows the possible Drinkers configurations:
>
> ____{Anna, Bert}
> ___/ ____________\
> {Anna}________{Bert}
> ___\____________/
> _________{}
>
> https://en.wikipedia.org/wiki/Hasse_diagram
>
> So that Dan Christensen can apply the Russell Paradox
> to the Drinker Paradox, is because of his error that
> he doesn't take Drinkers from a complete lattice (Set(_)
>
> isn't a complete lattice).

[snip]

Wrong again, Mr. Collapse. It is taken as an ARBITRARY set. For ANY set S and ANY proposition Q (be it true or false), we have:

EXIST(x):[x in S => Q]

PROOF: http://www.dcproof.com/STGeneralizedDrinkersThm.htm (9 lines, DC Proof format)

You can, for example, substitute

S = the set of drinkers D

Q = ALL(y):[Pub(y) => y in D] where Pub(y) means that y is in a given pub.

Then you obtain the famous Drinkers' Paradox:

EXIST(x):[x in D => ALL(y):[Pub(y) => y in D]]

[Mostowski Collapse]

The class of arbitraty sets, i.e. those sets that satisfy
Set(_), isn't a complete lattice, therefore also not a boolean
algebra. You proved it yourself here:

Counter Example to Being a complete lattice:

ALL(s):[Set(s) => EXIST(a):~a e s]
http://www.dcproof.com/UniversalSet.htm

So when you assume drinkers comes from Set(_), and
don't further restrict it, you are dealing with an incomplete
lattice. If the class would be a complete lattice, we would

have some element in the lattice which is the
top, which can be expressed as:

EXIST(s):[Set(s) & ALL(a):[a e s]]

But you proved the nagation of it. So you refutet
the existence of a top-element.

Thats the error that you think drinkers comes from
Set(_) alone. drinkers comes from somewhere else.
Can you fix it?

[Dan Christensen]

On Sunday, May 7, 2023 at 11:31:11 AM UTC-4, Mostowski Collapse wrote:

[snip irrelevant discussion of classes and lattices]

> ALL(s):[Set(s) => EXIST(a):~a e s]
> http://www.dcproof.com/UniversalSet.htm

> So when you assume drinkers comes from Set(_), and
> don't further restrict it, you are dealing with an incomplete
> lattice.

We start with the premise :

1. Set(u) & ALL(a):a e u
Premise

We obtain a contradiction from it, so it must be false.

~EXIST(s):[Set(s) & ALL(a):a e s]

Or equivalently...

ALL(s):[Set(s) => EXIST(a):~a e s]

Simple as that. There no need to muddy the waters with your talk of classes or lattices, Mr. Collapse. As usual, you seem to be desperately grasping at straws.

[Mostowski Collapse]

Well you might think its irrelevant.
But you just proved something about the
extensions of Set(_).

So even if you don't know what you are
doing, you are yourself a lattice researcher
right now. What you prove is that

Set(_), the extension of it, is not a complete
lattice. It doesn't have a top element.
This lead Cantor to label the "absolute infinite"

as the "inconsistent multiplicity". Since like
in the expectation of Rusells Paradox, this
here is not element of the extension of Set(_):

U = { x | x = x }

You might also don't know what the terms
extension/intension mean. Don't worry. There is
a first time for everything. Maybe you know

what a door knob is? I don't want to say a door
knob has the higher IQ like you. But if a door knob
is connected to the internet, via some smart home

appliance, it might know what extension/intension means.
Just google it, if you don't have a logic book at home.

https://letmegooglethat.com/?q=extension+intension


Dan Christensen schrieb:

[Mostowski Collapse]

Some info for the school skipper:

So what was before Rusells Paradox (1901)?
It was Cantor who banged his head here,
the same thing:

If we start from the notion of a definite
multiplicity [[Vielheit]] (a system, a totality)
of things, it is necessary, as I discovered,
to distinguish two kinds of multiplicities
(by this I always mean definite multiplicities).

For a multiplicity can be such that the assumption
that all of its elements " are together " leads
to a contradiction, so that it is impossible to
conceive of the multi-plicity as a unity, as " one
finished thing ". Such multiplicities I call
absolutely infinite or inconsistent multiplicities.

From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931
https://books.google.ch/books?id=v4tBTBlU05sC

After Russell there were more mondaine
names. You can also call it an incomplete
lattice, etc.. etc..

Mostowski Collapse schrieb:

[Mostowski Collapse]

The only difference is that incomplete lattices
can be also finite. For example if you take
this complete lattice:

___{Anna, Bert}
___/ ____________\
{Anna}________{Bert}
___\____________/
_________{}

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

And remove {Anna, Bert} you get an
incomplete lattice, also a semi-lattice:

{Anna}________{Bert}
___\____________/
_________{}
https://en.wikipedia.org/wiki/Hasse_diagram

On the other hand the extension of your DC Poop
Set(_) is always infinite because you have the
powerset axiom. Because of the union axiom of

set theory, the lattice has also arbitrary meets,
And by Cantors theorem, you can prove:

|A| < |𝒫(A)|

So I guess there is no way to make the
extension Set(_) finite. Just Cantors theorem
will say that it is finite, and

we cannot make it finite by some loops?

Mostowski Collapse schrieb:

[Mostowski Collapse]

Corr.: Typo

So I guess there is no way to make the
extension Set(_) finite. Just Cantors theorem

will say that it is infinite, and

Mostowski Collapse schrieb:

[Dan Christensen]

On Sunday, May 7, 2023 at 2:34:46 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb:
> > On Sunday, May 7, 2023 at 11:31:11 AM UTC-4, Mostowski Collapse wrote:
> >
> > [snip irrelevant discussion of classes and lattices]
> >
> >> ALL(s):[Set(s) => EXIST(a):~a e s]
> >> http://www.dcproof.com/UniversalSet.htm
> >
> >> So when you assume drinkers comes from Set(_), and
> >> don't further restrict it, you are dealing with an incomplete
> >> lattice.
> >
> > We start with the premise :
> >
> > 1. Set(u) & ALL(a):a e u
> > Premise
> >
> > We obtain a contradiction from it, so it must be false.
> >
> > ~EXIST(s):[Set(s) & ALL(a):a e s]
> >
> > Or equivalently...
> >
> > ALL(s):[Set(s) => EXIST(a):~a e s]
> >
> > Simple as that. There no need to muddy the waters with your talk of classes or lattices, Mr. Collapse. As usual, you seem to be desperately grasping at straws.
> >

> Well you might think its irrelevant.

[snip]

I do. If you can somehow invalidate this proof, do get back to us, Mr. Collapse.
http://www.dcproof.com/UniversalSet.htm

Or better still, finally, after all these years, demonstrate how how DC Proof is inconsistent.

[Mostowski Collapse]

Your constant repeat of the irrelevant Russell Paradox, for the
Drinker Paradox, sounds like you are parroting your own fail:

Genius fail - Wile E Coyote
https://www.youtube.com/watch?v=Z34bwVB_2W4

LoL

[Mostowski Collapse]

I mean if this were true, i.e. the labeling "Generalized":

> For any proposition Q, be it true or false, we have:
> ALL(s):[Set(s) => EXIST(x):[x in s => Q]]
> Proof: http://www.dcproof.com/STGeneralizedDrinkersThm.htm (9 lines)

One could derive the specialized drinkers from it? Which is
obviously not the case. Where on the scale from 1-1000 of
utter bullshit is this claim in the name of all ChatGPT?

A cool overview of Generative AI Secto
https://twitter.com/DeepLearn007/status/1653796135683620867

Why isn't Dan Christensen / DC Poop listed?

[Dan Christensen]

On Monday, May 8, 2023 at 10:22:20 AM UTC-4, Mostowski Collapse wrote:
> I mean if this were true, i.e. the labeling "Generalized":
>
> > For any proposition Q, be it true or false, we have:
> > ALL(s):[Set(s) => EXIST(x):[x in s => Q]]
> > Proof: http://www.dcproof.com/STGeneralizedDrinkersThm.htm (9 lines)
>

[snip]

It is generalized in the sense that Q can be any proposition whatsoever, be it true or false. You can use to introduce predicates about drinkers being in a pub, or the moon being made of green cheese.

[Mostowski Collapse]

Well if your Q is "generalized", how "generlized" is this P:

/* Drinker Paradox */
∃x(Px → ∀yPy) is valid.
https://www.umsu.de/trees/#~7x(Px~5~6yPy)

It can be also ANY predicate!

Dan Christensen, you get carried away by some self invented bull shit.

[Dan Christensen]

On Thursday, May 11, 2023 at 7:10:04 PM UTC-4, Mostowski Collapse wrote:
> Well if your Q is "generalized", how "generlized" is this P:
>
> /* Drinker Paradox */
> ∃x(Px → ∀yPy) is valid.

In your "standard" FOL system. Not in the logic commonly used math proofs.

> https://www.umsu.de/trees/#~7x(Px~5~6yPy)
>
> It can be also ANY predicate!
>

Once again, in DC Proof, I have proven:

EXIST(a):U(a) => EXIST(a):[U(a) & [EXIST(b):[U(b) & Drinker(b)] => Drinker(a)]]

Where U is the so-called "domain of discourse" that is implicit in your "standard" FOL.

Proof: https://www.dcproof.com/SmullyansDrinkersPrincipleDual.htm

Yes, it works for ANY predicate in place of Drinker here.

[Mostowski Collapse]

IWell in this you should rename it to generalized drinker paradox.
Also this here:

~P => [P => Q]
Martial Implication
https://www.dcproof.com/IfPigsCanFly.html

You sould give it a special name, like
"generalized From a falsehood, all things follow"
since Q can be any proposition.

Oho, what a coincidence, the above loooks very
similar to this here:

EXIST(a):~a e s] => EXIST(x):[x in s => Q]]
http://www.dcproof.com/STGeneralizedDrinkersThm.htm

Can you prove this here in DC Proof?

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

This would explain how
~P => [P => Q]
Gives:
EXIST(a):~a e s] => EXIST(x):[x in s => Q]]

Dan Christensen schrieb:

[Mostowski Collapse]

This quantifier distribution over material implication
should be also provable in DC Proof. Since its also
valid for an empty domain. For an empty domain it gives:

T → (F → F)

Which is valid. So I guess you should be able to
prove this here in DC Proof, like Wolfgang Schwartz
tree tool can prove it:

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

And it would then explain how:

~P => [P => Q]

Implies:

EXIST(a):~a e s => EXIST(x):[x in s => Q]

Proof: Sketch
In ~P => [P => Q] we can replace P by anything,
so replace it by x in s:
~x in s => [x in s => Q]
Because x was arbitary we can use ALL:
ALL(x):[~x in s => [x in s => Q]]
Now use ∀x(Ax → Bx) → (∃yAy → ∃zBz):
EXIST(y):~y in s => EXIST(z):[x in s => Q]]

Q.E.D.

Mostowski Collapse schrieb am Freitag, 12. Mai 2023 um 12:06:00 UTC+2:
> Well in this case you should rename it to generalized drinker paradox.

[Dan Christensen]

On Friday, May 12, 2023 at 6:06:00 AM UTC-4, Mostowski Collapse wrote:
> IWell in this you should rename it to generalized drinker paradox.
> Also this here:
>
> ~P => [P => Q]

> Material Implication
> https://www.dcproof.com/IfPigsCanFly.html
>

ALL(p):[Set(p) => EXIST(x):[ x in p => Q]]

Not the same thing at all, Mr. Collapse. What makes you think they are?

[Mostowski Collapse]

What makes you think your nonsense of a generalized
drinker paradox has even the slightest relevance to
Smullyans Drinker paradox. Lets say s are the drinkers

and U is the house, and lets say both are sets. Then
drinkers in the house is naturally Subset(s,U). And what
is non-drinker, we would still look at the house.

Ultimately you cannot prove:

ALL(U):ALL(s):[Set(s) & Set(U) & Subset(s,U) => EXIST(a):[a e U & ~a e s]]

There is no Russell Paradox for the Smullyan Riddle.

[Mostowski Collapse]

Here is a video by renowned mathematician Martin Davis,
R.I.P. January 1, 2023, about the Drinker Paradox. He spent
like half of his carreer on the Drinker Paradox and was

known as the Drinker Pradox guy at RAND Corporation:

Hilbert's tenth problem and the Drinker Paradox:
https://www.youtube.com/watch?v=dQw4w9WgXcQ

[Dan Christensen]

On Sunday, May 21, 2023 at 9:59:36 AM UTC-4, Mostowski Collapse wrote:
> What makes you think your nonsense of a generalized
> drinker paradox has even the slightest relevance to
> Smullyans Drinker paradox.

[snip]

Wrong again, Mr. Collapse. Again, Smullyan informally states his Drinkers' Principle as follows:

"There exists someone such that whenever he (or she) drinks, everybody drinks."
--Smullyan, "What is the name of this book?" p.209

You can formalize this statement in at least two different ways:

(1) Using "standard" FOL implicitly that assumes a non-empty domain of discourse. If we make this assumption explicit in DC Proof, we would have something like:

EXIST(a):U(a) => EXIST(a):[U(a) & [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]

For any unary predicates U and Drinker. Note that every quantifier here is restricted by U.

(2) Using ordinary set theory, can obtain: EXIST(a):[a in D => ALL(b):b in D]

For any set D.

Slightly more interesting might be: EXIST(a):[a in D => ALL(b):[Pub(b) => b in D]

For any set D and unary predicate Pub.

> Ultimately you cannot prove:
>
> ALL(U):ALL(s):[Set(s) & Set(U) & Subset(s,U) => EXIST(a):[a e U & ~a e s]]
>

Again, what happens if U=s?

> There is no Russell Paradox for the Smullyan Riddle.

The resolution of Russell's Paradox is fundamental to set theory. Deal with it, Mr. Collapse.

[Mostowski Collapse]

Are you dumb or what, do you really ask:

> > Ultimately you cannot prove:
> > ALL(U):ALL(s):[Set(s) & Set(U) & Subset(s,U) => EXIST(a):[a e U & ~a e s]]
> Again, what happens if U=s?

Its a witness that makes the formula false. It s=U is one
of the COUNTER EXAMPLES that makes the formula false.
Thats the reason the formula cannot be proved.

If it were that the formula could be proved, this would mean
we have deduced that the formula is generally valid. And
if we would have such a proof, we would know,

that the formula is also true for s=U. But the counter example
shows that the formula is not true for s=U. So if your logic
and set theory is consistent, we can conclude that

the formula CANNOT BE PROVED.

Got it dumbo?

[Dan Christensen]

On Sunday, May 21, 2023 at 3:17:53 PM UTC-4, Mostowski Collapse wrote:
> Are you dumb or what, do you really ask:
> > > Ultimately you cannot prove:
> > > ALL(U):ALL(s):[Set(s) & Set(U) & Subset(s,U) => EXIST(a):[a e U & ~a e s]]
> > Again, what happens if U=s?

I think we can agree that we should NOT be able to prove that statement, the counter-example being U=s.

Good.

[Mostowski Collapse]

CANNOT BE PROVED = There is no Russel Paradox in the Drinker Paradox.

[Dan Christensen]

On Sunday, May 21, 2023 at 3:56:49 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Sonntag, 21. Mai 2023 um 21:50:25 UTC+2:
> > On Sunday, May 21, 2023 at 3:17:53 PM UTC-4, Mostowski Collapse wrote:

[snip childish abuse by Mr. Collapse]

> > > > > Ultimately you cannot prove:
> > > > > ALL(U):ALL(s):[Set(s) & Set(U) & Subset(s,U) => EXIST(a):[a e U & ~a e s]]
> > > > Again, what happens if U=s?
> > I think we can agree that we should NOT be able to prove that statement, the counter-example being U=s.
> >

> CANNOT BE PROVED = There is no Russel Paradox in the Drinker Paradox.

Wrong again, Mr. Collapse. A set-theoretic version of a proof of Smullyan's Drinkers Principle requires the Subset Axiom (Specification in ZFC theory), which leads to a resolution of Russell's Paradox in a sub-proof. Deal with it, Mr. Collapse.

[Mostowski Collapse]

Your Banana Solution with Russells Paradox doesn't apply.
The "Universal Set" inside the Drinker Paradox exists as the set
U, i.e. the "house". When you model s and U as sets.

You cannot go on and model s as set and then leave out U,
and not model it as a set, as you do. It doesn't make any
sense, since there is the scenario s = U.

Smullyan doesn't talk about Drinkers outside of the house,
and he clearly indicates the scenario s = U. Read
for yourself. Or cant you read?

A man was at a bar. He suddenly slammed down his
fist and said, " Gimme a drink, and give everyone elsch
a drink, caush when I drink, everybody drinksh!" So drinks
were happily passed around the house.
https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf

[Mostowski Collapse]

Measured in Bananas, Dan Christensen has already
reached levels of stupidity that go into tons and tons.

Take his nonsensical generalized Drinker Paradox,
based on Russell Paradox. There are even not enough

bananas on this planet to measure the involved stupidity.

[Mostowski Collapse]

The moment Dan Christensen invented his
generalized drinker paradox, around 10 years
ago in 2014. Or some other moment.

Banana Song (I'm A Banana)
https://www.youtube.com/watch?v=LH5ay10RTGY

[Dan Christensen]

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

Dan

On Sunday, May 21, 2023 at 7:29:28 PM UTC-4, Mostowski Collapse wrote:
> Your Banana Solution with Russells Paradox doesn't apply.
> The "Universal Set" inside the Drinker Paradox exists as the set
> U, i.e. the "house". When you model s and U as sets.
>

[snip]

[Mostowski Collapse]

Rather not, possibly more nonsense incoming.

Dan Christensen schrieb:

[Mostowski Collapse]

Dan Christensen halucinated:
> ∃x(x ∈ U) & s ⊆ U <---- your redundant restrictions, which are NOT required in my proof.
> => ∃x(x ∈ U & (x ∈ s => s = U))

You didn't prove:

∃x(x ∈ U) => ∃x(x ∈ U & (x ∈ s => s = U))

Try proving it from Russell Paradox. Its impossible.
It wont prove the above from your bullshit nonsense.

You cannot prove the above without s ⊆ U, there
are simple counter models, when the actual domain
of discourse D is larger than U. If you have:

D =\= U

Then s = D is a counter example to the formula.
But you can also use something smaller, like
s = U u {d} where d e D \ U.

Hints: Whats the actual domain of discourse? Its
the range of your unrestricted quantifiers ∃x and ∀x.

[Mild Shock]

Why is this condition, in a set theoretic version, reasonable:

s ⊆ U

You can try yourself. When you do the non-set theoretic version,
like below with predicate U(_) for the pun and predicate Drinker(_)
for the drinkers. Then you can prove:

ALL(x):U(x) => /* U is the universe */
ALL(x):[Drinker(x) => U(x)]

Or symbolically using ⊆ between predicates:

ALL(x):U(x) => /* U is the universe */
Drinker ⊆ U

So we have again s ⊆ U respectively Drinker ⊆ U. Why was
this swept under the rug, when you create your generalized drinker.
Is this part of the generalization, sweeping stuff under the rug?

BTW: Here is a DC Proof proof:

14 ALL(x):U(x) => ALL(x):[Drinker(x) => U(x)]
Conclusion, 1

---------------------------- cut here --------------------------------------

1 ALL(x):U(x)
Premise

2 ~ALL(x):[Drinker(x) => U(x)]
Premise

3 ~~EXIST(x):~[Drinker(x) => U(x)]
Quant, 2

4 EXIST(x):~[Drinker(x) => U(x)]
Rem DNeg, 3

5 ~[Drinker(u) => U(u)]
E Spec, 4

6 ~~[Drinker(u) & ~U(u)]
Imply-And, 5

7 Drinker(u) & ~U(u)
Rem DNeg, 6

8 Drinker(u)
Split, 7

9 ~U(u)
Split, 7

10 U(u)
U Spec, 1

11 ~U(u) & U(u)
Join, 9, 10

12 ~~ALL(x):[Drinker(x) => U(x)]
Conclusion, 2

13 ALL(x):[Drinker(x) => U(x)]
Rem DNeg, 12

14 ALL(x):U(x) => ALL(x):[Drinker(x) => U(x)]
Conclusion, 1

Dan Christensen schrieb am Sonntag, 21. Mai 2023 um 17:22:30 UTC+2:

[Mild Shock]

But the condition s ⊆ U is not so important. Already using
this alone, where U represents the guests of the pub:

EXIST(x):[x e U & (x e s => Q(x,s))]

Prevents your errorneous conclusion. After all, Smullyan
talks about a man at the bar, the place inside a pub
where you usually order a drink. Not on venus or mars:

"A man was at a bar. He suddenly slammed down his
fist and said, " Gimme a drink, and give everyone elsch
a drink, caush when I drink, everybody drinksh!" So drinks
were happily passed around the house."
https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf

You know how a bar looks like. Its basically a kind
of alevated desk, that separates the kitchen etc.. from
the rest of the pub, where one side you find the bar tenders,

and on the other side the guests.

[Mild Shock]

If your intention was to remove x e U, to make it general.
Then you commited an error in my opinion. FOL indicates
that the FOL reading of EXIST(x):[...] amounts to

EXIST(x):[U(x) & ...] when we start designating the universe
to some predicate U(_). Namely this here is provable:

ALL(x):U(x) => /* U is the universe */

=> [EXIST(x):A(x) => EXIST(x):[U(x) & A(x)]]

If you have ALL(x):U(x), you can basically omit U(x) & ...
since its redundant. If you don't have ALL(x):U(x),

then its not redundant. There is an analogue in the
set theoretic setting. If you don't have ALL(x):[x e U],
then you need EXIST(x):[x e U & ...] to correctly model

the "matter", i.e. to not sweep something under the rug,
and produce nonsense results.