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

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:20:31 PM UTC-5, Mostowski Collapse wrote:
> 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

[Chris M. Thomasson]

On 11/14/2022 3:57 PM, Mostowski Collapse wrote:
> The problem is you still don't understand FOL. Mathematicians
> do heavily use FOL for the following reason:

[...]

The people in the establishment... The bartender, The Mormon, and The
Boooooozer. What one will most likely consume an alcoholic beverage?

[Dan Christensen]

On Monday, November 14, 2022 at 6:57:47 PM UTC-5, Mostowski Collapse wrote:
> The problem is you still don't understand FOL. Mathematicians
> do heavily use FOL for the following reason:
>

If you want to restrict every quantifier in a proof to the same non-empty domain as implicitly done in FOL, you can do so explicitly in DC Proof. See for example: https://dcproof.com/SmullyansDrinkerPrinciple.htm

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

Not built-into DC Proof (or ZFC), but you might be able introduce some additional axioms for classes in DC Proof. Not something that interests me.

> 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.

[snip]

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)]]]

Not a whole lot of difference. Deal with it, Jan Burse.

[Dan Christensen]

On Monday, November 14, 2022 at 11:10:11 PM UTC-5, Dan Christensen wrote:
> On Monday, November 14, 2022 at 6:57:47 PM UTC-5, Mostowski Collapse wrote:
> > The problem is you still don't understand FOL. Mathematicians
> > do heavily use FOL for the following reason:
> >

> If you want to restrict every quantifier in a proof to the same non-empty domain as implicitly done in FOL, you can do so explicitly in DC Proof. See for example: https://dcproof.com/SmullyansDrinkerPrinciple.htm

Might "functions" in FOL also be simulated in DC Proof (i.e. in ordinary math textbook logic) by the following axioms?

1. EXIST(a):D(a) <------ the implicit "background" domain in FOL
Axiom

2. ALL(a):[D(a) => D(f(a))] <------ both "domain" and "codomain" of function f are effectively the FOL background domain D
Axiom

Comments?

[Ross A. Finlayson]

You're in a train tunnel.

There's a light at the end.

Can you hear it?

[Dan Christensen]

On Tuesday, November 15, 2022 at 11:25:18 AM UTC-5, Dan Christensen wrote:
> On Monday, November 14, 2022 at 11:10:11 PM UTC-5, Dan Christensen wrote:
> > On Monday, November 14, 2022 at 6:57:47 PM UTC-5, Mostowski Collapse wrote:
> > > The problem is you still don't understand FOL. Mathematicians
> > > do heavily use FOL for the following reason:
> > >
>
> > If you want to restrict every quantifier in a proof to the same non-empty domain as implicitly done in FOL, you can do so explicitly in DC Proof. See for example: https://dcproof.com/SmullyansDrinkerPrinciple.htm
> Might "functions" in FOL also be simulated in DC Proof (i.e. in ordinary math textbook logic) by the following axioms?
>
> 1. EXIST(a):D(a) <------ the implicit "background" domain in FOL
> Axiom
>
> 2. ALL(a):[D(a) => D(f(a))] <------ both "domain" and "codomain" of function f are effectively the FOL background domain D
> Axiom
>
> Comments?

Wouldn't work in DC Proof since f(x) must be an element of a set there. Maybe define FOL functionality in terms of predicates in DC Proof, like F here:

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

where D is the non-empty domain implicit in FOL.

[Dan Christensen]

Just reminder, as you have told us, Jan Burse, ∀a∃b(f(a)=b) is actually a valid theorem FOL, citing this result: https://www.umsu.de/trees/#~6a~7b(f(a)=b)

What is the domain and codomain of the function f here? If you have to ask... It can only be that mysterious, overarching, UNSPECIFIED, but non-empty domain of discourse.

