Things dont go well. Now Dan Christensen aka Wonky
Man believes the Drinker Paradox needs the Russell Paradox.

I guess Zorns Lemma is indefinitely postponed.

Mostowski Collapse schrieb am Mittwoch, 23. September 2020 um 13:16:22 UTC+2:
> So whats the plan for proving Zorn's Lemma
> in DC Proof? Translate FOL to DC Proof?
>
> How do you think a FOL ZFC theorem is
> to be realized in DC Proof?

This Drinker Paradox:

∃x(Dx→∀yDy)

is logically equivalent to:

∃x∀y(Dx→Dy)

Even in some nonclassical logics. Its still not
some Aristoteles Term logic form. Does the
Drinker Paradox have some relationship

to Aristoteles Term logic?

Mostowski Collapse schrieb am Samstag, 15. Oktober 2022 um 13:21:20 UTC+2:
> Things dont go well. Now Dan Christensen aka Wonky
> Man believes the Drinker Paradox needs the Russell Paradox.
>
> I guess Zorns Lemma is indefinitely postponed.
> Mostowski Collapse schrieb am Mittwoch, 23. September 2020 um 13:16:22 UTC+2:
> > So whats the plan for proving Zorn's Lemma
> > in DC Proof? Translate FOL to DC Proof?
> >
> > How do you think a FOL ZFC theorem is
> > to be realized in DC Proof?

On Saturday, October 15, 2022 at 8:00:08 AM UTC-4, Mostowski Collapse wrote:
> This Drinker Paradox:
>
> ∃x(Dx→∀yDy)
>

It seems the proof of this requires an assumption of the existence a mysterious, overarching non-empty domain, making it quite useless in conventional mathematics. (See my thread on on this topic.)

Dan

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

How is it useless in conventional mathenatics.
Could you please explain? Is the theorem just or not?

LMAO!

Dan Christensen schrieb am Samstag, 15. Oktober 2022 um 16:30:17 UTC+2:
> On Saturday, October 15, 2022 at 8:00:08 AM UTC-4, Mostowski Collapse wrote:
> > This Drinker Paradox:
> >
> > ∃x(Dx→∀yDy)
> >
> It seems the proof of this requires an assumption of the existence a mysterious, overarching non-empty domain, making it quite useless in conventional mathematics. (See my thread on on this topic.)
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Dan Christensen aka wonky man halucinated:
> My set-theoretic version does not require it

How do you prove it without an non-empty domain?
Can you exactly show us how the drinker paradox

gets true in your version with an empty domain?
How does this sentence get true in an empty domain:

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

It can only get true if you used some assumption that
gets false in an empty domain. What was this assumption?

Well its easy, you used, for example:

Set(drinkers)
Axiom

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

Please prove Drinker Paradox without such an assumption,
and then your nonsense claims would make sense.

Mostowski Collapse schrieb am Samstag, 15. Oktober 2022 um 17:52:14 UTC+2:
> How is it useless in conventional mathenatics.
> Could you please explain? Is the theorem just or not?
>
> LMAO!
> Dan Christensen schrieb am Samstag, 15. Oktober 2022 um 16:30:17 UTC+2:
> > On Saturday, October 15, 2022 at 8:00:08 AM UTC-4, Mostowski Collapse wrote:
> > > This Drinker Paradox:
> > >
> > > ∃x(Dx→∀yDy)
> > >
> > It seems the proof of this requires an assumption of the existence a mysterious, overarching non-empty domain, making it quite useless in conventional mathematics. (See my thread on on this topic.)
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Its valid, no Russell Paradox needed (writing Exy for x ∈ y):

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

P.S.: You want the natural deduction proof, of this proof:
> ------------------------------------------------------------- (Ax)
> Da, Db |- Db, ∀yDy, ∃x(Dx → ∀yDy)
> ------------------------------------------------------------- (→R)
> Da |- Db, Db → ∀yDy, ∃x(Dx → ∀yDy)
> ------------------------------------------------------------ (∃R+C)
> Da |- Db, ∃x(Dx → ∀yDy)
> ------------------------------------------------- (∀R)
> Da |- ∀yDy, ∃x(Dx → ∀yDy)
> ------------------------------------------------- (→R)
> |- Da → ∀yDy, ∃x(Dx → ∀yDy)
> ------------------------------------------------- (∃R+C)
> |- ∃x(Dx → ∀yDy)

Well as I wrote, its already a natural deduction
proof, just replace the (R) labels by (I) labels.

Need more explanation?

R in sequent calculus = right introduction
I in natural deduction = introduction

They are the same, that is what NK (natural deduction)
and LK (sequent calculus) share. See also here:

Untersuchungen über das logische Schließen I
G. Gentzen - Mathematische Zeitschrift (1935)
https://eudml.org/doc/168546

Mostowski Collapse schrieb am Samstag, 15. Oktober 2022 um 18:05:27 UTC+2:
> Dan Christensen aka wonky man halucinated:
> > My set-theoretic version does not require it
>
> How do you prove it without an non-empty domain?
> Can you exactly show us how the drinker paradox
>
> gets true in your version with an empty domain?
> How does this sentence get true in an empty domain:
>
> EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]]
>
> It can only get true if you used some assumption that
> gets false in an empty domain. What was this assumption?
>
> Well its easy, you used, for example:
>
> Set(drinkers)
> Axiom
>
> http://www.dcproof.com/DrinkersThm1.htm" rel="nofollow" target="_blank">http://www.dcproof.com/DrinkersThm1.htm
>
> Please prove Drinker Paradox without such an assumption,
> and then your nonsense claims would make sense.
> Mostowski Collapse schrieb am Samstag, 15. Oktober 2022 um 17:52:14 UTC+2:
> > How is it useless in conventional mathenatics.
> > Could you please explain? Is the theorem just or not?
> >
> > LMAO!
> > Dan Christensen schrieb am Samstag, 15. Oktober 2022 um 16:30:17 UTC+2:
> > > On Saturday, October 15, 2022 at 8:00:08 AM UTC-4, Mostowski Collapse wrote:
> > > > This Drinker Paradox:
> > > >
> > > > ∃x(Dx→∀yDy)
> > > >
> > > It seems the proof of this requires an assumption of the existence a mysterious, overarching non-empty domain, making it quite useless in conventional mathematics. (See my thread on on this topic.)
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

