Two Pathological Quantifier Constructs to Avoid

[Dan Christensen]

THEOREM

For proposition P and any set X, we have:

EXIST(a):[a in X => P] is always true

ALL(a):[a in X & P] is always false

PROOF

Lemma: http://dcproof.com/UniversalSet.htm (28 lines)

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

Suppose...

2. Set(x)
Premise

3. Set(x) => EXIST(b):~b in x
U Spec, 1

4. EXIST(b):~b in x
Detach, 3, 2

5. ~y in x
E Spec, 4

6. ~y in x | P
Arb Or, 5

7. ~~y in x => P
Imply-Or, 6

8. y in x => P
Rem DNeg, 7

9. ALL(x):[Set(x) => EXIST(a):[a in x => P]]
Conclusion, 2

******************************************************************

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

2. Set(x)
Premise

3. Set(x) => EXIST(b):~b in x
U Spec, 1

4. EXIST(b):~b in x
Detach, 3, 2

5. ~y in x
E Spec, 4

6. ~y in x | ~P
Arb Or, 5

7. ~[~~y in x & ~~P]
DeMorgan, 6

8. ~[y in x & ~~P]
Rem DNeg, 7

9. ~[y in x & P]
Rem DNeg, 8

10. ALL(x):[Set(x) => EXIST(a):~[a in x & P]]
4 Conclusion, 2

11. ALL(x):[Set(x) => ~ALL(a):~~[a in x & P]]
Quant, 10

12. ALL(x):[Set(x) => ~ALL(a):[a in x & P]]
Rem DNeg, 11

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]

HTML format:

https://www.dcproof.com/ExistentialQuantifierOnConditionalTrue.htm
https://www.dcproof.com/UniversalQuantifierOnConditionalFalse.htm

[Graham Cooper]

On Monday, April 24, 2023 at 5:47:39 AM UTC+10, Dan Christensen wrote:
> THEOREM
>
> For proposition P and any set X, we have:
>
> EXIST(a):[a in X => P] is always true
>
> ALL(a):[a in X & P] is always false

sounds like rubish particular to DCProooth

DCProof is old hat you dont need quantifiers


A(x) A(y) EXIST(z) ...

fun X Y skolem1( X Y ) ....


Elim of quantifiers is prenex normal form

[Mostowski Collapse]

So you just proved:

i) EXIST(x):~P(x) => EXIST(x):[P(x) => Q]

ii) EXIST(x):~P(x) => ~ALL(x):[P(x) & Q]

Woa! That must be the biggest invention since sliced bread.
Quite trivial too prove, isn't it?
Wolfgang Schwartz tree tool can do it in a blink:

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

∃x¬Px → ¬∀x(Px∧Q) is valid.
https://www.umsu.de/trees/#~7x~3Px~5~3~6x%28Px~1Q%29

[Mostowski Collapse]

Is it intuitionistically valid, or a classical theorem? Depends
maybe also a little bit how quantifier are formulated. You
use Rem DNeg. Is this even necessary?

Here is another automated proof, its longer than
the proof by Wolfgang Schwartz which is a semantic
tableaux proof. Its also longer than your proof as

well. But I guess it can be shortened? Will post a
shorter proof if I have time and if I find one. But
meanwhile here it is unabridged:

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

1 ¬ ∀x:p(x)
Premise
2 ∀x: ¬ (p(x) ⊃ q)
Premise
3 ¬p(v)
Premise
4 ¬ (p(v) ⊃ q)
U Spec 2
5 p(v)
Premise
6 ¬q
Premise
7 ⊥
Detach 3,5
8 q
▲ Reductio 6,7
9 p(v) ⊃ q
▲ Conclusion 5,8
10 ⊥
Detach 4,9
11 p(v)
▲ Reductio 3,10
12 ∀x:p(x)
U Gen 11
13 ⊥
Detach 1,12
14 ¬ ∀x: ¬ (p(x) ⊃ q)
▲ Conclusion 2,13
15 ¬ ∀x:p(x) ⊃ ¬ ∀x: ¬ (p(x) ⊃ q)
▲ Conclusion 1,14

[Mostowski Collapse]

The theorems don't show anything pathological.
Thats a halucination of yours, and a rather moronic
marketing pitch. They can be derived from this theorem,

which you find in every school boy or girl
paint by numbers logic book:

∀x(Px ∧ Qx) → ∀xPx is valid.
https://www.umsu.de/trees/#~6x(Px~1Qx)~5~6xQx

Examples:
If every moon is green and of cheese then every moon is green.
if every prime number > 2 is odd and positive then every prime number > 2 is odd.

Means we can even strengthen the theorems,
into these two theorems, they work also:

i) EXIST(x):~P(x) => EXIST(x):[P(x) => Q(x)]

ii) EXIST(x):~P(x) => ~ALL(x):[P(x) & Q(x)]

Yes, that works also:

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

∃x¬Px → ¬∀x(Px ∧ Qx) is valid.
https://www.umsu.de/trees/#~7x~3Px~5~3~6x(Px~1Qx)

[Jim Burns]

Re: Two Pathological Quantifier Constructs to Avoid

Is what you mean by
"pathological construct"
something like
"does not mean what one thinks it does"
?

∃a: a ∈ X ∧ P(a)
and
∀a: a ∉ X ∨ P(a)
are
useful for making claims intended to
apply only in set X.
How they work is that, not-in set X
the truth or falsity of P is irrelevant.

∃a: a ∉ X ∨ P(a)
and
∀a: a ∈ X ∧ P(a)
are
not those claims, and they aren't
useful for making claims intended to
apply only in set X.

That's not what I would call "pathological"
but no one asked me.

Yes,
if, by "pathological", you mean
"not useful" in that way,
then I agree.

On 4/23/2023 3:47 PM, Dan Christensen wrote:

> THEOREM
>
> For proposition P and any set X, we have:
>
> EXIST(a):[a in X => P] is always true
>
> ALL(a):[a in X & P] is always false
>
> PROOF
>
> Lemma: http://dcproof.com/UniversalSet.htm (28 lines)
>
> 1. ALL(a):[Set(a) => EXIST(b):~b in a]
> Axiom

On the other hand,
a universal set exists in other theories.

For example,
there's Plural Quantification PQ
https://plato.stanford.edu/entries/plural-quant/

I have been using PQ. Its axioms,
Comprehension and Extensionality, are
exceptionally short and clear.
This is a godsend for the project on which
I've been working, re-composing our
mathematical logic as a series of haiku
or limericks.

We avoid the pathological set of
non-self-containing sets by managing
the domain(s) of discussion a bit
differently.

There's a domain of individuals,
with quantifiers ∃ ∀
a domain of sets with ∃² ∀²
of sets of sets ∃³ ∀³
etc. ∃⁴ ∀⁴ ∃⁵ ∀⁵ ...

Define R := {S: S ∉ S}
In PQ, R ∈ R is neither true nor false
R ∈ R is a syntax error.

In PQ, there is a universal set
By Comprehension,
for each predicate P(a) on individuals,
there is a set {a: P(a)} of all and only
those individuals for which it's true.
For a universally true predicate ⊤
there is a universal set {a: ⊤} of
individuals, a universal set ²{A: ⊤}²
of sets, ...

> EXIST(a):[a in X => P] is always true
>
> ALL(a):[a in X & P] is always false

For X := {a: ⊤} and P(a) :⇔ ¬⊤
∃a: a ∉ X ∨ P(a)
is false

For X = {a: ⊤} and P(a) :⇔ ⊤
∀a: a ∈ X ∧ P(a)
is true

[Dan Christensen]

> So you just proved:
>
> i) EXIST(x):~P(x) => EXIST(x):[P(x) => Q]
>
> ii) EXIST(x):~P(x) => ~ALL(x):[P(x) & Q]
>

Even easier to prove! If, however, your domain of quantification is a set (usually the case in mathematics), then there is no need for that extra axiom.

Though, for any "real-life" predicate P, it is quite reasonable to assume EXIST(x):~P(x) e.g. EXIST(x):~Dog(x)

I bring this up only as a kind of cautionary tale. In any "real-life" application, if you come up with quantification statements of the forms exhibited above, you should probably reconsider your initial assumptions. Maybe your implication should be a conjunction, or your conjunction should be a conditional.

[Dan Christensen]

Something like that. I present these examples as cautionary tales. If they arise in "real-life" applications, alarm bells should go off. You would most likely have made a mistake.

> On 4/23/2023 3:47 PM, Dan Christensen wrote:
>
> > THEOREM
> >
> > For proposition P and any set X, we have:
> >
> > EXIST(a):[a in X => P] is always true
> >
> > ALL(a):[a in X & P] is always false
> >
> > PROOF
> >
> > Lemma: http://dcproof.com/UniversalSet.htm (28 lines)
> >
> > 1. ALL(a):[Set(a) => EXIST(b):~b in a]
> > Axiom

> On the other hand,
> a universal set exists in other theories.
>

[snip]

In ordinary set theory, this is not the case. If you want to use more exotic set theories in "real-life" applications, you would probably not want to introduce a set the contains everything. For every set that you introduce, you may then also want to introduce an axiom of the form EXIST(a): a not in set X.

[Mostowski Collapse]

Dan Christensen wrote:
> quantification statements of the forms exhibited

Is this the nonsense take-away for your students?
What do you want to establish a new form of WFF?
Are you planning a new form of WFF for your tool?

https://en.wikipedia.org/wiki/Well-formed_formula

The Drinker Paradox has this form, which
you critizes as pathological:

EXIST(x):[P(x) => Q]

But without the premisse EXIST(x):~P(x).
Take the Drinker Paradox, it has this form

EXIST(x):[D(x) => ALL(x):D(x)]

via P=D and Q=ALL(x):D(x). But no assumption
EXIST(x):~D(x), its nevertheless provable:

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

Its a perfectly valid theorem, an Smullyan showed
its english phrasing. I don't think its something
pathological, maybe perplexing, but not pathological.

Of course extremly preplexing for a moron like
Dan Christensen who runs around with a proof tool,
where one would need an extra assumption

EXIST(x):x=x for the non-empty discourse. Like
after a couple of months, Dan Christensen is still
chewing the Drinker Paradox. But unfortunately

from his crank attitude of pathological formulas.

LoL

[Mostowski Collapse]

The linguistic problem here you write "form":

> quantification statements of the forms exhibited

But when you prove a "form", you basically prove:

EXIST(x):[P(x) => Q]