[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.

[Dan Christensen]

On Wednesday, November 16, 2022 at 11:13:41 AM UTC-5, Mostowski Collapse wrote:

> The above would be possible if f and g were set-like.
> Dan Christensen schrieb am Mittwoch, 16. November 2022 um 01:52:27 UTC+1:
> > On Tuesday, November 15, 2022 at 6:21:54 PM UTC-5, Dan Christensen wrote:
> > > On Tuesday, November 15, 2022 at 11:25:18 AM UTC-5, Dan Christensen wrote:
> > > > On Monday, November 14, 2022 at 11:10:11 PM UTC-5, Dan Christensen wrote:
> > > > > On Monday, November 14, 2022 at 6:57:47 PM UTC-5, Mostowski Collapse wrote:
> > > > > > The problem is you still don't understand FOL. Mathematicians
> > > > > > do heavily use FOL for the following reason:
> > > > > >
> > > >
> > > > > If you want to restrict every quantifier in a proof to the same non-empty domain as implicitly done in FOL, you can do so explicitly in DC Proof. See for example: https://dcproof.com/SmullyansDrinkerPrinciple.htm
> > > > Might "functions" in FOL also be simulated in DC Proof (i.e. in ordinary math textbook logic) by the following axioms?
> > > >
> > > > 1. EXIST(a):D(a) <------ the implicit "background" domain in FOL
> > > > Axiom
> > > >
> > > > 2. ALL(a):[D(a) => D(f(a))] <------ both "domain" and "codomain" of function f are effectively the FOL background domain D
> > > > Axiom
> > > >
> > > > Comments?
> > > Wouldn't work in DC Proof since f(x) must be an element of a set there. Maybe define FOL functionality in terms of predicates in DC Proof, like F here:
> > >
> > > ALL(a):[D(a) => EXIST(b):[D(b) & [F(a,b) & ALL(c):[D(c) => [F(a,c) => c=b]]]]]
> > >
> > > where D is the non-empty domain implicit in FOL.
> > Just reminder, as you have told us, Jan Burse, ∀a∃b(f(a)=b) is actually a valid theorem FOL, citing this result: https://www.umsu.de/trees/#~6a~7b(f(a)=b)
> >
> > What is the domain and codomain of the function f here? If you have to ask... It can only be that mysterious, overarching, UNSPECIFIED, but non-empty domain of discourse.

> Thats the problem with you, you don't understand

> FOL. This here is consistent (V the universal predicate):
>
> ALL(z):V(z)
>

I think it is you who does not understand, Jan Burse. The underlying, though unspecified domain, can be ANY non-empty domain, e.g. the the residents of a village.

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

It doesn't seem to be necessary, even in FOL.

> 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
>

That result is really just postulating the existence of a function in FOL. Here is the DC Proof translation.

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

where D corresponds to the implicit non-empty domain in FOL, and F(a,b) can be informally interpreted as f(a)=b

While you could assume ALL(a):D(a) as you would have it, it is not required here.

> 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.

In most math textbooks, functions are defined as follows:

"Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y , such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range [codomain] Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
--Terence Tao, "Analysis I," p. 49

Similarly in DC Proof:

ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) in gra => a1 in dom & b in cod]
& ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod => [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]

=> EXIST(fun):[Function(fun,dom,cod)
& ALL(a1):ALL(b):[a1 in dom & b in cod => [fun(a1)=b <=> (a1,b) in gra]]]]]

Where:
dom = domain
cod = codomain
gra = graph
fun = function name

> 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 equality of functions is more commonly defined in math textbooks as follows:

"Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y with the same domain and range [codomain] are said to be equal, f = g [with respect to the domain X], if and only if f(x) = g(x) for all x ∈ X."
--Terence Tao, "Analysis I," p. 51

Similarly, in DC Proof:

ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& Function(f1,dom,cod) & Function(f2,dom,cod)

=> [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]

I hope this helps.

[Mostowski Collapse]

It doesn't postulate something, its a theorem you moron.
Only axioms postulate something, theorems derive something.

Whats wrong with you?

[Mostowski Collapse]

And where do you see ∃!, the uniqueness quantifier?
It only says ∃. Your translation is utter nonsense.

[Mostowski Collapse]

If the tree tool by Wolfgang Schwartz says:

... is valid

It did produce a proof, and proved a theorem.
Did you think ∀x∃yf(x)=y is an axiom?

Example:

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

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

P.S.: If it says:

.. is invalid

Then it found a couter model, and we can expect
that there is no proof of a corresponding theorem.

Example:

/* Predicates are not Sets */
∃x¬Sx is invalid.
https://www.umsu.de/trees/#~7x~3Sx

[Alex]

drinkers to much

[Dan Christensen]

On Wednesday, November 16, 2022 at 12:36:42 PM UTC-5, Mostowski Collapse wrote:

> > Dan Christensen schrieb am Mittwoch, 16. November 2022 um 18:27:20 UTC+1:

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

