Since Dan-O-Matik aka Wonky Man believes in Wikipedia, this
could help cure his botched Drinker Paradox. Might he take a
closer look what he proved:

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

And then what Wikipedia wants:

∃x e P [D(x) => ∀y e P D(y)]
https://en.wikipedia.org/wiki/Drinker_paradox

or expanding the bounded quantifier:

∃x[x e P & [D(x) => ∀x[x e P => D(y)]]
https://en.wikipedia.org/wiki/Bounded_quantifier#Bounded_quantifiers_in_set_theory

If we use y e drinkers for D(y), and z e pub for z e P, what
do we get. Correct a different formula:

/* Corrected Formula */
EXIST(x):[x e pub & [x e drinkers => ALL(a):[a e pub => a e drinkers]]]

Would he dare proving the above formula in DC Proof?
Can he do it without Russell Paradox?

Maybe the Wikipedia Articel should be fixed in as far,
Works also for Classes:

Maybe the formula should be amended, since the
Drinking Principle also works for classes, it is not
the case that P must be set. So the more correct
formula would be, and what is provable:

∃xP(x) => ∃x(P(x) & (D(x) => ∀y(P(y)=>D(y)))

The elegance is now that when we rely on the universe of
discourse as representing the pub, we get this theorem,
which is also provable in FOL, since FOL has the non-empty
universe of discourse assumption:

∃x(D(x) => ∀yD(y))

We can deduce by Occam's razor that the Drinking Principle
is not about sets, since Smullyan doesn't mention them.
He also gives a hint that it could be the domain of
discourse even, by his epilogue:

Logician: I know a fellow who is such that whenever he drinks, everyone does.

Student: I just don't understand. Do you mean everyone on earth?

Logician: Yes, naturally.

https://archive.org/details/whatisnameofthis00smul/page/210/mode/2up

Mostowski Collapse schrieb am Montag, 17. Oktober 2022 um 09:06:30 UTC+2:
> Since Dan-O-Matik aka Wonky Man believes in Wikipedia, this
> could help cure his botched Drinker Paradox. Might he take a
> closer look what he proved:
>
> /* Wrong Formula */
> EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]]
> http://www.dcproof.com/DrinkersThm1.htm
>
> And then what Wikipedia wants:
>
> ∃x e P [D(x) => ∀y e P D(y)]
> https://en.wikipedia.org/wiki/Drinker_paradox
>
> or expanding the bounded quantifier:
>
> ∃x[x e P & [D(x) => ∀x[x e P => D(y)]]
> https://en.wikipedia.org/wiki/Bounded_quantifier#Bounded_quantifiers_in_set_theory
>
> If we use y e drinkers for D(y), and z e pub for z e P, what
> do we get. Correct a different formula:
>
> /* Corrected Formula */
> EXIST(x):[x e pub & [x e drinkers => ALL(a):[a e pub => a e drinkers]]]
>
> Would he dare proving the above formula in DC Proof?
> Can he do it without Russell Paradox?

On Monday, October 17, 2022 at 3:06:30 AM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> Since Dan-O-Matik aka Wonky Man believes in Wikipedia, this
> could help cure his botched Drinker Paradox.

I have presented a novel (AFAIK) and purely set-theoretic version of DP. It is apparently driving poor Jan Burse insane with jealousy. See my recent thread "The Drinker’s Paradox: A Tale of Three Paradoxes (reposted)" here at sci.math

Dan

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

I really admire Dan Christensens approach to computerized
logic. He is really helping the cause. His newest coutious
tale about "pathological" formulas where a wild propositional

formula appears is very useful. We now have a new name
for "negation". So if we prove:

~A => (A => B)

We must admit that since a wild propositional variable appears,
that we didn't prove something about implication

and "negation". Out contraire, we prove "pathology"!

Dan Christensen schrieb am Mittwoch, 21. September 2022 um 07:23:28 UTC+2:
> Here is the truth table for the IMPLIES-operator:
>
> A B A=>B
> T T T
> T F F
> F T T
> F F T

But since he is living in a lower echolon of logic, we must excuse
that he is not fluent in the following identity:

~A <=> ∀B (A => B)

This is unlike Coq, which can prove the same:

Lemma ex1: forall (Q:Prop), ~Q <-> (forall (P:Prop), (Q -> P)).
intuition.
specialize (H False).
apply H.
apply H0.
Qed.
https://coq.inria.fr/download

The identity requires that one not only looks at the => direction
but also in the <= direction. And of course quantifying over
propositional variables can be challenging.

Mostowski Collapse schrieb am Dienstag, 25. April 2023 um 03:34:28 UTC+2:
> I really admire Dan Christensens approach to computerized
> logic. He is really helping the cause. His newest coutious
> tale about "pathological" formulas where a wild propositional
>
> formula appears is very useful. We now have a new name
> for "negation". So if we prove:
>
> ~A => (A => B)
>
> We must admit that since a wild propositional variable appears,
> that we didn't prove something about implication
>
> and "negation". Out contraire, we prove "pathology"!
>
> Dan Christensen schrieb am Mittwoch, 21. September 2022 um 07:23:28 UTC+2:
> > Here is the truth table for the IMPLIES-operator:
> >
> > A B A=>B
> > T T T
> > T F F
> > F T T
> > F F T

Jumbo dumbo idiot Dan Christensen with a truth table like that leaves no place for mathematics to have 0 as divisor as undefined. Dan never had a logical brain to even step foot on the turf that is Logic.

Dan is a mindless pathetic idiot of math and logic and belongs in a sanatorium, not in a classroom.

Here is an example of Dan Christensen fumbling with the most simple of logic reasoning, and yet Canada keeps allowing this misfit to dig deeper into logic.

The stupid Dan Christensen always chokes up when it comes to logic or even just plain commonsense with his 2 OR 1 = 3 and his AND as subtraction.

On Wednesday, January 25, 2017 at 10:08:09 AM UTC-6, Peter Percival wrote:
> Dan Christensen wrote:
> > On Wednesday, January 25, 2017 at 9:47:32 AM UTC-5, Archimedes Plutonium wrote:
> >> On Wednesday, January 25, 2017 at 8:27:19 AM UTC-6, Dan Christensen wrote:
> >>> On Wednesday, January 25, 2017 at 9:16:52 AM UTC-5, Archimedes Plutonium wrote:
> >>>> PAGE58, 8-3, True Geometry / correcting axioms, 1by1 tool, angles of logarithmic spiral, conic sections unified regular polyhedra, Leaf-Triangle, Unit Basis Vector
> >>>>
> >>>> The axioms that are in need of fixing is the axiom that between any two points lies a third new point.
> >>>
> >>> The should be "between and any two DISTINCT points."
> >>>
> >>
> >> What a monsterous fool you are
> >>
> >
> > OMG. You are serious. Stupid and proud of it.
>
> And yet Mr Plutonium is right. Two points are distinct (else they would
> be one) and it is not necessary to say so.
>

Apparently Dan Christensen never took calculus or flunked it with this statement.
On Tuesday, June 2, 2015 at 8:57:54 AM UTC-5, Dan Christensen wrote:
> On Tuesday, June 2, 2015 at 2:32:51 AM UTC-4, Archimedes Plutonium wrote:
> > The nonexistence of a curved angle because there is no way to measure the angle if either one of the rays is not a straightline segment at the vertex,
>
> From the derivative of each curve at the point of contact you have the slopes of their respective tangents there. (Assuming derivatives are defined there.) From these slopes, you should be able to calculate angle formed.
>
>
> Dan

On Wednesday, September 21, 2022 at 12:23:28 AM UTC-5, Dan Christensen wrote:
> Here is the truth table for the IMPLIES-operator:
>
> A B A=>B
> T T T
> T F F
> F T T
> F F T
>
> Judging by frequent questions at MSE (at least once every day) on this topic, there seems to be much confusion about this one, simple table.
>
> This table is often used to "define" the IMPLIES-operator in introductory textbooks. No real explanation is usually given, just a few examples. There is a good reason for this, namely that to truly understand why it works, you must understand some basic methods of proof, i.e. the following rules of inference in propositional logic:
>
> 1. Premise
> 2. Conclusion (intro =>, intro ~)
> 3. Join (intro &)
> 4. Split (elim &)
> 5. Detachment (elim =>)
> 6. Remove ~~
>
> (For an excellent introduction to these rules of inference, you need only work your way through only the first 3 (of 13) examples in the DC Proof tutorial.)
>
> The above truth table is really just a table of the following 4 theorems in propositional logic:
>
> 1. A & B => [A => B]
>
> 2. A & ~B => ~[A => B]
>
> 3. ~A & B => [A => B]
>
> 4. ~A & ~B => [A => B]
>
> *****************************************************************
>
> Thm 1: A & B => [A => B]
>
> 1. A & B
> Premise
>
> 2. A
> Premise
>
> 3. B
> Split, 1
>
> 4. A => B
> Conclusion, 2
>
> 5. A & B => [A => B]
> Conclusion, 1
>
> *****************************************************************
>
> Thm 2: A & ~B => ~[A => B]
>
> 1. A & ~B
> Premise
>
> 2. A => B
> Premise
>
> 3. A
> Split, 1
>
> 4. ~B
> Split, 1
>
> 5. B
> Detach, 2, 3
>
> 6. ~B & B
> Join, 4, 5
>
> 7. ~[A => B]
> Conclusion, 2
>
> 8. A & ~B => ~[A => B]
> Conclusion, 1
>
> *****************************************************************
>
> Thm 3: ~A & B => [A => B]
>
> 1. ~A & B
> Premise
>
> 2. A
> Premise
>
> 3. B
> Split, 1
>
> 4. A => B
> Conclusion, 2
>
> 5. ~A & B => [A => B]
> Conclusion, 1
>
> *****************************************************************
>
> Thm 4: ~A & ~B => [A => B]
>
> 1. ~A & ~B
> Premise
>
> 2. A
> Premise
>
> 3. ~B
> Premise
>
> 4. ~A
> Split, 1
>
> 5. A & ~A
> Join, 2, 4
>
> 6. ~~B
> Conclusion, 3
>
> 7. B
> Rem DNeg, 6
>
> 8. A => B
> Conclusion, 2
>
> 9. ~A & ~B => [A => B]
> Conclusion, 1
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Whats a blind spot? I mean its in the truth table, isn't it?

~A <=> ∀B (A => B)

Here another example of a blind spot:

"When bees make hexagons in their hives, the six-sided
shapes fit together perfectly. In fact, we’ve actually never
seen bees make any other shape. That’s what I found out
when I visited my friend Sue Cobey, a bee researcher
at Washington State University."
https://www.nwpb.org/ask-dr-universe/why-do-bees-make-hexagons-in-their-hives/

Wrong, check out Australia for a counter example:

Types of stingless bees
https://www.youtube.com/watch?v=auwDFVEs_fQ

Mostowski Collapse schrieb am Dienstag, 25. April 2023 um 03:39:33 UTC+2:
> But since he is living in a lower echolon of logic, we must excuse
> that he is not fluent in the following identity:
>
> ~A <=> ∀B (A => B)
>
> This is unlike Coq, which can prove the same:
>
> Lemma ex1: forall (Q:Prop), ~Q <-> (forall (P:Prop), (Q -> P)).
> intuition.
> specialize (H False).
> apply H.
> apply H0.
> Qed.
> https://coq.inria.fr/download
>
> The identity requires that one not only looks at the => direction
> but also in the <= direction. And of course quantifying over
> propositional variables can be challenging.
> Mostowski Collapse schrieb am Dienstag, 25. April 2023 um 03:34:28 UTC+2:
> > I really admire Dan Christensens approach to computerized
> > logic. He is really helping the cause. His newest coutious
> > tale about "pathological" formulas where a wild propositional
> >
> > formula appears is very useful. We now have a new name
> > for "negation". So if we prove:
> >
> > ~A => (A => B)
> >
> > We must admit that since a wild propositional variable appears,
> > that we didn't prove something about implication
> >
> > and "negation". Out contraire, we prove "pathology"!
> >
> > Dan Christensen schrieb am Mittwoch, 21. September 2022 um 07:23:28 UTC+2:
> > > Here is the truth table for the IMPLIES-operator:
> > >
> > > A B A=>B
> > > T T T
> > > T F F
> > > F T T
> > > F F T

How it started:

The Antique Greeks, true champions in telling Cautionary Tales,
involving Propositional Quantifiers as well, maybe modally
attached to an Agent:
https://en.wikipedia.org/wiki/Epimenides_paradox (circa 600 BC)

How its groing:

Dan Christensen, left his job at the Cheese Cake factory, just
like John Gabriel in Calculus, proclaims himself as champion of
telling Cautionary Tales in Logic, but all he does is showing ignorance of:
~A <=> ∀B (A => B)

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 09:26:56 UTC+2:
> Whats a blind spot? I mean its in the truth table, isn't it?
> ~A <=> ∀B (A => B)
> Here another example of a blind spot:
>
> "When bees make hexagons in their hives, the six-sided
> shapes fit together perfectly. In fact, we’ve actually never
> seen bees make any other shape. That’s what I found out
> when I visited my friend Sue Cobey, a bee researcher
> at Washington State University."
> https://www.nwpb.org/ask-dr-universe/why-do-bees-make-hexagons-in-their-hives/
>
> Wrong, check out Australia for a counter example:
>
> Types of stingless bees
> https://www.youtube.com/watch?v=auwDFVEs_fQ
> Mostowski Collapse schrieb am Dienstag, 25. April 2023 um 03:39:33 UTC+2:
> > But since he is living in a lower echolon of logic, we must excuse
> > that he is not fluent in the following identity:
> >
> > ~A <=> ∀B (A => B)
> >
> > This is unlike Coq, which can prove the same:
> >
> > Lemma ex1: forall (Q:Prop), ~Q <-> (forall (P:Prop), (Q -> P)).
> > intuition.
> > specialize (H False).
> > apply H.
> > apply H0.
> > Qed.
> > https://coq.inria.fr/download
> >
> > The identity requires that one not only looks at the => direction
> > but also in the <= direction. And of course quantifying over
> > propositional variables can be challenging.
> > Mostowski Collapse schrieb am Dienstag, 25. April 2023 um 03:34:28 UTC+2:
> > > I really admire Dan Christensens approach to computerized
> > > logic. He is really helping the cause. His newest coutious
> > > tale about "pathological" formulas where a wild propositional
> > >
> > > formula appears is very useful. We now have a new name
> > > for "negation". So if we prove:
> > >
> > > ~A => (A => B)
> > >
> > > We must admit that since a wild propositional variable appears,
> > > that we didn't prove something about implication
> > >
> > > and "negation". Out contraire, we prove "pathology"!
> > >
> > > Dan Christensen schrieb am Mittwoch, 21. September 2022 um 07:23:28 UTC+2:
> > > > Here is the truth table for the IMPLIES-operator:
> > > >
> > > > A B A=>B
> > > > T T T
> > > > T F F
> > > > F T T
> > > > F F T