and then you discuss this "form". But you neglected
that you had also an axiom EXIST(x):~P(x). Its not
some sort of necessary condition for the "form"

to be "pathological true". If it were a necessary condition
you would be able to prove the converse:

EXIST(x):[P(x) => Q] => EXIST(x):~P(x)

But you cannot prove the converse. The converse
has a counter model:

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

The Drinker Paradox is a nice example that shows
that EXIST(x):~P(x) is not a necessary condtion to
make EXIST(x):[P(x) => Q] generally valid. Because

the Drinker Paradox doesn't have this assumption,
but is nevertheless generally valid.

[Mostowski Collapse]

I don't believe that there is any countionary tale behind
this "form", in the sense that it should be avoided:

EXIST(x):[P(x) => Q]

The Drinker Paradox is a nice example which shows
that this form can have a very interesting logical
content. Its not very difficult to take the Drinker Paradox:

EXIST(x):[D(x) => ALL(x):D(x)]

And bring it into MiniScope form, via A => B is
the same as ~A | B classically, and then shift
the EXIST(x) into the left branch of the disjunction:

EXIST(x):~D(x) | ALL(x):D(x)

Now use deMorgan for universal quantifier:

EXIST(x):~D(x) | ~EXIST(x):~D(x)

So the Drinker Paradox is becomes nothing else
than an instance of LEM.

Law of excluded middle
https://en.wikipedia.org/wiki/Law_of_excluded_middle

[Dan Christensen]

On Monday, April 24, 2023 at 12:38:36 PM UTC-4, Mostowski Collapse wrote:
> The linguistic problem here you write "form":
> > quantification statements of the forms exhibited
> But when you prove a "form", you basically prove:
>
> EXIST(x):[P(x) => Q]
>
> and then you discuss this "form". But you neglected
> that you had also an axiom EXIST(x):~P(x).

[snip]

I have not yet presented of a formal proof of this. Here it is:

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

2. ~P(x)
E Spec, 1

3. ~P(x) | Q
Arb Or, 2

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

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

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

I hope this helps.

[Dan Christensen]

On Monday, April 24, 2023 at 12:45:56 PM UTC-4, Mostowski Collapse wrote:
> I don't believe that there is any countionary tale behind
> this "form", in the sense that it should be avoided:
>
> EXIST(x):[P(x) => Q]
>

[snip]

The important point here is that if EXIST(a): ~P(a), then Q could be any, even nonsensical, possibly false proposition. See my previous posting here.

[Mostowski Collapse]

Trick question, quizz for dummies. Is EXIST(a):~P(a)
always needed to prove EXIST(x):[P(x) => Q] ? Or could

a formula of the form EXIST(x):[P(x) => Q] also be
generally valid without the premis EXIST(a):~P(a) ?

Dan Christensen schrieb:

[Jim Burns]

On 4/24/2023 12:23 PM, Dan Christensen wrote:
> On Monday, April 24, 2023
> at 11:07:15 AM UTC-4, Jim Burns wrote:

>> Yes,
>> if, by "pathological", you mean
>> "not useful" in that way,
>> then I agree.
>
> Something like that.
> I present these examples as cautionary tales.
> If they arise in "real-life" applications,
> alarm bells should go off.
> You would most likely have made a mistake.

Yesbut,
that's an error of
_saying something unintended_
which is important, but isn't logic.

>> On the other hand,
>> a universal set exists in other theories.

> In ordinary set theory, this is not the case.

Which set theory one is using
is important, but isn't logic.

> If you want to use more exotic set
> theories in "real-life" applications,

No.
My reason for using PQ is that
it's _less_ exotic.
Less usual. Less powerful, maybe?
But clearly less exotic.

Comprehension:
∃²x₂,∀y: y ∈ x₂ ⟺ P(y)
∃³x₃,∀²y₂: y₂ ∈ x₃ ⟺ P(y₂)
∃⁴x₄,∀³y₃: y₃ ∈ x₄ ⟺ P(y₃)
...

You might find it interesting to see
which set theory Gödel uses in
his 1931 paper on formally undecidable
propositions.

> you would probably not want to
> introduce a set the contains everything.
> For every set that you introduce,
> you may then also want to introduce
> an axiom of the form
> EXIST(a): a not in set X.

Thank you for your interest in my project.
No, I do not want to do that.

[Mostowski Collapse]

Your plural quantifiers were a very short love affair it seems.
You already changed topcis into something else. Gödel
had variables with indices showing their type level.

But I don't think Dan Christensen has some problems
with type levels. He uses Set(x), and then if he writes
set membership y e x, he is quite strict to avoid some

telescoping. You can say his usage of set theory is
ultra boring. I have probably not yet seen an instance
where he would use z e y and y e x, thats somehow

beyond his "real-life"? Maybe he thinks such chains
also pathological. Anyway, I am hoping that Rossy
Boy can contribute some limerics and haikus, to

brighten up the day, since its monday.

[Mostowski Collapse]

Maybe Dan Christensen is so obsessed with Russells
Paradox and EXIST(x):~P(x) in the incarnation of a
consequence of Russells Paradox, because

he is trapped in a lower echolon of logic. Kind of
trapped in a infinite loop that runs in circles in
a closed cavern deep under the ground, and

he cannot go to higher levels. Thats maybe the
reason that we never find z e y and y e x and
that function spaces where such a pain. Whereas

set theorists clearly have a rich domain of discourse
before their eyes which various stratification levels,
exemplified in von Neumann hierarchy of sets.

Or if they abandon set theory, they have just Gödel
type level indices which must have been an institution
at the time Gödel wrote his paper. A long forgotten

mathematical logic institution? Not at all, it comes all
back in the form of Coq, which has even a little Quines
new foundation it it? Their stratification is generic.

"It may come as a surprise to you that there isn't a single
Type in Coq. Instead there is an infinite hierarchy of types
Type@{0}, Type@{1}, Type@{2}… with Type@{i} : Type@{j} if i < j.
This means that every universe (Type@{j}) contains every
universe with a smaller level as an element."

It will show the indices via this Coq command?

Set Printing Universes: In Coq top-level
"View" > "Display universe levels": In Coq IDE

Didn't try yet. Could be fun!

[Mostowski Collapse]

Oops forgot the link:

Set Printing Universes has no effect
https://stackoverflow.com/a/48607878

Type : Type in Coq
https://stackoverflow.com/a/54073247

Woa! Everybody now juggling with different
sub-universe spanning infinities...

LoL

The logic component of Coq is Gallina, the specification
language of Coq. It allows developing mathematical theories
and to prove specifications of programs. The theories are
built from axioms, hypotheses, parameters, lemmas,
theorems and definitions of constants, functions, predicates and sets.

Built on top of Coq CIC? In Coq, logical objects are typed
o ensure their logical correctness. The rules implemented
by the typing algorithm are described in Chapter Calculus
of Inductive Constructions. More about Types from
Adam Chlipala, author of Certified Programming:

http://adam.chlipala.net/cpdt/html/Universes.html

[Dan Christensen]

On Monday, April 24, 2023 at 3:19:41 PM UTC-4, Mostowski Collapse wrote:
> Maybe Dan Christensen is so obsessed with Russells
> Paradox and EXIST(x):~P(x) in the incarnation of a
> consequence of Russells Paradox, because
>
> he is trapped in a lower echolon of logic.

"Trapped" along with what seems to be the vast majority of working mathematicians? I can live with that.

[Mostowski Collapse]

Ok, I thought so, you are indeed obsessed. Just like WM
is facinated by dark numbers, you are facinated by the dark
elements that pop up for each set.

So when ever you have a set x, by this theorem:

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

There pops up some dark element y, with ~y e x. So
although there is no universal set. There is universal
darkness. For every set x, there is at least one companion

y from the dark elements, an element that looks over
your shoulder x, a good angle or rather the devil that drives
you to prove pathological formulas such as:

ALL(x):[Set(x) => ~ALL(a):[a in x & P]]

So logic shows us the forbidden fruits, and we are not
allowed to touch them, otherwise we have to leave
the paradies and earn the anger of Gods.

LMAO!

[Mostowski Collapse]

In working mathematicians text books you cannot prove:

... => EXIST(b):~b in a ...

Whats the type of b? Respectively the set of b?
It would not be well formed, because EXIST(b) is "pathological"
to use your own words. So you start with "pathological"

and you get "pathological". What do you expect? In
working mathematician text books, living in the lower
echolon of logic, you would need to specify some

set c where b belongs to:

... => EXIST(b):[b in c & ~b in a]

Good Luck with deriving that from Russells Paradox.

LoL

[Dan Christensen]

On Monday, April 24, 2023 at 3:49:21 PM UTC-4, Mostowski Collapse wrote:

[snip]

> So when ever you have a set x, by this theorem:
> ALL(a):[Set(a) => EXIST(b):~b in a]

Or equivalently: ~EXIST(a):[Set(a) & ALL(b):b in a]

Look familiar? Just ordinary set theory, Mr. Collapse.

Again, see: http://dcproof.com/UniversalSet.htm

[Mostowski Collapse]

You start with something pathological again:

~ ... & ALL(b):[b in a]

Whats the type of b? Respectively the set of b?

It would not be well formed, because ALL(b) is "pathological"

to use your own words. So you start with "pathological"

and you get "pathological". What do you expect? In
working mathematician text books, living in the lower
echolon of logic, you would need to specify some

set c where b belongs to:

~ ... & ALL(b):[b in c => b in a]

Good Luck with deriving that from Russells Paradox.

LoL

[Dan Christensen]

On Monday, April 24, 2023 at 4:05:02 PM UTC-4, Mostowski Collapse wrote:
> You start with something pathological again:
>
> ~ ... & ALL(b):[b in a]
> Whats the type of b? Respectively the set of b?
> It would not be well formed, because ALL(b) is "pathological"
> to use your own words. So you start with "pathological"
>
> and you get "pathological".

You are making no sense here, Mr. Collapse. Relax. Take a deep breath and try again. More slowly this time.

Dan

[Jim Burns]

On 4/24/2023 3:00 PM, Mostowski Collapse wrote:

> Your plural quantifiers were
> a very short love affair it seems.

!
Not at all!

I just find it easier to explain
pluralities as typed sets.
Sets are pluralities of individuals.
Sets of sets are pluralities of sets.
etc.

I've extended
https://plato.stanford.edu/entries/plural-quant/
somewhat, but not unreasonably, I think.