> > > That result is really just postulating the existence of a function in FOL.
> > > Here is the DC Proof translation.
> > > ALL(a):[D(a) => EXIST(b):[D(b) & [F(a,b) & ALL(c):[D(c) => [F(a,c) => c=b]]]]]
> > > where D corresponds to the implicit non-empty domain in FOL,
> > > and F(a,b) can be informally interpreted as f(a)=b

> And where do you see ∃!, the uniqueness quantifier?

The use of the f(x) notation ensures uniqueness. If f(x)=y1 and f(x)=y2, then y1=y2.

> It only says ∃. Your translation is utter nonsense.

Getting desperate, Jan Burse?

> Mostowski Collapse schrieb am Mittwoch, 16. November 2022 um 18:33:22 UTC+1:
> > It doesn't postulate something, its a theorem you moron.
> > Only axioms postulate something, theorems derive something.

Technically, every axiom is a theorem. If you enter an axiom of FOL, your tree program should say that it is a valid result.

[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]

On Wednesday, November 16, 2022 at 3:38:31 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)."

A formal axiom would be nice.

Here is DC Proof function Axiom:

ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
=> [ALL(a1):ALL(b):[(a1,b) in gra => a1 in dom & b in cod]
& ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in gra]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod => [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]

=> EXIST(fun):[Function(fun,dom,cod)
& ALL(a1):ALL(b):[a1 in dom & b in cod => [fun(a1)=b <=> (a1,b) in gra]]]]]

Where:
dom = domain
cod = codomain
gra = graph

What is the standard FOL equivalent? Maybe something like:

ALL(a):[D(a) => EXIST(b):[D(b) & [F(a,b) & ALL(c):[D(c) => [F(a,c) => c=b]]]]] (in DC Proof notation)

where D is the non-empty domain implicit in FOL, but explicitly stated here.

> Now how do you prove ∀x∃yf(x)=y in FOL.

No idea. It looks more like a definition to me. But maybe you can show us the proof using a form of natural deduction, Jan Burse? Hint: You would need to start with a formal definition of a function in FOL.