Which inference rule is different in free logic. So
how would the longer proof for free logic look like,
if there is a proof in free logic at all? (Didn't try)

Anyway, sequent calculus proof with ALL(drinkers),
it needs one more application of (∀R) rule:

------------------------------------------------------------ (Ax)
Ead, Ebd |- Ebd, ∀yEyd, ∃x(Exd → ∀yEyd)
------------------------------------------------------------ (→R)
Ead |- Ebd, Ebd → ∀yEyd, ∃x(Exd → ∀yEyd)
------------------------------------------------------------ (∃R+C)
Ead |- Ebd, ∃x(Exd → ∀yEyd)
------------------------------------------------- (∀R)
Ead |- ∀yEyd, ∃x(Exd → ∀yEyd)
------------------------------------------------- (→R)
|- Ead → ∀yEyd, ∃x(Exd → ∀yEyd)
------------------------------------------------- (∃R+C)
|- ∃x(Exd → ∀yEyd)
------------------------------------------------- (∀R)
|- ∀d∃x(Exd → ∀yEyd)

Mostowski Collapse schrieb am Samstag, 15. Oktober 2022 um 18:32:04 UTC+2:
> Its valid, no Russell Paradox needed (writing Exy for x ∈ y):
>
> ∀d∃x(Exd → ∀yEyd) is valid.
> https://www.umsu.de/trees/#~6d~7x%28Exd~5~6yEyd%29
>
> P.S.: You want the natural deduction proof, of this proof:
> > ------------------------------------------------------------- (Ax)
> > Da, Db |- Db, ∀yDy, ∃x(Dx → ∀yDy)
> > ------------------------------------------------------------- (→R)
> > Da |- Db, Db → ∀yDy, ∃x(Dx → ∀yDy)
> > ------------------------------------------------------------ (∃R+C)
> > Da |- Db, ∃x(Dx → ∀yDy)
> > ------------------------------------------------- (∀R)
> > Da |- ∀yDy, ∃x(Dx → ∀yDy)
> > ------------------------------------------------- (→R)
> > |- Da → ∀yDy, ∃x(Dx → ∀yDy)
> > ------------------------------------------------- (∃R+C)
> > |- ∃x(Dx → ∀yDy)
>
> Well as I wrote, its already a natural deduction
> proof, just replace the (R) labels by (I) labels.
>
> Need more explanation?
>
> R in sequent calculus = right introduction
> I in natural deduction = introduction
>
> They are the same, that is what NK (natural deduction)
> and LK (sequent calculus) share. See also here:
>
> Untersuchungen über das logische Schließen I
> G. Gentzen - Mathematische Zeitschrift (1935)
> https://eudml.org/doc/168546
> Mostowski Collapse schrieb am Samstag, 15. Oktober 2022 um 18:05:27 UTC+2:
> > Dan Christensen aka wonky man halucinated:
> > > My set-theoretic version does not require it
> >
> > How do you prove it without an non-empty domain?
> > Can you exactly show us how the drinker paradox
> >
> > gets true in your version with an empty domain?
> > How does this sentence get true in an empty domain:
> >
> > EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]]
> >
> > It can only get true if you used some assumption that
> > gets false in an empty domain. What was this assumption?
> >
> > Well its easy, you used, for example:
> >
> > Set(drinkers)
> > Axiom
> >
> > http://www.dcproof.com/DrinkersThm1.htm" rel="nofollow" target="_blank">http://www.dcproof.com/DrinkersThm1.htm
> >
> > Please prove Drinker Paradox without such an assumption,
> > and then your nonsense claims would make sense.
> > Mostowski Collapse schrieb am Samstag, 15. Oktober 2022 um 17:52:14 UTC+2:
> > > How is it useless in conventional mathenatics.
> > > Could you please explain? Is the theorem just or not?
> > >
> > > LMAO!
> > > Dan Christensen schrieb am Samstag, 15. Oktober 2022 um 16:30:17 UTC+2:
> > > > On Saturday, October 15, 2022 at 8:00:08 AM UTC-4, Mostowski Collapse wrote:
> > > > > This Drinker Paradox:
> > > > >
> > > > > ∃x(Dx→∀yDy)
> > > > >
> > > > It seems the proof of this requires an assumption of the existence a mysterious, overarching non-empty domain, making it quite useless in conventional mathematics. (See my thread on on this topic.)
> > > > Dan
> > > >
> > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > Visit my Math Blog at http://www.dcproof.wordpress.com

We have some light at the end of the tunnel,
Dan Christense proved the Drinker Paradox
with proof by cases. But we saw him also

follow proof alleys. What are proof alleys?
How about doing this theorem in DC Proof:

Kőnig's lemma
It gives a sufficient condition for an infinite
graph to have an infinitely long path.
https://en.wikipedia.org/wiki/K%C5%91nig's_lemma

What if the alleyes never end. Is there
an infinite counter model then?

Newest low in the DC Proof discussions,
Wonky Man the Uber Papagayox claims this:

ALL(x):[x e u] & EXIST(x):[x e u]

Is the same as:

ALL(x):U(x) & EXIST(x):U(x)

Hint: The first is inconsistent. The second not.