I've also pretty-much dumped the
discussion of the ontological status of
pluralities. I can't imagine someone being
_less_ satisfied with pluralities than
they are with sets, so I'm not highly
motivated to pursue that. So, sue me.

I mention Gödel because, well, just look
at his set theory! It's sets, sets of sets,
sets of sets of sets, ... with Comprehension
and Extensionality.

I feel that a reference to Gödel is
an appropriate response to accusations of
"exotickness".

[Mostowski Collapse]

Here you derive a pathological sentence:
http://dcproof.com/UniversalSet.htm (28 lines)

~EXIST(s):[Set(s) & ALL(a):aes]
or equivalently...
ALL(s):[Set(s) => EXIST(a):~a e s]

They are pathological because you don't use
set bounded quantifier formulas:

ALL(a):[a e c => ...]
EXIST(a):[a e c & ...]

Try proving the with set bounded quantifier
formulas as the theorem. Its impossible, right?

[Mostowski Collapse]

So you are lamenting garbage in garbage out.
You start with a pathological sentence (the axiom
representing the theorem UniversalSet) and

you get a pathological sentences (the theorems
ExistentialQuantifierOnConditionalTrue and
UniversalQuantifierOnConditionalFalse).

Why lament? You left your lower echolon, and
banged your head since it was raining ashes.
The art is of course how to get to higher order

logic, without banging your head? Actually
Hermann Klaus Hugo Weyl (9 November 1885 –
8 December 1955) featured some neat ideas,

he wrote "Das Kontinuum" identifying much
more pathological formulas, and going even
some caverns deeper, and nevertheless

obtaining real analysis!

Weyl’s Predicative Classical Mathematics as a
Logic-Enriched Type Theory
https://www.cs.rhul.ac.uk/~zhaohui/weylFinal.pdf

[Dan Christensen]

On Monday, April 24, 2023 at 4:25:15 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 24. April 2023 um 22:15:00 UTC+2:
> > On Monday, April 24, 2023 at 4:05:02 PM UTC-4, Mostowski Collapse wrote:
> > > You start with something pathological again:
> > >
> > > ~ ... & ALL(b):[b in a]
> > > Whats the type of b? Respectively the set of b?
> > > It would not be well formed, because ALL(b) is "pathological"
> > > to use your own words. So you start with "pathological"
> > >
> > > and you get "pathological".
> > You are making no sense here, Mr. Collapse. Relax. Take a deep breath and try again. More slowly this time.
> >

> Here you derive a pathological sentence:
> http://dcproof.com/UniversalSet.htm (28 lines)
>
> ~EXIST(s):[Set(s) & ALL(a):aes]

You are confused. There is nothing wrong with an existential quantifier on a conjunction.

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

Likewise, there is nothing wrong with a universal quantifier on a conditional.

> They are pathological because you don't use
> set bounded quantifier formulas:
>
> ALL(a):[a e c => ...]
> EXIST(a):[a e c & ...]
>

You missed the point, Mr. Collapse. Do pay attention. The following are, in some sense, "pathological":

For any set X and proposition P:

EXIST(a):[a in X => P]

ALL(a):[a in X & P]

For any proposition Q and predicate P such that EXIST(a):~P(a):

EXIST(a):[P(a) => Q]
ALL(a):[P(a) & Q]

[Mostowski Collapse]

Its relatively easy to demonstrate that you are a liar if
you would claim that your input is not already pathological.

/* Dan Christensen claims this not pathological */

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

http://dcproof.com/UniversalSet.htm

Because you yourself proved it pathological here:

/* Dan Christensen claims this pathological */
ALL(x):[Set(x) => ~ALL(a):[a e x & P]]
https://www.dcproof.com/UniversalQuantifierOnConditionalFalse.htm

Just use P=True, what do you get? I get the following

... => ~ALL(a):[a e x & T] ...

Which is equivalent to:

... => ~ALL(a):[a e x] ...

Which is equivalent to:

... => EXIST(a):[~a e x] ...

Dan Christencen is a liar verified.
Q.E.D.

[Dan Christensen]

On Monday, April 24, 2023 at 4:53:06 PM UTC-4, Mostowski Collapse wrote:
> Its relatively easy to demonstrate that you are a liar if
> you would claim that your input is not already pathological.
>
> /* Dan Christensen claims this not pathological */
> ALL(s):[Set(s) => EXIST(a):~a e s]

I made no such claim. This just says something is excluded from every set, i.e. there is no universal set in ordinary set theory. We have a universal quantifier on a conditional--not a problem. It is universal quantifiers on conjunctions that can be pathological.

> http://dcproof.com/UniversalSet.htm
>
> Because you yourself proved it pathological here:
>
> /* Dan Christensen claims this pathological */
> ALL(x):[Set(x) => ~ALL(a):[a e x & P]]

Here we have a universal quantifier on a conjunction: ALL(a):[a in x & P] where x is a set. It will be false for ANY proposition P, be it true or false. In this sense ALL(a):[a in x & P] is pathological. Get it?

> https://www.dcproof.com/UniversalQuantifierOnConditionalFalse.htm
>
[snip]

I hope this helps.

[Mostowski Collapse]

Yes agreed this if this is pathological, where P is arbitrarily plugable:

> 1) Your Theorem

> ALL(x):[Set(x) => ~ALL(a):[a e x & P]]

> https://www.dcproof.com/UniversalQuantifierOnConditionalFalse.htm

Then this is also pathological, what you used as an axiom:

> 2) Your Axiom

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

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

So you have shown garbage in, garbage out.
You have shown a "pathological" formula leads to a "pathological
formula, if we accept your terminology of "pathological".

Hint: Proof sketch. Just plugin P=True into 1) and you get 2).

[Mostowski Collapse]

But its easier to use your other theorem, to show the state
of affaire. Yes I agree also that if this pathological,

where P is arbitrarily plugable:

> 3) Your Theorem II
> ALL(a):[Set(x) => EXIST(a):[a e x => P]]
> https://www.dcproof.com/ExistentialQuantifierOnConditionalTrue.htm

Then we must conclude that this is also pathological,

what you used as an axiom:

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

So you have shown garbage in, garbage out.
You have shown a "pathological" formula leads to a "pathological
formula, if we accept your terminology of "pathological".

Hint: Proof sketch. Just plugin P=False into 3) and you get 2).

[Mostowski Collapse]

Oh, I forgot, you don't have Falsum in DC Poop. Thats maybe
why you don't see that EXIST(a):~a e s is a special case
of EXIST(a):[a e s => P] with P=False?

Well you can prove in DC Poop:

EXIST(a):~a e s <=> EXIST(a):[a e s => Q & ~Q]

Right? Yes or No? Or is this over your head?

∃a¬Eas ↔ ∃a(Eas → (q∧¬q)) is valid.
https://www.umsu.de/trees/#~7a~3Eas~4~7a(Eas~5q~1~3q)

This is very very elementary propositional logic ~A <=> A -> False.

[Mostowski Collapse]

In higher order logic we have even?
EXIST(a):~a e s <=> ALL(P):EXIST(a):[a e s => P]

Beause the above is equivalent to, a does not appear in P?
EXIST(a):~a e s <=> ALL(P):[ALL(a):a e s => P]

Which is propositional equivalent to:
EXIST(a):~a e s <=> ~ALL(a):a e s

Which is Ok because of deMogan for quantifiers.
The propositional core is provable in Coq:

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

If I use the Print command, which I just learnt from Julio, I get:

ex1 =
fun Q : Prop =>
conj
(fun (H : ~ Q) (P : Prop) (H0 : Q) =>
let H1 : False := H H0 in False_ind P H1)
(fun H : forall P : Prop, Q -> P =>
(fun H0 : Q => let H1 : Q -> False := H False in H1 H0) : ~ Q)
: forall Q : Prop, ~ Q <-> (forall P : Prop, Q -> P)

Arguments ex1 Q%type_scope

Didn't try with the existential quantifier interleaved yet in Coq.
But Coq shines here, since it can also provide such higher
order reasoning. The propositional core is still tame, more like

QSAT, but nevertheless, quite impressive what Coq can do.

[Dan Christensen]

On Monday, April 24, 2023 at 6:42:44 PM UTC-4, Mostowski Collapse wrote:
> Yes agreed this if this is pathological, where P is arbitrarily plugable:
>
> > 1) Your Theorem
> > ALL(x):[Set(x) => ~ALL(a):[a e x & P]]

Here we have a universal quantifier on a conjunction, and even if you substitute "~P " for "P", ALL(a)[a in x & ~P] will still be false.

> > https://www.dcproof.com/UniversalQuantifierOnConditionalFalse.htm
>

> Then this is also pathological, what you used as an axiom:
>

Still wrong.

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

In other words, every set excludes something, which we know is always true.

If we substitute "~EXIST(a):~a e s]" for "EXIST(a):~a e s]" we would have:

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

In other words, every set includes everything, which we know to be false.

So, ALL(s):[Set(s) => EXIST(a):~a e s] is NOT pathological in the sense I am using the word.

[Dan Christensen]

On Monday, April 24, 2023 at 6:58:01 PM UTC-4, Mostowski Collapse wrote:
> Oh, I forgot, you don't have Falsum in DC Proof.

I don't know why you would want to, but it's easy to create the equivalent of your precious "falsum" symbol. Just Introduce proposition T as an axiom at the beginning of your proof.

1. T
Axiom