[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:15:17 AM UTC-5, Mostowski Collapse wrote:
> Your axiom violates EXIST(a):~D(a) what Smullyan assumes
> as the Universe of Discourse.

[snip]

Again, 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 better 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 --------------------------------------------------

[Fritz Feldhase]

On Saturday, February 4, 2023 at 8:27:45 PM UTC+1, Mostowski Collapse wrote:
> Come on Dan-O-Matik, you can do better 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 [...]

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

How about

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

Reduces the number of (different) predicates.

If there is someone who is a drinker or not a drinker, then ... (In other words, if there is someone, then ...)

[Dan Christensen]

On Saturday, February 4, 2023 at 2:27:45 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
> 27. EXIST(b):[U(b) & [Drinker(b) => ALL(a):[U(a) => Drinker(a)]]]
> Cases, 2, 26

[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

[Dan Christensen]

On Saturday, April 29, 2023 at 8:20:28 PM UTC-4, Mostowski Collapse wrote:

> Mostowski Collapse schrieb am Sonntag, 30. April 2023 um 02:17:13 UTC+2:
> > 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
> > > 27. EXIST(b):[U(b) & [Drinker(b) => ALL(a):[U(a) => Drinker(a)]]]
> > > Cases, 2, 26

> Now prove the other direction from 27 to 1.

That's just silly, Mr. Collapse. You cannot generally derive axioms from a theorem that was derived from those very axioms!

[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:46:07 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. 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.

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

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

[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 proble and the Drinker Paradox:
https://www.youtube.com/watch?v=dQw4w9WgXcQ

[Dan Christensen]

See my reply just now to your identical posting elsewhere (here or at sci.logic)

Dan

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

On Sunday, May 21, 2023 at 10:00:18 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. 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.
>
>

[snip]

[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?

[Mostowski Collapse]

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

[Dan Christensen]

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

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

[snip]

What a truly odd thing to say, Mr. Collapse.

Guessing at your meaning, the non-existence of a universal set (see Russell's Paradox) can indeed be used in a truly simple, set-theoretic proof of Smullyan's Drinkers' Principle. (See my previous postings here.) I hope this helps.

[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

[Dan Christensen]

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

> Your [snip childish abuse] Solution with Russells Paradox doesn't apply.

Wrong again, Mr. Collapse. It applies to a set-theoretic proof of Smullyan's Drinkers' Principle. See my recent postings on this topic here and at sci.logic.

[Mostowski Collapse]

You don't make a very mentally sane impression Dan!
The formula ∃x(x ∈ U) says the house U is non-empty.
The intro of Smullyans Riddle reads "A man was at a bar.":

**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

So we have there is a man at the bar. Which translates
into, when U = house, since the bar is located in the house:

> /* Set Theoretic Drinker Paradox */
> ∃x(x ∈ U)

And the rest is then:

> s ⊆ U => ∃x(x ∈ U & (x ∈ s => ∀y(y ∈ U => y ∈ s))

Why cant you prove it? It doesn't need the Russell Paradox.
You can prove it just like here:

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

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

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

Dan Christensen schrieb:

[Mostowski Collapse]

Ther rest is when we turn the bar scenario
exclamation, from "I" into "someone".

when I drink, everybody drinksh

~~>

when someone drinksh, everybody drinksh

But the scenario is basically the same.
The house is non-empty. We only look at
drinkers in the house.

The drinker paradox is an exercise in:
- existential import (because U is non-empty)
- correlation is not causation

If we would dig deeper into the "causation"
issue, we could ask will unter all circumstances
really "drinks happily pass around the house".

The conclusion is usually No. It is quite
possible that s =\= U. And then the formula
is satisfied by picking someone from U \ s.

Mostowski Collapse schrieb:

[Mostowski Collapse]

But to pick somebody from U \ s, you don't
need Russells Paradox. Ordinary Logic can do
that alredy. If s =\= U and s ⊆ U,

i.e. if we dont have:

∀y(y ∈ U => y ∈ s)

Then we have:

~∀y(y ∈ U => y ∈ s)

Which is logically equivalent to:

∃y(y ∈ U & ~y ∈ s)

LoL

Mostowski Collapse schrieb:

[Dan Christensen]

On Sunday, May 21, 2023 at 8:15:54 PM UTC-4, Mostowski Collapse wrote:

[snip childish abuse]

> The formula ∃x(x ∈ U) says the house U is non-empty.
> The intro of Smullyans Riddle reads "A man was at a bar.":
>

He states his Drinkers' Principle as follows:

"There exists someone such that whenever he (or she) drinks, everybody drinks." (p.209)

No explicit mention of any sets or predicates or houses (empty or not).

Also see my recent postings here on this topic here and at sci.logic

[Mostowski Collapse]

Dan Christensen was asking the moon and sun god
and then used his stick and stones to make some runes:

> No explicit mention of any sets or
> predicates or houses (empty or not).

if there is really no mention of sets and predicates,
and if our formalization is not allowed to provide
some added value of a transpilation,

I guess we need to give up. Then any formulation
is wrong. So I guess its back to stick and stones,
and not the brave new world of proof writers

and proof assistants.

LoL


Dan Christensen schrieb:

[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

[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.

[Mild Shock]

But the term "generalization" is wrongly applied. You didn't do
a generalization. A generalization doesn't have false positives
and only false positives. A generalization can be specialized,

so that the old result can be obtained. Take this example
from mathematics of a generalization. A real valued
matrice is a generalization of a single real number:

| a11 ... a1n |
... ....
| am1 ... amn |
https://en.wikipedia.org/wiki/Matrix_(mathematics)

In general matrices loose commutativity. For two square
matrices A and B, it is not necessary anymore the case
that their product commutes:

/* not provable anymore for square matrices n > 1 *
A*B = B*A

So in the generalization there is less provable. But you
have somewhere a lever so that you can still get the
special thingy. Namely square matrices of size 1,

behave like single real numbers:

/* provable for square matrices n = 1 *
A*B = B*A

Nothing of all this is found in your generalized Drinker Paradox.
It is rather a specialized Drinker Paradox, since it makes things
provable that werent provable before. And this is a one way

ticket. You have no lever to prove the original Drinker Paradox.
What would be your level to extract the original Drinker Paradox,
when you have, a muffin changed into a chihuahua:

> **Muffin:** ∃x¬Dx is invalid.
> https://www.umsu.de/trees/#~7x~3Dx

> **Chihuahua:** EXIST(x):[~x in s] is valid.
> http://www.dcproof.com/UniversalSet.htm

You went from general to special. You prove a special Drinker
Paradox, not a general Drinker Paradox.

[Dan Christensen]

On Monday, May 29, 2023 at 8:40:11 PM UTC-4, Mild Shock wrote:
> > > Conclusion it requires more work, to go from predicates
> > > to sets, than blindly replacing each predicate by a set
> > > membership.

> > I never claimed otherwise. In set theory, you have more tools at your disposal.

> > > It requires more when you want to
> > > preserve validity and invalidity, i.e. when you want to
> > > prevent false positives in the new formalization with sets.
> > [snip]
> >
> > "False positives?" With more tools, you can supposedly prove things that you could not prove without them.

> But the term "generalization" is wrongly applied.

Wrong.

> You didn't do
> a generalization. A generalization doesn't have false positives
> and only false positives. A generalization can be specialized,
>
> so that the old result can be obtained.

This is precisely what I have done here: http://www.dcproof.com/STGeneralizedDrinkersThm.htm

Here again, is Smullyan's informal definition of his Drinkers' Principle:

"[T]here exists someone such that whenever he (or she) drinks, everybody drinks." (1)

Using only your "standard" FOL modelling of Smullyan's DP, this translates to EXIST(x):[D(x) => ALL(y):D(y)] for any unary predicate D where D(x) means x is a drinker.

Using ordinary set theory and rules of logic (more tools!), in addition to (1), we can generalize:

"[T]here exists someone such that whenever he (or she) drinks, ANYTHING WHATSOEVER can be true." (2)

More formally: EXIST(x):[x in d => Q] for any set d and proposition Q, be it true or false

The "old result" is just the SPECIAL CASE of Q = ALL(y):y in d. Again, Q could be ANY proposition whatsoever, even Q = ~ALL(y):y in d, the negation of special case! AFAICT this insight is impossible using only FOL.

Now this does not mean that this is logically inconsistent. It does not mean that we can prove from this that both a statement AND its negation can be true.

[Mild Shock]

See my response to your crazyness in "Why is model theory needed?"

You don't get the FOL Drinker Paradox by specializing Q.

Whats wrong with you?

[Mild Shock]

Well if you restrict something, you get a "specialization",
and not a "generalization". Like if you restrict the natural
numbers N, into the even numbers E:

E = { n e N | n mod 2 = 0 }

Then you can also find formulas where you have a place
holder, where you can now plug in any other formula.
Thats an effect of "specialization", and not an effect

of "generalization". Example:

While the domain D was N, and the universe of discourse
was N, you could not prove:

/* Not provable for D=N if ALL(x):N(x) */
EXIST(x):[D(x) => Q]

When the domain D is E, and the universe of discourse
is still N, you can then prove:

/* Provable for D=E since ~ALL(x):E(x) */
EXIST(x):[D(x) => Q]

[Dan Christensen]

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

Dan

On Wednesday, May 31, 2023 at 4:44:25 AM UTC-4, Mild Shock wrote:
> Well if you restrict something, you get a "specialization",
> and not a "generalization". Like if you restrict the natural
> numbers N, into the even numbers E:
>
> E = { n e N | n mod 2 = 0 }

[snip]

[Mild Shock]

It would a win-win situation for everybody if Dan Christensen
could use the language that is found in math text books. We might
understand him, and he might understand some math.

And there is even a Unicode sign for specialization-generalization,
that is used math text books. You mignt have seen it already in your
life time, since you are not John Gabriel who was raised by some wolfs:

Unicode Character “⊊” (U+228A)
https://www.compart.com/en/unicode/U+228A

For example we could say the rational numbers are a
specialization of the real numbers:

ℚ ⊊ ℝ

They are more special, and hence you can prove the following,
for an arbitrary formula A:

∃x ∈ ℝ (x ∈ ℚ => A)

But a sane mathematician woudn't call the rational numbers more
general than the real numbers, only because the above theorem
with an arbitrary formula A is provable? Unless the person

is called Dan Christensen who lost his mind.

[Mild Shock]

The specialization-generalization sign:

> Unicode Character “⊊” (U+228A)
> https://www.compart.com/en/unicode/U+228A

Has a technical name, it is called "Subset of with Not
Equal To" in Unicode, it hints that it can be defined as follows:

P ⊊ Q <=> P ⊆ Q & P =\= Q

But mathematician usually simply say "proper subset"
for ⊊, in contrast to "subset" for ⊆. You can also
write it down with P and Q predicates, first observe

that P = Q <=> P ⊆ Q & Q ⊆ P. Therefore P =\= Q <=>
~(P ⊆ Q) v ~(Q ⊆ P). And therefore P ⊊ Q <=> P ⊆ Q &
~(Q ⊆ P). So an alternative statement would be:

P ⊊ Q <=> P ⊆ Q & Q ⊈ P

Which reads with predicates:

P ⊊ Q <=> ALL(x):[P(x) ⊆ Q(x)] & EXIST(x):[Q(x) & ~P(x)]

If Q=U is the domain of discourse, i.e. ALL(x):U(x), the above
reduces to, lets also use a set P=s for the other predicate:

s ⊊ U <=> ALL(x):[x e s => U(x)] & EXIST(x):[U(x) & ~(x e s)]

Or simplified, since from ALL(x):U(x) we have ALL(x):[x e s => U(x)]
anyway true, and EXIST(x):[U(x) & ~(x e s)] doesn't need the U(x).

So we get:

s ⊊ U <=> EXIST(x):[~(x e s)]

Thats what you proved here, every set s is a specialization
of the domain of discourse U:

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

Very easy!

[Dan Christensen]

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

Dan

On Wednesday, May 31, 2023 at 2:42:16 PM UTC-4, Mild Shock wrote:
> It would a win-win situation for everybody...

[snip]

[Mild Shock]

Its getting more and more generalized the more stuff
you add. First you have nothing added:

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

Then you add Set(_) and change D into a set s,
and you get already STGeneralizedDrinkerParadox:

9 ALL(s):[Set(s) => EXIST(x):[x e s => ALL(x):x e s]]
4 Conclusion, 2
http://www.dcproof.com/STGeneralizedDrinkersThm.htm

Then you add x e ℝ and replace Set(s) by s ⊊ ℝ and you
get the RAGeneralizedGeneralizedDrinkerParadox:

ALL(s):[s ⊊ ℝ => EXIST(x):[x e ℝ & (x e s => Q(x,s))]]

The more you add the more general it gets.
Ad infinitum. Whats so difficult to understand.

[Zach]

"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."

You are an imbecile.

[Dan Christensen]

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

Dan

On Wednesday, May 31, 2023 at 7:47:58 PM UTC-4, Mild Shock wrote:
> Its getting more and more generalized the more stuff
> you add. First you have nothing added:
>
> ∃x(Dx → ∀yDy) is valid.

[snip]

[Mild Shock]

What are you talking about? The RAGeneralized-
GeneralizedDrinkers has also an arbitrary Q(x,s):

/* Real Analysis Generalized Generalized Drinker Paradox */

> ALL(s):[s ⊊ ℝ => EXIST(x):[x e ℝ & (x e s => Q(x,s))]]

I can also shout, but not out of desperation, but since you did
the shouting via capital letters, so I do also some shouting:

for ARBITRARY predicate Q.

[Mild Shock]

The RAGeneralizedGeneralizedDrinkers has the advantage,
that unlike in the Smullyan proof, where the guest "jim" as
a non-drinker might not be needed, namely when everybody

is drinking in the pub, here we have always a non-drinker "jim",
which makes it possibly the generalized the Drinker Paradox,
so that for ARBITRARY predicate Q the implication holds.

But as a bonus "jim" is now from the real numbers. Because s ⊊ ℝ,
we have that ℝ \ s is non-empty so "jim" is from the ℝ \ s. So in
the generalized generalized Drinker Paradox there is a tremedous

improvement over Smullyans proof, who had two scenarios,
one scenario for ∀yDy and one scenario for ~∀yDy, and the
existential quantifier would pick "jim" accordingly:

Scenario 1: ∀yDy, the outer existential quantifier can pick
any "jim" which will be a drinker
Scenario 2: ~∀yDy, the outer existential quantifier must pick
a "jim" which is a non-drinker

So already Dan Christensens genius set theoretical
generalized drinker eliminated scenario 1. But his non-drinker,
in Dan Christensens genius pioneer proof of the STGeneralizedDrinker:

ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]
http://www.dcproof.com/STGeneralizedDrinkersThm.htm

In the above "jim" will be a non-drinker from the universe of
discourse, somebody from U \ s, where U is the universe of
discourse. This works for an ARBITRARY predicate Q.

In the improve real analysis generalized generalized
drinker paradox, the "jim" will be from the real numbers.
So we could generalize Smullyan once more:

/* Real Analysis Generalized Generalized Drinker Paradox */
> ALL(s):[s ⊊ ℝ => EXIST(x):[x e ℝ & (x e s => Q(x,s))]]

[Mild Shock]

In second order logic, one cannot prove your nonsense.
In second order logic one would have capital case variable
names X, Y, ... for "sets" and lower case variable names x, y, ...

for "elements". You cannot prove in second order logic
your nonsense. In second order logic there is no need for
Set(_) since there is the variable casing convention:

/* Not Provable in Second Order Logic */
ALL(X):EXIST(x):~x e X
http://www.dcproof.com/UniversalSet.htm

Why is it not provable in second order logic? Well
if it where provable ALL(X):EXIST(x):~x e X in second
order logic, it would hold for any second order logic

model. But a second order logic has usually X=U
as a possible value for a "set" variable. And we have
ALL(x):x e U. End of demonstration.

[Mild Shock]

Here is the same stipulation, that a mathematician working
in a certain way with second order logic, wouldn't be
bothered by Russells Paradox:

"On page 24, footnote 16 reads, in part, "as far as I know, Hilbert never
considered a universal all-encompassing domain. Thus, according to
the thesis at hand, he should not have been bothered by Russell's paradox."

Stewart Shapiro, Foundations without Foundationalism: A Case for Second-Order Logic
(New York/Oxford, Oxford University Press, 1991)
Reviewed by CRAIG SMORYNSKI
https://projecteuclid.org/journals/modern-logic/volume-4/issue-3/Review-of-Stewart-Shapiro-Foundations-without-foundationalism-A-case-of/rml/1204835293.pdf

[Mild Shock]

About this competition by CeBo:
https://www.freelancer.com/projects/mathematics/Find-Common-Math-Theorem-Proven/

You can prove the Drinker Paradox, a set theoretic version of, with
with very little of ZFC. Would this qualify for this competition?

I would reveal one of the best kept secrets, even not known to
man, last to speak for Dan Christensen, and his DC Poop.

[Mild Shock]

Actually there is a class of proofs that fit this schema:

"Just tell me the theorem and a link to a normal (non-ZFC) proof
and I will make a milestone for it and release it when you supply
a link to a proof of it using only ZFC."
https://www.freelancer.com/projects/mathematics/Find-Common-Math-Theorem-Proven/

Sometimes a second order logic theorem can be translated
into a first order logic theorem with a little ZFC. A large class
of theorems that are in second order logic, are theorems

from second-order arithmetic. Second-order arithmetic is
also the main subject of reverse mathematics. There is also
a related model theory for certain subsystems:

The term was introduced by Mostowski (1959) as a
strengthening of the notion of ω-model.
https://en.wikipedia.org/wiki/Beta-model

Guess what the two sorts of second
order will be model theoretically?

[Mild Shock]

Never heard about reverse mathematic?
This introduction has one of its main sections:

An Introduction to Reverse Mathematics
Second Order Arithmetic
variables x,y,z,. . . that range over natural numbers and
X,Y ,Z,. . . that range over sets of natural numbers.
https://legacy-www.math.harvard.edu/theses/senior/cobb/cobb.pdf

Probably a book that Dan Christensen never
has opened, only maybe seen its cover.

What color is the cover, beige?

[Mild Shock]

Yes the uniqueness quantifier thats the blind spot of Dan O
Matik, the fraudster that claims to have written DC Proof tool.
He doesn't understand simple quantifiers such as "indeterminate"

and "paradoxical" that are related to counting, possibly refutes
Habermas Universam pragmatism that sane people can understand
other sane people, or he is completely insane. But its not so

difficult to see that the usual quantifiers:

∀x A(x): "forall"
∃x A(x): "exists"

Do only express a very small fraction of the quantitive
measurements available in natural language. This is
a nice addition:

Ix A(x): "indeterminate", "many", can be defined as: ∃x∃y(A(x) & A(y) & x=\=y)
Px A(x): "paradoxical", "none", can be defined as: ~∃xA(x)
∃!x A(x): "determinate", "unique" can be defined as: ~Px A(x) & ~Ix A(x)

Have Fun!

Mostowski Collapse schrieb am Mittwoch, 16. November 2022 um 18:36:42 UTC+1:
> And where do you see ∃!, the uniqueness quantifier?
> It only says ∃. Your translation is utter nonsense.

[Dan Christensen]

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

Dan

On Saturday, July 29, 2023 at 3:40:41 PM UTC-4, Mild Shock wrote:
> Yes the uniqueness quantifier thats the blind spot...

[snip]