(Doesn't have to be "T". Any string of letters of any length beginning with an uppercase letter would do.)

Then your "falsum" symbol would be be ~T.

> Thats maybe
> why you don't see that EXIST(a):~a e s is a special case
> of EXIST(a):[a e s => P] with P=False?
>

Normally, to indicate that P is tru, we would simply introduce the premise:

2. P
Premise

To indicate that P is false:

2. ~P
Premise

But, if you insist, for P is true, we could introduce:

2. P <=> T
Premise

For P is false:

2. P <=> ~T
Premise

It would, however, make for much longer proofs. I really can't recommend it.

[Dan Christensen]

On Monday, April 24, 2023 at 7:26:14 PM UTC-4, Mostowski Collapse wrote:
> In higher order logic we have even?
> EXIST(a):~a e s <=> ALL(P):EXIST(a):[a e s => P]
>

You just won't see that in many math textbooks. It simply isn't necessary in most proofs. It would only confuse students. Maybe you can implement it YOUR theorem prover. BTW how is that coming along?

[Mostowski Collapse]

Really. Why not? Its very sad that you have no grasp of
this simple identity, which is behind what you presented
(nothing to do with Sets or Russell):

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

How did you resolve Epimenides' Paradox?

[Mostowski Collapse]

You should really start a legislative initiative to rename "negation"
into "pathology", like the guy who wanted to make π equal 3.4 by law.

Subsequently these Wikipedia articles will have to be deleted, when
the law, the Dan Christensen Logic article, comes into force:

https://de.wikipedia.org/wiki/Ex_falso_quodlibet

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

[Dan Christensen]

On Monday, April 24, 2023 at 9:42:40 PM UTC-4, Mostowski Collapse wrote:
> Really. Why not? Its very sad that you have no grasp of
> this simple identity, which is behind what you presented
> (nothing to do with Sets or Russell):
>
> ~A <=> ∀B (A => B)
>
> How did you resolve Epimenides' Paradox?

See the thread: "Resolution of Epimenides' Paradox (in DC Proof)"

Dan

[Mostowski Collapse]

You can also play around with different scopes.
This here should also work:

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

Some authors go even that far to define Falsum
via ∀B B. This is even provable in Coq:

Lemma ex2: False <-> (forall (P:Prop), P).

intuition.
specialize (H False).
apply H.

Qed.

You might also want to check Dag Prawitz, 1965
Natural deduction : a proof-theoretical study
Page 67: Definability of False in Intuitionistic Logic
https://archive.org/details/naturaldeduction0000praw/page/66/mode/2up

So its even intuitionistically valid in 2nd Order.
Dag Prawitz makes also the remark "In contrast
to the situation for first order logic").

[Ross Finlayson]

There are lots of adages which are sorts of parables or morals,
there's for example:

"If you don't have something nice to say, it's better to say nothing at all".

In the adversarial, that might come across as "if you don't have something
destructive to add, do not be providing extra rope".

Here though the tone of "these constructs are dangerous because they
are not resulting truth, which is the only nice thing there is to say", is
coming across much better than "logic proves fallacies", which would
be oxymoronic, i.e. a contradiction in terms, i.e. contradictory to
"logic does not prove fallacies, only illustrating how fallacies are formed".

So if it helps keep people from getting their ass beat to death and the resulting
jawbone being used to slay a ton of infidels, because "material implication is wrong",
I'm sort of for it.

Also, for eliminating "ex falso quodlibet", goes a long way, to that that means "eliminate
ex falso quodlibet by detecting and removing it", not "forget how to disprove fallacies",
though often enough "forget about it" is sage.


Burse is still a braying, lolling, ass, but, it's much better that you get into why
enthymemes' discovery invalidates closures, than, compounding stupid.



About whether "shaving simply isn't reflexive a verb" for example,
illustrates the dialectic about types, and their hierarchies, and inverting
them, because "inverses are general", that "inverses are diverse", structurally,
and constructivistically.

[Mostowski Collapse]

Did a Herpes Blister explode in your Face?

Ross Finlayson schrieb am Dienstag, 25. April 2023 um 17:48:40 UTC+2:
> .. gibberish ..

[Dan Christensen]

On Sunday, April 23, 2023 at 3:47:39 PM UTC-4, Dan Christensen wrote:
> THEOREM
>
> For proposition P and any set X, we have:
>
> EXIST(a):[a in X => P] is always true
>
> ALL(a):[a in X & P] is always false
>
[snip]

Both results will hold for ANY set X and ANY proposition P regardless of its truth value. We could even substitute "~P" for "P" and they would still hold. It is in this sense that constructs such as EXIST(a):[a in X => P] and ALL(a):[a in X & P] might be termed "pathological."

ALL(x):[Set(x) => EXIST(a):[a in x => P]]
Proof: https://www.dcproof.com/ExistentialQuantifierOnConditionalTrue.htm

ALL(x):[Set(x) => ~ALL(a):[a in x & P]]
https://www.dcproof.com/UniversalQuantifierOnConditionalFalse.htm

[Dan Christensen]

On Tuesday, April 25, 2023 at 5:09:01 PM UTC-4, Dan Christensen wrote:
> On Sunday, April 23, 2023 at 3:47:39 PM UTC-4, Dan Christensen wrote:
> > THEOREM
> >
> > For proposition P and any set X, we have:
> >
> > EXIST(a):[a in X => P] is always true
> >
> > ALL(a):[a in X & P] is always false
> >
> [snip]
>
> Both results will hold for ANY set X and ANY proposition P regardless of its truth value. We could even substitute "~P" for "P" and they would still hold. It is in this sense that constructs such as EXIST(a):[a in X => P] and ALL(a):[a in X & P] might be termed "pathological."
>
> ALL(x):[Set(x) => EXIST(a):[a in x => P]]
> Proof: https://www.dcproof.com/ExistentialQuantifierOnConditionalTrue.htm
>

Applied to the so-called Drinkers' Paradox, with x = the set of people drinking in a pub, and P = the proposition that everyone in the pub is drinking, it must be the case that, there exists someone who, if he or she is drinking in the pub, then it must be TRUE that everyone in the pub is drinking. But it must ALSO be the case that, there exists someone who, if he or she is drinking in the pub, then it must be FALSE that everyone in the pub is drinking.

[Ross Finlayson]

Yours?

[Ross Finlayson]

I really don't know and _don't want to know_, all your problems, and I hope it isn't
that you have micro-clots all over the place from miRNA damage.

I hope it isn't, because, that would be very bad for the half of the population that
got the shot.

You did work very hard to sell it, that and your crypto offerings, I don't keep track
of that, either, so if you were right they must be doing very well.

I don't keep track of that kind of thing, but, there are some rumblings that there
were big mistakes made and lots of people got ripped off tons of money, ....

Too personal?

[Mostowski Collapse]

Ever heard in your life about proof by cases? Your halucinations
are a little bit pathological. The Drinker Paradox, when modelled
with a pub, doens't have one of these forms:

EXIST(a):[a in X => P]

ALL(a):[a in X & P]

If you model the Drinker Paradox with a pub, you get this
formula here, where you cannot apply your
halucinations of pathological:

EXIST(a):[P(a) & (D(a) => ALL(b):[P(b) => D(p)]]

For a non-empty pub, EXIST(a):P(a), the drinker
Paradox is generally valid, irrespective of whether
everybody is drinking or not, i.e. whether

ALL(b):[P(b) => D(p)] is true or not:

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

The word "valid" means satisfied under any circumstance,
i.e. the Drinker Formula ∃x(Px ∧ (Dx → ∀y(Py → Dy)) is satisfied
in model where ∀y(Py → Dy) is true, and it is satisfied in a

model where ∀y(Py → Dy) is false. Provided that ∃xPx
is satisfied. Because of this coverage of two stituations by
the Drinker Formula a usual proof proceeds by proof by cases.

[Mostowski Collapse]

You can model the pub also as a set, make it smaller
than what a predicate would give. The same result.
Under the assumption EXIST(a):a e P, this is generally valid:

EXIST(a):[a e P & (D(a) => ALL(b):[b e P => D(p)]]

Thats what Wikipedia sells as the Drinker Paradox:

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

Again it doesn't have your pathological form. And
its provable by cases, since the above formula becomes
satisfiable irrespective whether ∀y in P D(y) is true

or false. You can also prove it with Wolfgang Schartz tool:

∃xExp → ∃x(Exp ∧ (Dx → ∀y(Eyp → Dy))) is valid.
https://www.umsu.de/trees/#~7xExp~5~7x(Exp~1(Dx~5~6y(Eyp~5Dy)))

In the above Exp respevtively Eyp is some encoding
for x∈p respectively y∈p. Unfortunately Wolfgang Schartz tool
doesn't allow infix notation for set membership.

But I guess you should be flexible enough in your mind
to run through the example with Exp respevtively Eyp
instead of x∈p respectively y∈p. You don't have

Alzheimer as Archimedes Plutonium does?

[Mostowski Collapse]

Whats wrong fruitcake? On your period again?

Ross Finlayson schrieb am Mittwoch, 26. April 2023 um 01:07:30 UTC+2:
> ... gibberish ...

[Mostowski Collapse]

Instead of wasting your time, with the Drinker Paradox,
which seems to be quite over your head, you could
try to solve the below problem.

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

It shows that in natural language there are expressions
which are not representable in first order logic (FOL)
and also not representable in DC Poop.

For pathological you use a natural language expression:

On Sunday, April 23, 2023 at 3:47:39 PM UTC-4, Dan Christensen wrote:
> Both results will hold for ANY set X and ANY
proposition P regardless of its truth value.

https://groups.google.com/g/sci.logic/c/Q8FsBsKloo4/m/4VO2_AdxAwAJ

How do you want to express "ANY proposition P" in 1st Order?
To make your statement about "pathology" formalizable
you need a language that is at least 2nd Order.

Dan Christensen schrieb am Dienstag, 25. April 2023 um 23:42:47 UTC+2:

[Mostowski Collapse]

In a 2nd Order language you can formulate it. And your
blind spot about one of the directions <= might go away.
But then it becomes something that isn't "pathological"

at all. It just some observation about Falsum respectively
negation. For Falsum you can consider:

f <=> ∀B B

This is again provable in Coq:

Lemma ex2: False <-> (forall (P:Prop), P).
intuition.
specialize (H False).
apply H.
Qed.

You might also want to check Dag Prawitz, 1965
Natural deduction : a proof-theoretical study
Page 67: Definability of False in Intuitionistic Logic
https://archive.org/details/naturaldeduction0000praw/page/66/mode/2up

So its even intuitionistically valid in 2nd Order.
Dag Prawitz makes also the remark "In contrast

to the situation for first order logic". Since its

intuitionistically valid we could obtain a Coq proof,
without using one of the classical logic mechanism
in the above Coq proof.

[Dan Christensen]

> Ever heard in your life about proof by cases? [snip childish abuse] The Drinker Paradox, when modelled

> with a pub, doens't have one of these forms:
> EXIST(a):[a in X => P]

See my previous posting. Again, we have:

x = the set of people drinking in a pub

P = the proposition that everyone in the pub is drinking

Which part don't you understand, Mr. Collapse?

Maybe you find set theory too confusing? If you would rather use a predicate X for the people drinking in that pub, then you would reasonably need to assume that this does not include everyone and everything in the universe. (Set theory automatically takes care of this.) Then it would follow that:

EXIST(a):[X(a) => P]

Look familiar?

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

2. ~X(x)
E Spec, 1

3. ~X(x) | P
Arb Or, 2

4. ~~X(x) => P
Imply-Or, 3

5. X(x) => P
Rem DNeg, 4

6. EXIST(a):[X(a) => P]
E Gen, 5

I hope this helps.

[Mostowski Collapse]

I don't see this here on Wikipedia:

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

Which you can write more explicitly the usual translation:

EXIST(a):[a e P & (D(a) => ALL(b):[b e P => D(p)]]

https://en.wikipedia.org/wiki/Bounded_quantifier#Bounded_quantifiers_in_set_theory

Where do you see EXIST(a):[a in X => P] ?

[Mostowski Collapse]

The translation rules are here on wikipedia:

Rule 1: How to translate bounded existential quantifier:
∃x in P [Q] <=> ∃x(x in P & Q)
Rule 2: How to translate bounded universal quantifier:
∀y in P [Q] <=> ∀y(y in P => Q)
https://en.wikipedia.org/wiki/Bounded_quantifier#Bounded_quantifiers_in_set_theory

The Drinker Paradox, to translate it needs both
Rule 1 and Rule 2, since it has a bounded existential
quantifier and a bounded universal quantifier:

/* Has ∃x in P and ∀y in P */

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

When you apply the translation rules, you get:

∃x(x in P & [D(x) => ∀y(y in P => D(y))])

Which DOES NOT have your "pathological" form:

∃x(x in P => Q)

The CLASH is "&" in the Drinker Paradox versus "=>" in your Pathological form.

What makes you think the Drinker Paradox on Wikipedia
has a pathological form, in contradiction to what every
body sees, that it DOES NOT have the pathological form?

[Mostowski Collapse]

What makes you cheating? The full proof, closing everything
gives me the following:

7 EXIST(a):~X(a) => EXIST(a):[X(a) => P]
Conclusion, 1

Thats also not the Drinker Paradox. The Drinker paradox,
without the Pub, would be:

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

It has indeed the "pathological" form. But it does not need
the assumption EXIST(a):~D(a) to be provable:

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

You only need EXIST(a):a=a, i.e. non-empty domain of discourse.

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

1 EXIST(a):~X(a)
Premise

2 ~X(x)
E Spec, 1

3 ~X(x) | P
Arb Or, 2

4 ~~X(x) => P
Imply-Or, 3

5 X(x) => P
Rem DNeg, 4

6 EXIST(a):[X(a) => P]
E Gen, 5

7 EXIST(a):~X(a) => EXIST(a):[X(a) => P]
Conclusion, 1

[Dan Christensen]

On Wednesday, April 26, 2023 at 12:21:40 PM UTC-4, Mostowski Collapse wrote:
> The translation rules are here on wikipedia:
>
> Rule 1: How to translate bounded existential quantifier:
> ∃x in P [Q] <=> ∃x(x in P & Q)
> Rule 2: How to translate bounded universal quantifier:
> ∀y in P [Q] <=> ∀y(y in P => Q)
> https://en.wikipedia.org/wiki/Bounded_quantifier#Bounded_quantifiers_in_set_theory
>
> The Drinker Paradox, to translate it needs both
> Rule 1 and Rule 2, since it has a bounded existential
> quantifier and a bounded universal quantifier:
>
> /* Has ∃x in P and ∀y in P */
> ∃x in P [D(x) => ∀y in P D(y)]
> https://en.wikipedia.org/wiki/Drinker_paradox
> When you apply the translation rules, you get:
>
> ∃x(x in P & [D(x) => ∀y(y in P => D(y))])
>
> Which DOES NOT have your "pathological" form:
>
> ∃x(x in P => Q)
>
> The CLASH is "&" in the Drinker Paradox versus "=>" in your Pathological form.
>
> What makes you think the Drinker Paradox on Wikipedia
> has a pathological form, in contradiction to what every
> body sees, that it DOES NOT have the pathological form?

See my fairly direct translation of Smullyan's original proof here:

http://www.dcproof.com/SmullyansDrinkerPrinciple.htm (28 lines)

He unreasonably wanted to consider the case of everyone and everything in the universe being a drinker. He needn't have, however. It would be reasonable to ignore this case and to simply assume to the contrary that there exists someone or something in the universe that is NOT a drinker. He considers this case on on line 12. On line 25, he concludes:

~ALL(b):[U(b) => Drinker(b)] <------------- U being the implicit "universe" in question

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

He could as easily have proven:

~ALL(b):[U(b) => Drinker(b)]

=> EXIST(a):[U(a) & [Drinker(a) => ~ALL(b):[U(b) => Drinker(b)]]] <--------------- Note the negation

Seems kind of "pathological," don't you think?

[Mostowski Collapse]

You are extremly talented in screwing the Drinker Paradox.
There is no assumption like this in the Drinker Paradox (without pub):

∃x~Dx

And there is also no assumption like this in the Drinker Paradox (with pub):

∃x(Px & ~Dx)

The Drinker Paradox has no such assumptions. Its provable without:

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

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

[Mostowski Collapse]

But ∃y~Dy respectively ∃y(Py & ~Dy) might appear
in a proof by cases, because they are the negation of:

∀yDy respectively ∀y(Py → Dy)

So you naturally prove the Drinker Paradox with two cases:

Case 1) ∃x~Dx respectively ∃x(Px & ~Dx)
Case 2) ∀yDy respectively ∀y(Py → Dy)

But unlike what you suggest by juggling with A => (B => A)
these "inner opposites" of Drinker Paradox are not provable:

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

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

So you cannot turn your "pathological" forms into something
that would show a collapse of logic, and therefore another
justification of avoiding them. The Drinker Paradox will

not open the gate of hell for you. Because there is no
such gate as far as one would know. It is not the case that
becaue the Drinker Paradox without pub uses the "pathological"

that we now can prove the "inner opposite" of the Drinker Paradox as well.
But keep on looking for such a Dan Christensen Paradox.
You might get famous, together with your church of nonsense.

[Dan Christensen]

On Wednesday, April 26, 2023 at 1:40:48 PM UTC-4, Mostowski Collapse wrote:

> > On Wednesday, April 26, 2023 at 12:21:40 PM UTC-4, Mostowski Collapse wrote:

[snip]

> > See my fairly direct translation of Smullyan's original proof here:
> >
> > http://www.dcproof.com/SmullyansDrinkerPrinciple.htm (28 lines)
> >
> > He unreasonably wanted to consider the case of everyone and everything in the universe being a drinker. He needn't have, however. It would be reasonable to ignore this case and to simply assume to the contrary that there exists someone or something in the universe that is NOT a drinker. He considers this case on on line 12. On line 25, he concludes:
> >
> > ~ALL(b):[U(b) => Drinker(b)] <------------- U being the implicit "universe" in question
> >
> > => EXIST(a):[U(a) & [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]
> >
> > He could as easily have proven:
> >
> > ~ALL(b):[U(b) => Drinker(b)]
> >
> > => EXIST(a):[U(a) & [Drinker(a) => ~ALL(b):[U(b) => Drinker(b)]]] <--------------- Note the negation
> >
> > Seems kind of "pathological," don't you think?

> You are extremly talented in screwing the Drinker Paradox.
> There is no assumption like this in the Drinker Paradox (without pub):
>
> ∃x~Dx
>

Wrong. On line 25, Smullyan considers that case: ~ALL(b):[U(b) => Drinker(b)]

Or equivalently: EXIST(b):[U(b) & ~Drinker(b)]

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

[Mostowski Collapse]

First you cheat with your DC Proofs, not closing them.
Now you cheat with snipping. I wrote the same:

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 19:40:48 UTC+2:
> And there is also no assumption like this in the Drinker Paradox (with pub):
> ∃x(Px & ~Dx)

https://groups.google.com/g/sci.logic/c/Q8FsBsKloo4/m/jhNAAGiyAwAJ

Why do you snip it? Its the same as your:

> Or equivalently: EXIST(b):[U(b) & ~Drinker(b)]

Whats wrong with you?

[Mostowski Collapse]

But its not an assumption of some sort of the Drinker
Paradox. It only appears in proof by cases, and
gets discarded. Proof by cases is:

G, A |- B
G, ~A |- B
--------------
G |- B

A and ~A get discarded respectively "discharged".
They do not persist into the theorem that gets proved.
Whats wrong with you?

Anyway I admire the roller coaster that the Drinker
Paradox induces in you. You are really going down
some rabbit wholes.

You seem to see some writing on the wall that nobody
else sees. Only this writting on the wall disappears
as fast as it appears.

So far I don't see anything "pathological" anywhere.
You cannot prove the "inner opposite" of the Drinker
Paradox. So what makes you see

these burning bushes?

[Mostowski Collapse]

Why is there no light at the end of the rabbit
hole. Its sucking you in and in, without end, the
Drinker Paradox and the "pathological" form have

taken Dan Christensen hostage. Just like Moses:

"There the angel of the Lord appeared to him in a
flame of fire out of a bush; he looked, and the bush
was blazing, yet it was not consumed. Then Moses said,
'I must turn aside and look at this great sight, and
see why the bush is not burned up.'
https://en.wikipedia.org/wiki/Burning_bush

An enternal flame has been lit in Dan Christensen.
Which is has already lasted fo months. Keeping
him from getting some sleep and consuming

all his resource, if there were not his mother
delivering him food and drinks into his basement.

[Mostowski Collapse]

So we are all waiting for the arrival of then ten
commandments concerning "pathological" formulas!

[Dan Christensen]

On Wednesday, April 26, 2023 at 2:05:53 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 26. April 2023 um 19:55:21 UTC+2:
> > On Wednesday, April 26, 2023 at 1:40:48 PM UTC-4, Mostowski Collapse wrote:
> >
> > > > On Wednesday, April 26, 2023 at 12:21:40 PM UTC-4, Mostowski Collapse wrote:
> > [snip]
> > > > See my fairly direct translation of Smullyan's original proof here:
> > > >
> > > > http://www.dcproof.com/SmullyansDrinkerPrinciple.htm (28 lines)
> > > >
> > > > He unreasonably wanted to consider the case of everyone and everything in the universe being a drinker. He needn't have, however. It would be reasonable to ignore this case and to simply assume to the contrary that there exists someone or something in the universe that is NOT a drinker. He considers this case on on line 12. On line 25, he concludes:
> > > >
> > > > ~ALL(b):[U(b) => Drinker(b)] <------------- U being the implicit "universe" in question
> > > >
> > > > => EXIST(a):[U(a) & [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]
> > > >
> > > > He could as easily have proven:
> > > >
> > > > ~ALL(b):[U(b) => Drinker(b)]
> > > >
> > > > => EXIST(a):[U(a) & [Drinker(a) => ~ALL(b):[U(b) => Drinker(b)]]] <--------------- Note the negation
> > > >
> > > > Seems kind of "pathological," don't you think?
> > > You are extremly talented in screwing the Drinker Paradox.
> > > There is no assumption like this in the Drinker Paradox (without pub):
> > >

> > > ∃x~Dx <------------------- SEE HERE

> > >
> > Wrong. On line 25, Smullyan considers that case: ~ALL(b):[U(b) => Drinker(b)]
> >
> > Or equivalently: EXIST(b):[U(b) & ~Drinker(b)]
> >

No comment????

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

> First you cheat with your DC Proofs, not closing them.

No "cheating" there. Every line of the proof is valid. Deal with it, Mr. Collapse.

> Now you cheat with snipping. I wrote the same:
> Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 19:40:48 UTC+2:
> > And there is also no assumption like this in the Drinker Paradox (with pub):
> > ∃x(Px & ~Dx)

Actually you wrote (scroll up):

"There is no assumption like this in the Drinker Paradox (without pub): ∃x~Dx"

And I refuted that nonsense. You were left speechless and could only change the subject. Must be frustrating as hell for you, Mr. Collapse.

[Mostowski Collapse]

Here is my post again. It litterally had "(without pub)" and "(with pub)":
Do you intend to snip it again, and use the crippled version to
halucinate some allegations and accusations? Whats wrong with you?

Maybe you don't understand what is meant by Drinker Paradox (without pub).
I am pretty sure everybody on sci.logic and sci.math undertands
that the formula ∃x(Dx → ∀yDy) is meant, since it doesn't have P the pub.

Maybe you don't understand what is meant by Drinker Paradox (with pub).
I am pretty sure everybody on sci.logic and sci.math undertands that the
formula ∃x(Px ∧ (Dx → ∀y(Py → Dy))) is meant, since it does have P the pub.

Only a complete idiot like Dan-O-Matik doesn't understand such parenthesis expressions.

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 19:40:48 UTC+2:
> You are extremly talented in screwing the Drinker Paradox.
> There is no assumption like this in the Drinker Paradox (without pub):
>
> ∃x~Dx
>

> And there is also no assumption like this in the Drinker Paradox (with pub):
>
> ∃x(Px & ~Dx)
>

> The Drinker Paradox has no such assumptions. Its provable without:
> ∃x(Dx → ∀yDy) is valid.
> https://www.umsu.de/trees/#~7x(Dx~5~6yDy)
> ∃xPx → ∃x(Px ∧ (Dx → ∀y(Py → Dy))) is valid.
> https://www.umsu.de/trees/#~7xPx~5~7x(Px~1(Dx~5~6y(Py~5Dy)))

https://groups.google.com/g/sci.logic/c/Q8FsBsKloo4/m/jhNAAGiyAwAJ

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 22:41:12 UTC+2:
> Still mushi in the brains? P stands for PUB. Can't you read english:

[Dan Christensen]

On Wednesday, April 26, 2023 at 4:56:15 PM UTC-4, Mostowski Collapse wrote:
> Here is my post again. It litterally had "(without pub)" and "(with pub)":

[snip]

You previously wrote:

>
> Yes I wrote, note the "WITHOUT PUB":

> "There is no assumption like this in the Drinker Paradox (without pub): ∃x~Dx"

> ∃x~Dx
>

There, you really seemed to be grasping at straws, Mr. Collapse!

Here, it is reasonable to interpret D(x) to mean x is a drinker in the pub. Smullyan considered two cases (see line 2):

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

Case 1: ALL(a):[U(a) => D(x)], that is, everyone and everything in the universe is a drinker in the pub (not at all reasonable)

Case 2: ~ALL(a):[U(a) => D(x)] or EXIST(a):[U(a) & ~D(c)], that is, there exists someone or something that is NOT a drinker in the pub (certainly true in "real life")

From (2), we can obtain:

EXIST(a):[U(a) & [Drinker(a) => Q]]] where Q is ANY proposition whatsoever, be it true or false. Substitute any logical expression whatsoever, with or without logical connectives and quantifiers. The result would be true even if, instead, you used the negation of that expression, hence the "pathological" aspect of it all.

I hope this helps.

[Mostowski Collapse]

You keep discussion the proof of the Drinker Paradox, and
citing the proof from Smullyan, and not the Drinker Paradox itself,
which is a formula, and not a proof. The Drinker Paradox can

have a couple of different proofs, not only the proof given
in Smulyan. Concerning the proof, I already wrote. Do you claim
that an "inner opposite" Drinker Paradox, i.e. a formula:

∃x(Dx → ¬∀yDy) respectively ∃x(Px ∧ (Dx → ¬∀y(Py → Dy))) is provable`?

Can you show us such a proof, in case you believe these
alternative Drinker Paradoxes are provable? For example
a proof in DC Poop? I doubt the (with pub) version is provable

from ∃xPx. If you could obtain such a proof, it would show
that the Wolfgang Schwarz tool has a bug.

Mostowski Collapse schrieb am Mittwoch, 26. April 2023 um 19:50:02 UTC+2:
> But ∃y~Dy respectively ∃y(Py & ~Dy) might appear
> in a proof by cases, because they are the negation of:
>
> ∀yDy respectively ∀y(Py → Dy)
>
> So you naturally prove the Drinker Paradox with two cases:
>
> Case 1) ∃x~Dx respectively ∃x(Px & ~Dx)
> Case 2) ∀yDy respectively ∀y(Py → Dy)
>
> But unlike what you suggest by juggling with A => (B => A)
> these "inner opposites" of Drinker Paradox are not provable:
>
> ∃x(Dx → ¬∀yDy) is invalid.
> https://www.umsu.de/trees/#~7x(Dx~5~3~6yDy)
>

> ∃xPx → ∃x(Px ∧ (Dx → ¬∀y(Py → Dy))) is invalid.
> https://www.umsu.de/trees/#~7xPx~5~7x(Px~1(Dx~5~3~6y(Py~5Dy)))
https://groups.google.com/g/sci.logic/c/Q8FsBsKloo4/m/BFJ0AemyAwAJ

[Mostowski Collapse]

I nowhere find U(a) on Wikipedia:

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

Where did you get U(a) from? When you make this case, which
is also nonsense, since the x in D(x) is free, not bound by quantifier:

> Case 1: ALL(a):[U(a) => D(x)], that is, everyone and everything
in the universe is a drinker in the pub (not at all reasonable)

The case in usually:

ALL(a):[P(a) => D(a)] respectively ~EXIST(a):[P(a) & ~D(a)]

And the english translation is:

"Every body is drinking in the pub"

Which is a quite likely situation for a pub. Possibly more
likely than having a guest that is not drinking, and only
ordering some finger food. Even the finger food is given

to the guests so that they drink more, and that the pub
can make high sales of their beverages. Ever been in a
pub? Or do you live by the food and drinks that your mother

sends you to your basementn and you never go out?

[Mostowski Collapse]

Maybe shut down your computer and go into a pub,
to understand the Drinker Paradox. Now I am convinced
you cannot grasp the situation of a pub and having

guests that order and don't order drinks. Also the
picture here shows me that there is something wrong
with your understanding of the Drinker Paradox:

http://www.dcproof.com/DrinkersParadox.html

Why is there a Betrand Russell in the picture? The
drinker Paradox is not dealing with a predicate U(a),
the Universe, where this is a set or not. The predicate

is P(a) for a pub only, no set theory involved. This
is also a nonsense translation here. Why would one
translate Smullyan with U(a) when Smullyan invented

the pub as a setting for his paradox:

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

Sometimes you don't make sense Dan-O-Matik.

[Mostowski Collapse]

I mean Smullyan starts his riddle with:

"A man was at a bar"
https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf

Why do you make chit chat about universe here:

> It would be reasonable to ignore this case and to simply
assume to the contrary that there exists someone or
something in the universe that is NOT a drinker.

How should this be relevant if anyway everything
is restrictued to the pub P? Thats a crazy idea!

[Dan Christensen]

On Wednesday, April 26, 2023 at 5:27:17 PM UTC-4, Mostowski Collapse wrote:

[snip]
> > You previously wrote:
> >
> > >
> > > Yes I wrote, note the "WITHOUT PUB":
> > > "There is no assumption like this in the Drinker Paradox (without pub): ∃x~Dx"
> > > ∃x~Dx
> > >
> >
> > There, you really seemed to be grasping at straws, Mr. Collapse!
> >
> > Here, it is reasonable to interpret D(x) to mean x is a drinker in the pub. Smullyan considered two cases (see line 2):
> >
> > http://www.dcproof.com/SmullyansDrinkerPrinciple.htm
> >
> > Case 1: ALL(a):[U(a) => D(x)], that is, everyone and everything in the universe is a drinker in the pub (not at all reasonable)
> >
> > Case 2: ~ALL(a):[U(a) => D(x)] or EXIST(a):[U(a) & ~D(c)], that is, there exists someone or something that is NOT a drinker in the pub (certainly true in "real life")
> >
> > From (2), we can obtain:
> >
> > EXIST(a):[U(a) & [Drinker(a) => Q]]] where Q is ANY proposition whatsoever, be it true or false. Substitute any logical expression whatsoever, with or without logical connectives and quantifiers. The result would be true even if, instead, you used the negation of that expression, hence the "pathological" aspect of it all.
> >

> You keep discussion the proof of the Drinker Paradox, and
> citing the proof from Smullyan, and not the Drinker Paradox itself,
> which is a formula, and not a proof.

[snip]

Smullyan originally framed the Drinker Principle as follows:

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

No mention of any pub.

Here is his proof translated word-for-word into the DC Proof format:

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

I have also devised my set theoretic proof:

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

[Mostowski Collapse]

Troll alert. You might have copied the words from Smullyan.
But you didn't understand them. The formulas that you placed
under the words of Smullyan don't make any sense.

You use nonsense like. Already this here is wrong:

"Either it is true that everybody drinks or it isn't." (Two cases to consider)

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

It should read:

2 ALL(b):[P(b) => Drinker(b)] | ~ALL(b):[P(b) => Drinker(b)]
Or Not

Smullayan is taking about the pub, not the universe.
Whats wrong with you? Smullyan starts with:

"A man was at a bar"
https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf

[Mostowski Collapse]

Just read Smullyan:

"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

"around the house", and not around the planet earth
and venus and mars etc.. The whole universe. You
simply did never undertand the Drinker Paradox Dan O

Matik. This is so sad to see! Its a little frightening.

[Mostowski Collapse]

Because you didn't read Smullyan, and because you are
brain damaged, you make misinterpretations and strange
estimates about probabilities of formulas, like here:

> Case 1: ALL(a):[U(a) => D(x)], that is, everyone and everything
in the universe is a drinker in the pub (not at all reasonable)

Whereas what Smullyan means:

> Case 1: ALL(a):[P(a) => D(x)], that is, Every body is drinking
in the pub, which is quite possible, for example if somebody
pays a round for everybody, or if every body is drinking in the pub.

If like 99% of the People that go into a Pub, also drink in
the Pub. Then the probability that a Pub with lets say 20
guests in it, every body drinks is still:

99% ** 20 = 81%

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

[Dan Christensen]

On Wednesday, April 26, 2023 at 6:27:13 PM UTC-4, Mostowski Collapse wrote:
> Just read Smullyan:
>
> "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
>

On page 210, paragraph 3 where he begins his proof:

"Solution. Yes, it really is true that there exists someone such that whenever he (or she) drinks, everybody drinks."

No mention of any pub in his proof. A minor point, but since you brought it up...

[Dan Christensen]

On Wednesday, April 26, 2023 at 6:38:55 PM UTC-4, Mostowski Collapse wrote:
> Because you didn't read Smullyan,

You are s glutton for punishment, Mr. Collapse. Take another look at the commentary in my proof:

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

[snip childish abuse]

> > Case 1: ALL(a):[U(a) => D(x)], that is, everyone and everything
> in the universe is a drinker in the pub (not at all reasonable)
> Whereas what Smullyan means:
>
> > Case 1: ALL(a):[P(a) => D(x)], that is, Every body is drinking
> in the pub, which is quite possible, for example if somebody
> pays a round for everybody, or if every body is drinking in the pub.
>

Nowhere does he mention a pub in this proof (p. 210). Try again.

[Mostowski Collapse]

Well what does this mean. Maybe not in Alaska?

"A man was at a bar"
https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf

And then wikipedia goes on:

"The proof begins by recognizing it is true that either everyone in the pub
is drinking, or at least one person in the pub is not drinking. Consequently,
there are two cases to consider:"
https://en.wikipedia.org/wiki/Drinker_paradox

LMAO!

[Mostowski Collapse]

Basically you are stipulating that the phrase "everybody" used
in the context of the Drinker Paradox means everything in the
universe, including Unicorns, Cars, Airplanes, etc...

Already since phrase is "-body" you can assume its not the
universe. So it must refer to some humans. Prologue of
the story give the context so that the "-body" can be resolved.

************************************************
Obviously you are not the sharpest tool in the shed.
************************************************

Maybe study Donkey Anaphora and anaphora in general?
Before you create nonsens posts like this here. Even
Wikipedia gets it right, you are possibly the only moron

that didn't get it right and was able to distort it?

From Wikipedia it gives me:

> Case 1: ALL(a):[P(a) => D(x)], that is, Every body is drinking
in the pub, which is quite possible, for example if somebody
pays a round for everybody, or if every body is drinking in the pub.

Your Nonsense wants:

> Case 1: ALL(a):[U(a) => D(x)], that is, everyone and everything
in the universe is a drinker in the pub (not at all reasonable)
Whereas what Smullyan means:

How can it be unreasonable that everybody is drinking [in the pub]?
I would say this is rather a quite possible and reasonable
case, that might be not that infrequent.

It only gets infrequent if you consider Apes, Benanas, etc.. as you do.

[Mostowski Collapse]

Here is the difference between "-body" and "-thing":

Some unspecified person
https://en.wiktionary.org/wiki/somebody

An uncertain or unspecified thing;
https://en.wiktionary.org/wiki/something

Hope this helps!

[Mostowski Collapse]

Its even easier in French:

quelqu’un
https://de.wiktionary.org/wiki/quelqu%E2%80%99un

quelque chose
https://de.wiktionary.org/wiki/quelque_chose

Although quelqu’un is also used for choses sometimes,
in its plural form. Maybe this explains why you don't understand
Smullyan? Its a french english problem?

[Dan Christensen]

On Thursday, April 27, 2023 at 7:26:40 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 27. April 2023 um 00:51:57 UTC+2:
> > On Wednesday, April 26, 2023 at 6:38:55 PM UTC-4, Mostowski Collapse wrote:
> > > Because you didn't read Smullyan,
> > You are s glutton for punishment, Mr. Collapse. Take another look at the commentary in my proof:
> >
> > http://www.dcproof.com/SmullyansDrinkerPrinciple.htm
> >
> > [snip childish abuse]
> > > > Case 1: ALL(a):[U(a) => D(x)], that is, everyone and everything
> > > in the universe is a drinker in the pub (not at all reasonable)
> > > Whereas what Smullyan means:
> > >
> > > > Case 1: ALL(a):[P(a) => D(x)], that is, Every body is drinking
> > > in the pub, which is quite possible, for example if somebody
> > > pays a round for everybody, or if every body is drinking in the pub.
> > >
> > Nowhere does he mention a pub in this proof (p. 210). Try again.

> Well what does this mean. Maybe not in Alaska?
> "A man was at a bar"
> https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf

Not part of the Smullyan's actual proof on p. 210. Deal with it, Mr. Collapse.

> And then wikipedia goes on:
>
> "The proof begins by recognizing it is true that either everyone in the pub
> is drinking, or at least one person in the pub is not drinking. Consequently,
> there are two cases to consider:"
> https://en.wikipedia.org/wiki/Drinker_paradox
>

It is best to stick the original sources in such cases.

[Dan Christensen]

On Thursday, April 27, 2023 at 7:38:07 AM UTC-4, Mostowski Collapse wrote:
> Basically you are stipulating that the phrase "everybody" used
> in the context of the Drinker Paradox means everything in the
> universe, including Unicorns, Cars, Airplanes, etc...
>
> Already since phrase is "-body" you can assume its not the
> universe. So it must refer to some humans. Prologue of
> the story give the context so that the "-body" can be resolved.
>

[snip]

His proof makes no use of a Pub or a Human predicate. It he has only the one predicate (Drinker). I introduced a predicate U for the implicit "domain of discourse."

With my set-theoretic version, you avoid this silliness. In ordinary set theory (if not in more exotic versions), there is no universal set, i.e. every set excludes something (see Russell's Paradox). For any set x and proposition Q (be it true or false), we can prove: EXIST(a):[a in x => Q].

[Dan Christensen]

On Thursday, April 27, 2023 at 11:44:51 AM UTC-4, Dan Christensen wrote:
> On Thursday, April 27, 2023 at 7:38:07 AM UTC-4, Mostowski Collapse wrote:
> > Basically you are stipulating that the phrase "everybody" used
> > in the context of the Drinker Paradox means everything in the
> > universe, including Unicorns, Cars, Airplanes, etc...
> >
> > Already since phrase is "-body" you can assume its not the
> > universe. So it must refer to some humans. Prologue of
> > the story give the context so that the "-body" can be resolved.
> >
> [snip]
>
> His proof makes no use of a Pub or a Human predicate. It he has only the one predicate (Drinker). I introduced a predicate U for the implicit "domain of discourse."
>
> With my set-theoretic version, you avoid this silliness. In ordinary set theory (if not in more exotic versions), there is no universal set, i.e. every set excludes something (see Russell's Paradox). For any set x and proposition Q (be it true or false), we can prove: EXIST(a):[a in x => Q].

For a set-theoretic Drinker's Paradox, we can use x = the set of drinkers in a given pub, and Q = every one in that pub is a drinker. Alternatively, we could use Q = the negation, NOT everyone in that pub is a drinker. We could use ANY proposition for Q, be it true or false. Hence the "pathological "nature of the EXIST(a):[a in x => Q] construct.

[Mostowski Collapse]

Dan Christensen schrieb am Donnerstag, 27. April 2023 um 17:44:51 UTC+2:
> His proof makes no use of a Pub or a Human predicate. It he has only the one predicate (Drinker).
I introduced a predicate U for the implicit "domain of discourse."

It has a human predicate, he says:

Solution.
"Either it is true that EVERBODY drinks or it isn't. "
https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf

He says "-BODY", he doesn't say "-THING".

You cannot translate it as:

ALL(x):[U(x) => D(x)] v ~ALL(x):[U(x) => D(x)]

With U meaning domain of discourse, i.e. universe.

Whats wrong with you? Are you dumb or what?

[Mostowski Collapse]

Maybe its a french english problem for Dan O Matik? You can
translate this sentences. Also in french it is not translated
towards domain of discourse:

> Solution.
> "Either it is true that EVERBODY drinks or it isn't. "
> https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf

Bable fish gives me:
> Soit il est vrai que TOUT LE MONDE boit, soit ce n'est pas le cas.
https://www.babelfish.ch/

ALL(x):[P(x) => D(x)] v ~ALL(x):[P(x) => D(x)]

Where P means the common noun phrase (CN) Person.
But it would be an incorrect translation, if you use
U that would mean the comon noun phrase (CN) Thing.

If you use U, i.e. the common noun phrase (CN) Thing,
then this would for example include my stone nr 12
in my garden landscape. But this is nonsense.

https://www.shutterstock.com/de/image-photo/landscaping-garden-path-194433671

When you are in a room with Anna and Bert, and your
name is Carlo, and the room has also a Table and three
Chairs, then there is a difference between everybody

and everything in the room example:

Everybody = {Anna, Bert, Carlo}
Everything = {Anna, Bert, Carlo, Table, Chair1, Chair2, Chair3}
(Even maybe everything only = {Table, Chair1, Chair2, Chair3} )

[Mostowski Collapse]

Just check out the given explanation on french wikipedia,
what "tout le monde" i.e. "everbody" means:

1. Toutes les personnes d’un ensemble donné
2. (En particulier) Toutes les parties prenantes d'une affaire.
https://fr.wiktionary.org/wiki/tout_le_monde

Its always relative to some reference collection. If you want
to express the everybody in the on earth, there is even
a special expression for that:

Pour le monde dans le sens de la Terre, on dit le monde entier.
https://fr.wiktionary.org/wiki/tout_le_monde

In as far this brings me to a nice exercise. Because
Smullyan was complete aware of this reference to some
collection, he deviced his Paradox as follows:

It contains 3 different Paradoxes with 3 different
referents of everybody:
- Drinker Paradox
- Sterile Woman Paradox (He calls the more dramatic version)
- Abstinenent Logician Paradox (From Christmas card imaginary conversation)
-
https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf

[Dan Christensen]

On Friday, April 28, 2023 at 8:56:27 AM UTC-4, Mostowski Collapse wrote:
> Dan Christensen schrieb am Donnerstag, 27. April 2023 um 17:44:51 UTC+2:
> > His proof makes no use of a Pub or a Human predicate. It he has only the one predicate (Drinker).
> > I introduced a predicate U for the implicit "domain of discourse."

> It has a human predicate, he says:
>
> Solution.
> "Either it is true that EVERBODY drinks or it isn't. "
> https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf
>
> He says "-BODY", he doesn't say "-THING".
>

You are grasping at straws here, Mr. Collapse. In supposedly "standard" FOL, its mysterious, non-empty domain of discourse is never named or specified. Not very mathematical. Again, you can avoid all this silliness by using a set-theoretic model (my preference). Then we would have:

ALL(a):[a in D => Q]

For ANY set D and ANY proposition Q, be it true or false.

I think Smullyan used "standard" FOL.

> You cannot translate it as:
>
> ALL(x):[U(x) => D(x)] v ~ALL(x):[U(x) => D(x)]
>

I disagree. As you can see in my proof, it works. Assuming a non-empty predicate U (its ONLY requirement), you can prove:

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

The first 4 lines:

The non-empty domain of discourse analogous to the IMPLICIT, UNSPECIFIED domain of discourse in First-Order Predicate Logic.

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

"Either it is true that everybody drinks or it isn't." (Two cases to consider)

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

"Suppose it is true that everybody drinks." (Case 1)

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

"Then take any person--call him Jim."

4. U(jim) <------------------------------ Applying the existence of a non-empty domain of discourse U (line 1)
E Spec, 1
...

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

Deal with it, Mr. Collapse.

[Julio Di Egidio]

On Friday, 28 April 2023 at 18:00:33 UTC+2, Dan Christensen wrote:

> Again, you can avoid all this silliness by using a set-theoretic
> model (my preference). Then we would have:
> ALL(a):[a in D => Q]
> For ANY set D and ANY proposition Q, be it true or false.

Is that an axiom or a provable statement
from your set theory?

Meanwhile, and as I have already pointed out
to you, *the only set that can exist in that theory
is the empty set*.

Let's look at it by (classical) case analysis on Q:
- Case Q=True:
ALL(a):[a in D => True]
ALL(a):[a in D] // by trivial impl.
namely, *every set is the universal set*.
- Case Q=False (i.e. ~Q=True):
ALL(a):[a in D => False]
ALL(a):[a not in D] // by vacuous impl.
namely, *every set is the empty set*.

Which, to re-sum it up, is:
ALL(a):[a in D => (True \/ False)]
equivalent to:
ALL(a):[(a in D => True) /\ (a in D => False)]
which is true iff:
*every set is the universal set*
AND *every set is the empty set*
which eventually means:
*There is only the empty set in that theory!*
QED.

So, the only interesting question really remains
whether you introduce that statement as an
axiom or it is a provable theorem from you set
theory axioms.

If the former, not all is lost since that *is* an
altogether nonsensical statement.

Julio

[Dan Christensen]

On Friday, April 28, 2023 at 12:32:34 PM UTC-4, Julio Di Egidio wrote:
> On Friday, 28 April 2023 at 18:00:33 UTC+2, Dan Christensen wrote:
>
> > Again, you can avoid all this silliness by using a set-theoretic
> > model (my preference). Then we would have:
> > ALL(a):[a in D => Q]
> > For ANY set D and ANY proposition Q, be it true or false.
> Is that an axiom or a provable statement
> from your set theory?
>

It is an application of a theorem that ALL(s):[Set(s) => EXIST(x):[x in s => Q(x,s)]]

Here is formal proof: http://www.dcproof.com/DrinkersThm1.htm

Perhaps you can go this proof and point out where you think I first supposedly went wrong.

> Meanwhile, and as I have already pointed out
> to you, *the only set that can exist in that theory
> is the empty set*.
>

D can be any set whatsoever.

> Let's look at it by (classical) case analysis on Q:

> - Case Q=True:

In ordinary logic, that would be simply "Q". I'm guessing Q=False would be " ~Q"

> ALL(a):[a in D => True]
> ALL(a):[a in D] // by trivial impl.
> namely, *every set is the universal set*.
> - Case Q=False (i.e. ~Q=True):
> ALL(a):[a in D => False]
> ALL(a):[a not in D] // by vacuous impl.
> namely, *every set is the empty set*.
>
> Which, to re-sum it up, is:
> ALL(a):[a in D => (True \/ False)]
> equivalent to:
> ALL(a):[(a in D => True) /\ (a in D => False)]
> which is true iff:
> *every set is the universal set*
> AND *every set is the empty set*
> which eventually means:
> *There is only the empty set in that theory!*

[snip]

Huh??? Please recast this "proof" using more commonly used notation without the logical constants "True" and "False". You don't usually see them in textbook math proofs.

[Julio Di Egidio]

On Friday, 28 April 2023 at 22:14:57 UTC+2, Dan Christensen wrote:
> On Friday, April 28, 2023 at 12:32:34 PM UTC-4, Julio Di Egidio wrote:
> > On Friday, 28 April 2023 at 18:00:33 UTC+2, Dan Christensen wrote:
> >
> > > Again, you can avoid all this silliness by using a set-theoretic
> > > model (my preference). Then we would have:
> > > ALL(a):[a in D => Q]
> > > For ANY set D and ANY proposition Q, be it true or false.
> >
> > Is that an axiom or a provable statement
> > from your set theory?
>
> It is an application of a theorem that ALL(s):[Set(s) => EXIST(x):[x in s => Q(x,s)]]
> Here is formal proof: http://www.dcproof.com/DrinkersThm1.htm
> Perhaps you can go this proof and point out where you think I first supposedly went wrong.

Ah, that one, where Q(x,s) again is *any* proposition,
and which, to answer my own question, relies on the
*theorem* "ALL(s):[Set(s) => EXIST(a):~a e s]".
<http://www.dcproof.com/UniversalSet.htm>

So your system, the set theory at least, *is* doomed.

> > Meanwhile, and as I have already pointed out
> > to you, *the only set that can exist in that theory
> > is the empty set*.
>
> D can be any set whatsoever.

That's its definition, I have shown the consequences.

> > Let's look at it by (classical) case analysis on Q:
> > - Case Q=True:
> In ordinary logic, that would be simply "Q". I'm guessing Q=False would be " ~Q"

<snip>
> Huh??? Please recast this "proof" using more commonly used notation
> without the logical constants "True" and "False". You don't usually see
> them in textbook math proofs.

That, as usual when it comes to mathematics and doing
mathematics, is the very opposite of true: indeed even you
had to say "any proposition Q, be it true or false".

That said, as for proving things formally, try these:
ALL(s):[Set(s) => EXIST(x):[x in s => (x = x)]].
ALL(s):[Set(s) => EXIST(x):[x in s => ~(x = x)]].
Just two "applications" of your theorem.

So your system, the set theory at least, *is* doomed.
And now if you are smart, you'll investigate that and
fix it...

Have fun. (QED and EOD.)

Julio

[Mostowski Collapse]

At least you are finally asking the right questions.
Where do you see this here in Smullyans actual proof?

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

Is there even a Set predicate on p. 210 ? Could you
maybe finally get your head around the Drinker Paradox

and understand it? Its really trivial BTW.

[Mostowski Collapse]

You can also prove it (without pub) in Coq, no problem at all:
https://github.com/mayconamaro/drinkerParadox/blob/master/drinkerParadox.v

Just introduce classical logic in Coq:
Axiom LEM : forall P : Prop, P \/ ~P.

Just introduce non-empty domain:
Hypothesis u : U.

Have Fun! (Same for you Julio, its definitively provable in Coq)

P.S.: The above is version 4 of the Drinker Paradox:

- Drinker Paradox (with pub)

- Sterile Woman Paradox (He calls the more dramatic version)
- Abstinenent Logician Paradox (From Christmas card imaginary conversation)

- Drinker Paradox (without pub, if we stipulate the domain of discourse is restricted)
https://cs.bme.hu/~szeredi/ait/Smullyan-What-is-the-Name-of-This-Book.pdf

[Julio Di Egidio]

On Saturday, 29 April 2023 at 00:01:18 UTC+2, Mostowski Collapse wrote:

> You can also prove it (without pub) in Coq, no problem at all:

Drinker's Paradox (in Coq), with or without pub, and with detailed analysis:
<https://groups.google.com/g/sci.logic/c/kDCIdVY9U4E/m/MeJGiN1UAAAJ>

ESAD, you spamming piece of shit.

*Plonk*

Julio

[Mostowski Collapse]

The link here is older, its from May 15, 2019
https://github.com/mayconamaro/drinkerParadox/blob/master/drinkerParadox.v

Your post is from 22.03.2023, 14:50:54. If you take the
Coq proof from May 15, 2019, and rename U to P, for pub:

Just introduce non-empty domain:
Hypothesis p : P.

You get a proof of what is described here:

/* Drinker Paradox / Drinker Theorem */
Consider the set of all people in a given pub. Then there
exists a person who if her or she is drinking in the given pub,
then everyone in that pub is drinking.

But this modification is not anymore the Drinker Paradox, its just nonsense:

/* Abomination / Crazyness by Dan Christensen */
Consider the set of all drinkers in that world, and the set of all
people in a given pub. Then there exists a person who, if her or she is
drinking, then everyone in that pub is drinking.
http://www.dcproof.com/DrinkersThm1.htm

Where on Smullyan's actual proof on p. 210 do you see
such an Abomination / Crazyness Dan-O-Matik. What
dope were you consuming?

[Julio Di Egidio]

On Saturday, 29 April 2023 at 00:27:07 UTC+2, Mostowski Collapse wrote:

> <stupidities vulgarities lies and insanity ad nauseam>

*Warning*: Mostowski Collapse, real name Jan Burse, is a piece
of spamming and trolling shit across as many boards as s/he manages:
and I'd just like to know who is responsible for paying his or her bills!

ESAD you and the whole resident insane retarded nazi brigade.

*Troll Alert*

Julio