Using ordinary set theory, we can prove:

(1) ALL(a):[a in X & a=a] is FALSE for any set X.

Whereas

(2) ALL(a):[a in X => a=a]] is TRUE for any set X.

----------------------------------------------------------------------
PROOF (1)

Lemma: From Russel's Paradox (Proof: http://dcproof.com/UniversalSet.htm )

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

Let x be a set

2. Set(x)
Premise

Apply lemma

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 | ~y=y
Arb Or, 5

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

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

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

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

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

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

----------------------------------------------------------------------
PROOF (2)

1. Set(x)
Premise

2. y in x
Premise

3. y=y
Reflex

4. ALL(a):[a in x => a=a]
Conclusion, 2

5. ALL(x):[Set(x) => ALL(a):[a in x => a=a]]
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

On Saturday, June 3, 2023 at 10:33:09 AM UTC-7, Dan Christensen wrote:
> Using ordinary set theory, we can prove:
>
> (1) ALL(a):[a in X & a=a] is FALSE for any set X.
>
> Whereas
>
> (2) ALL(a):[a in X => a=a]] is TRUE for any set X.
>
> ----------------------------------------------------------------------
> PROOF (1)
>
> Lemma: From Russel's Paradox (Proof: http://dcproof.com/UniversalSet.htm )
>
> 1. ALL(a):[Set(a) => EXIST(b):~b in a]
> Axiom
>
> Let x be a set
>
> 2. Set(x)
> Premise
>
> Apply lemma
>
> 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 | ~y=y
> Arb Or, 5
>
> 7. ~[~~y in x & ~~y=y]
> DeMorgan, 6
>
> 8. ~[y in x & ~~y=y]
> Rem DNeg, 7
>
> 9. ~[y in x & y=y]
> Rem DNeg, 8
>
> 10. ALL(x):[Set(x) => EXIST(a):~[a in x & a=a]]
> Conclusion, 2
>
> 11. ALL(x):[Set(x) => ~ALL(a):~~[a in x & a=a]]
> Quant, 10
>
> 12. ALL(x):[Set(x) => ~ALL(a):[a in x & a=a]]
> Rem DNeg, 11
>
> ----------------------------------------------------------------------
> PROOF (2)
>
> 1. Set(x)
> Premise
>
> 2. y in x
> Premise
>
> 3. y=y
> Reflex
>
> 4. ALL(a):[a in x => a=a]
> Conclusion, 2
>
> 5. ALL(x):[Set(x) => ALL(a):[a in x => a=a]]
> 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

Maybe you should read Quine, even the introduction to his book
on set theory could help you, he doesn't employ "material implication",
though.

He does help explain class/set distinction and then also gets into
when "=" means intensionality and when it means extensionality.

Then he doesn't so much "address the resolution of the paradoxes
of quantification" as allude to them.

Anyways your

1) "I'm conflicted"
2) "Whatever..."

isn't any stronger than

1) "Whatever..."

Yeah there are features of universal quantification and equals
that sort of imply a universe of logical theoretical objects
already exists, and you can only infer deductively about them,
which is why there is what's called "science" and for example
"systems of representation in reference" about "expert systems"
and in the face of "uncertainty".

Of course there are closed-deductively forms in the finite, ....

But, as Quine points out, at some point the logic
gets into the, infinite. Quine glosses over issues
of universality and extensionality when he talks
about "=" as a predicate, then also he indicates that
all the "special forms of predicates" are each their
own kinds of "ultimate classes". (In, "little theories".)

I guess its rather the paradox of irrelevance.
There are so many theorems that are irrelevant,
und would never make it into a paper, since

they use either inconsistent assumptions,
or then are non-construction and can therefore not be
applied. Are just some Unicorn dreams.

Maybe post some math when have outgrown your
juvenile phase of 1000-th version of Russels paradox
which is totally irrelevant and useless to mathematics.

Dan Christensen schrieb am Samstag, 3. Juni 2023 um 19:33:09 UTC+2:
> Using ordinary set theory, we can prove:
>
> (1) ALL(a):[a in X & a=a] is FALSE for any set X.
>
> Whereas
>
> (2) ALL(a):[a in X => a=a]] is TRUE for any set X.
>
> ----------------------------------------------------------------------
> PROOF (1)
>
> Lemma: From Russel's Paradox (Proof: http://dcproof.com/UniversalSet.htm )
>
> 1. ALL(a):[Set(a) => EXIST(b):~b in a]
> Axiom
>
> Let x be a set
>
> 2. Set(x)
> Premise
>
> Apply lemma
>
> 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 | ~y=y
> Arb Or, 5
>
> 7. ~[~~y in x & ~~y=y]
> DeMorgan, 6
>
> 8. ~[y in x & ~~y=y]
> Rem DNeg, 7
>
> 9. ~[y in x & y=y]
> Rem DNeg, 8
>
> 10. ALL(x):[Set(x) => EXIST(a):~[a in x & a=a]]
> Conclusion, 2
>
> 11. ALL(x):[Set(x) => ~ALL(a):~~[a in x & a=a]]
> Quant, 10
>
> 12. ALL(x):[Set(x) => ~ALL(a):[a in x & a=a]]
> Rem DNeg, 11
>
> ----------------------------------------------------------------------
> PROOF (2)
>
> 1. Set(x)
> Premise
>
> 2. y in x
> Premise
>
> 3. y=y
> Reflex
>
> 4. ALL(a):[a in x => a=a]
> Conclusion, 2
>
> 5. ALL(x):[Set(x) => ALL(a):[a in x => a=a]]
> 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

On Saturday, June 3, 2023 at 2:02:40 PM UTC-4, Ross Finlayson wrote:
> On Saturday, June 3, 2023 at 10:33:09 AM UTC-7, Dan Christensen wrote:
> > Using ordinary set theory, we can prove:
> >
> > (1) ALL(a):[a in X & a=a] is FALSE for any set X.
> >
> > Whereas
> >
> > (2) ALL(a):[a in X => a=a]] is TRUE for any set X.
> >
> > ----------------------------------------------------------------------
> > PROOF (1)
> >
> > Lemma: From Russel's Paradox (Proof: http://dcproof.com/UniversalSet.htm )
> >
> > 1. ALL(a):[Set(a) => EXIST(b):~b in a]
> > Axiom
> >
> > Let x be a set
> >
> > 2. Set(x)
> > Premise
> >
> > Apply lemma
> >
> > 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 | ~y=y
> > Arb Or, 5
> >
> > 7. ~[~~y in x & ~~y=y]
> > DeMorgan, 6
> >
> > 8. ~[y in x & ~~y=y]
> > Rem DNeg, 7
> >
> > 9. ~[y in x & y=y]
> > Rem DNeg, 8
> >
> > 10. ALL(x):[Set(x) => EXIST(a):~[a in x & a=a]]
> > Conclusion, 2
> >
> > 11. ALL(x):[Set(x) => ~ALL(a):~~[a in x & a=a]]
> > Quant, 10
> >
> > 12. ALL(x):[Set(x) => ~ALL(a):[a in x & a=a]]
> > Rem DNeg, 11
> >
> > ----------------------------------------------------------------------
> > PROOF (2)
> >
> > 1. Set(x)
> > Premise
> >
> > 2. y in x
> > Premise
> >
> > 3. y=y
> > Reflex
> >
> > 4. ALL(a):[a in x => a=a]
> > Conclusion, 2
> >
> > 5. ALL(x):[Set(x) => ALL(a):[a in x => a=a]]
> > 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

> Maybe you should read Quine, even the introduction to his book
> on set theory could help you,

[snip]

Thanks, but I'm not asking for any "help." I'm simply pointing why, in ordinary set theory (no classes), you should avoid constructs of the form ALL(a):[a in x & P]. They will always be false since every set must exclude some object.

> he doesn't employ "material implication",

[snip]

I see no reason to avoid material implication for logical propositions that are unambiguously either true or false in the present.

Dan

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

Also for a moron like you it might not be evident
that you can replace a=a by TRUE. So you proved
these two theorems:

~ALL(a):[a e X]
TRUE

The first theorem has not even a mosquito leg
difference from your Universal Set theorem, at
least not in classical logic. And the second theorem,

is not something anybody would surprise.

Mild Shock schrieb am Samstag, 3. Juni 2023 um 20:13:41 UTC+2:
> I guess its rather the paradox of irrelevance.
> There are so many theorems that are irrelevant,
> und would never make it into a paper, since
>
> they use either inconsistent assumptions,
> or then are non-construction and can therefore not be
> applied. Are just some Unicorn dreams.
>
> Maybe post some math when have outgrown your
> juvenile phase of 1000-th version of Russels paradox
> which is totally irrelevant and useless to mathematics.
> Dan Christensen schrieb am Samstag, 3. Juni 2023 um 19:33:09 UTC+2:
> > Using ordinary set theory, we can prove:
> >
> > (1) ALL(a):[a in X & a=a] is FALSE for any set X.
> >
> > Whereas
> >
> > (2) ALL(a):[a in X => a=a]] is TRUE for any set X.
> >
> > ----------------------------------------------------------------------
> > PROOF (1)
> >
> > Lemma: From Russel's Paradox (Proof: http://dcproof.com/UniversalSet.htm )
> >
> > 1. ALL(a):[Set(a) => EXIST(b):~b in a]
> > Axiom
> >
> > Let x be a set
> >
> > 2. Set(x)
> > Premise
> >
> > Apply lemma
> >
> > 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 | ~y=y
> > Arb Or, 5
> >
> > 7. ~[~~y in x & ~~y=y]
> > DeMorgan, 6
> >
> > 8. ~[y in x & ~~y=y]
> > Rem DNeg, 7
> >
> > 9. ~[y in x & y=y]
> > Rem DNeg, 8
> >
> > 10. ALL(x):[Set(x) => EXIST(a):~[a in x & a=a]]
> > Conclusion, 2
> >
> > 11. ALL(x):[Set(x) => ~ALL(a):~~[a in x & a=a]]
> > Quant, 10
> >
> > 12. ALL(x):[Set(x) => ~ALL(a):[a in x & a=a]]
> > Rem DNeg, 11
> >
> > ----------------------------------------------------------------------
> > PROOF (2)
> >
> > 1. Set(x)
> > Premise
> >
> > 2. y in x
> > Premise
> >
> > 3. y=y
> > Reflex
> >
> > 4. ALL(a):[a in x => a=a]
> > Conclusion, 2
> >
> > 5. ALL(x):[Set(x) => ALL(a):[a in x => a=a]]
> > 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

On Saturday, June 3, 2023 at 2:13:41 PM UTC-4, Mild Shock wrote:
> I guess its rather the paradox of irrelevance.

Actually, it's not a paradox at all. It's more of a cautionary tale to avoid if possible constructs of the form ALL(a):[a in x & P]

> There are so many theorems that are irrelevant,
> und would never make it into a paper, since
>
> they use either inconsistent assumptions,

No inconsistent assumptions here.

> or then are non-construction and can therefore not be
> applied.

Constructive proofs are not usually required. The rules of logic that I use are widely accepted by the vast majority of mathematicians. Some rules may be rejected by certain elements outside the mainstream.

[snip childish abuse]

Dan

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

Maybe you have entered now the baby phase
that these behave similarly, since we have:

~ALL(a):[a e X] <=> EXIST(a):[~a e X]

How long will this baby phase last. Multiple
months? It only makes me marvel once again
whether you wrote DC proof by yourself.

Most likely you stole it, inherited it from someone
or got it by some other means. After all your
DC proof tools has these two inference rules:
- Quantifier switch (annoyingly introduces an extra negation sign)
- Double negation removal

So you should know quantifier duality of ALL and
EXIST sleep walking. But you are totally clueless and
extremly slow. That DC proof has many inference

rules that unnecessarely introduce a negation sign,
even if not necessary for classical logic, let me
already to the speculation that the real author

had some intuitionistic tool in mind, or that the present
author is an utter moron, who wants to terrorize the
users of DC proof if complete nonsense inference rules.

I am still undecided which of the stories behind DC proof
are true. Maybe both. When DC proof changed hands
nobody told the owner: Watch out intuitionistic inference

rules. And since the new owner doesnt know a damn
bit of intuitionistic logic, there is now this crank tool.

Mild Shock schrieb am Samstag, 3. Juni 2023 um 20:20:18 UTC+2:
> Also for a moron like you it might not be evident
> that you can replace a=a by TRUE. So you proved
> these two theorems:
>
> ~ALL(a):[a e X]
> TRUE
>
> The first theorem has not even a mosquito leg
> difference from your Universal Set theorem, at
> least not in classical logic. And the second theorem,
>
> is not something anybody would surprise.
> Mild Shock schrieb am Samstag, 3. Juni 2023 um 20:13:41 UTC+2:
> > I guess its rather the paradox of irrelevance.
> > There are so many theorems that are irrelevant,
> > und would never make it into a paper, since
> >
> > they use either inconsistent assumptions,
> > or then are non-construction and can therefore not be
> > applied. Are just some Unicorn dreams.
> >
> > Maybe post some math when have outgrown your
> > juvenile phase of 1000-th version of Russels paradox
> > which is totally irrelevant and useless to mathematics.
> > Dan Christensen schrieb am Samstag, 3. Juni 2023 um 19:33:09 UTC+2:
> > > Using ordinary set theory, we can prove:
> > >
> > > (1) ALL(a):[a in X & a=a] is FALSE for any set X.
> > >
> > > Whereas
> > >
> > > (2) ALL(a):[a in X => a=a]] is TRUE for any set X.
> > >
> > > ----------------------------------------------------------------------
> > > PROOF (1)
> > >
> > > Lemma: From Russel's Paradox (Proof: http://dcproof.com/UniversalSet.htm )
> > >
> > > 1. ALL(a):[Set(a) => EXIST(b):~b in a]
> > > Axiom
> > >
> > > Let x be a set
> > >
> > > 2. Set(x)
> > > Premise
> > >
> > > Apply lemma
> > >
> > > 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 | ~y=y
> > > Arb Or, 5
> > >
> > > 7. ~[~~y in x & ~~y=y]
> > > DeMorgan, 6
> > >
> > > 8. ~[y in x & ~~y=y]
> > > Rem DNeg, 7
> > >
> > > 9. ~[y in x & y=y]
> > > Rem DNeg, 8
> > >
> > > 10. ALL(x):[Set(x) => EXIST(a):~[a in x & a=a]]
> > > Conclusion, 2
> > >
> > > 11. ALL(x):[Set(x) => ~ALL(a):~~[a in x & a=a]]
> > > Quant, 10
> > >
> > > 12. ALL(x):[Set(x) => ~ALL(a):[a in x & a=a]]
> > > Rem DNeg, 11
> > >
> > > ----------------------------------------------------------------------
> > > PROOF (2)
> > >
> > > 1. Set(x)
> > > Premise
> > >
> > > 2. y in x
> > > Premise
> > >
> > > 3. y=y
> > > Reflex
> > >
> > > 4. ALL(a):[a in x => a=a]
> > > Conclusion, 2
> > >
> > > 5. ALL(x):[Set(x) => ALL(a):[a in x => a=a]]
> > > 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

On Saturday, June 3, 2023 at 11:17:55 AM UTC-7, Dan Christensen wrote:
> On Saturday, June 3, 2023 at 2:02:40 PM UTC-4, Ross Finlayson wrote:
> > On Saturday, June 3, 2023 at 10:33:09 AM UTC-7, Dan Christensen wrote:
> > > Using ordinary set theory, we can prove:
> > >
> > > (1) ALL(a):[a in X & a=a] is FALSE for any set X.
> > >
> > > Whereas
> > >
> > > (2) ALL(a):[a in X => a=a]] is TRUE for any set X.
> > >
> > > ----------------------------------------------------------------------
> > > PROOF (1)
> > >
> > > Lemma: From Russel's Paradox (Proof: http://dcproof.com/UniversalSet.htm )
> > >
> > > 1. ALL(a):[Set(a) => EXIST(b):~b in a]
> > > Axiom
> > >
> > > Let x be a set
> > >
> > > 2. Set(x)
> > > Premise
> > >
> > > Apply lemma
> > >
> > > 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 | ~y=y
> > > Arb Or, 5
> > >
> > > 7. ~[~~y in x & ~~y=y]
> > > DeMorgan, 6
> > >
> > > 8. ~[y in x & ~~y=y]
> > > Rem DNeg, 7
> > >
> > > 9. ~[y in x & y=y]
> > > Rem DNeg, 8
> > >
> > > 10. ALL(x):[Set(x) => EXIST(a):~[a in x & a=a]]
> > > Conclusion, 2
> > >
> > > 11. ALL(x):[Set(x) => ~ALL(a):~~[a in x & a=a]]
> > > Quant, 10
> > >
> > > 12. ALL(x):[Set(x) => ~ALL(a):[a in x & a=a]]
> > > Rem DNeg, 11
> > >
> > > ----------------------------------------------------------------------
> > > PROOF (2)
> > >
> > > 1. Set(x)
> > > Premise
> > >
> > > 2. y in x
> > > Premise
> > >
> > > 3. y=y
> > > Reflex
> > >
> > > 4. ALL(a):[a in x => a=a]
> > > Conclusion, 2
> > >
> > > 5. ALL(x):[Set(x) => ALL(a):[a in x => a=a]]
> > > 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
>
> > Maybe you should read Quine, even the introduction to his book
> > on set theory could help you,
> [snip]
>
> Thanks, but I'm not asking for any "help." I'm simply pointing why, in ordinary set theory (no classes), you should avoid constructs of the form ALL(a):[a in x & P]. They will always be false since every set must exclude some object.
> > he doesn't employ "material implication",
> [snip]
>
> I see no reason to avoid material implication for logical propositions that are unambiguously either true or false in the present.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

You're unequipped to deal with these "paradoxes" unless you
get them out of the way up front.

Your ignorance of the surrounds does not serve you well.

On Saturday, June 3, 2023 at 2:20:18 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:

[snip childish abuse]
> that you can replace a=a by TRUE.

"TRUE" is not usually used like this in textbook math proofs. Save it for your philosophy class, Mr. Collapse.

Dan

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

That Rossy Boys Herpes gets worse and worse is also
seen in your very recents posts. Although you like
writing posts with dual notions in it, you are

totally clueless when it comes to duality in logic.
You cannot recognize it sleep walking. If a post
does not contain the word dual directly, you

will not recognize it. The moron you are, you
will jump on every other keyword (here Equality,
Paradox) in a post. A little entertaining but also

very sad to see, since certain breaking of this duality plays
a role in intutionistic logic. Another name for
it, when quantifiers are involved, is the square of

opposition, which doesnt fully hold for intuitionistic logic.

Ross Finlayson schrieb am Samstag, 3. Juni 2023 um 20:47:41 UTC+2:
> On Saturday, June 3, 2023 at 11:17:55 AM UTC-7, Dan Christensen wrote:
> > On Saturday, June 3, 2023 at 2:02:40 PM UTC-4, Ross Finlayson wrote:
> > > On Saturday, June 3, 2023 at 10:33:09 AM UTC-7, Dan Christensen wrote:
> > > > Using ordinary set theory, we can prove:
> > > >
> > > > (1) ALL(a):[a in X & a=a] is FALSE for any set X.
> > > >
> > > > Whereas
> > > >
> > > > (2) ALL(a):[a in X => a=a]] is TRUE for any set X.
> > > >
> > > > ----------------------------------------------------------------------
> > > > PROOF (1)
> > > >
> > > > Lemma: From Russel's Paradox (Proof: http://dcproof.com/UniversalSet.htm )
> > > >
> > > > 1. ALL(a):[Set(a) => EXIST(b):~b in a]
> > > > Axiom
> > > >
> > > > Let x be a set
> > > >
> > > > 2. Set(x)
> > > > Premise
> > > >
> > > > Apply lemma
> > > >
> > > > 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 | ~y=y
> > > > Arb Or, 5
> > > >
> > > > 7. ~[~~y in x & ~~y=y]
> > > > DeMorgan, 6
> > > >
> > > > 8. ~[y in x & ~~y=y]
> > > > Rem DNeg, 7
> > > >
> > > > 9. ~[y in x & y=y]
> > > > Rem DNeg, 8
> > > >
> > > > 10. ALL(x):[Set(x) => EXIST(a):~[a in x & a=a]]
> > > > Conclusion, 2
> > > >
> > > > 11. ALL(x):[Set(x) => ~ALL(a):~~[a in x & a=a]]
> > > > Quant, 10
> > > >
> > > > 12. ALL(x):[Set(x) => ~ALL(a):[a in x & a=a]]
> > > > Rem DNeg, 11
> > > >
> > > > ----------------------------------------------------------------------
> > > > PROOF (2)
> > > >
> > > > 1. Set(x)
> > > > Premise
> > > >
> > > > 2. y in x
> > > > Premise
> > > >
> > > > 3. y=y
> > > > Reflex
> > > >
> > > > 4. ALL(a):[a in x => a=a]
> > > > Conclusion, 2
> > > >
> > > > 5. ALL(x):[Set(x) => ALL(a):[a in x => a=a]]
> > > > 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
> >
> > > Maybe you should read Quine, even the introduction to his book
> > > on set theory could help you,
> > [snip]
> >
> > Thanks, but I'm not asking for any "help." I'm simply pointing why, in ordinary set theory (no classes), you should avoid constructs of the form ALL(a):[a in x & P]. They will always be false since every set must exclude some object.
> > > he doesn't employ "material implication",
> > [snip]
> >
> > I see no reason to avoid material implication for logical propositions that are unambiguously either true or false in the present.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com
> You're unequipped to deal with these "paradoxes" unless you
> get them out of the way up front.
>
> Your ignorance of the surrounds does not serve you well.

I guess Rossy Boys Herpes has now jumped to you.

Dan Christensen schrieb am Samstag, 3. Juni 2023 um 20:56:23 UTC+2:
> On Saturday, June 3, 2023 at 2:20:18 PM UTC-4, Mild Shock (aka Mr.. Collapse) wrote:
>
> [snip childish abuse]
> > that you can replace a=a by TRUE.
> "TRUE" is not usually used like this in textbook math proofs. Save it for your philosophy class, Mr. Collapse.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Or to put it simple, so that you understand why your tool
makes people dumb, including yourself. Your tool doesn't
provide de Morgan rules. You cannot do with one click:

~(A v B) ~~> ~A & ~B

https://en.wikipedia.org/wiki/De_Morgan%27s_laws

You meed many many clicks, one click that replaces the
logical connective, and introduces a hell of new negation
signs, and a couple of other clicks to remove the double

negations. Same problem with quantifiers.

P.S.: It also wrongly labels rules as de Morgan, but its
not de Morgan in the sense of classical de Morgan laws.
Its something else. Here is an example:

1 ~[P | Q]
Premise

2 ~~[~P & ~Q]
DeMorgan, 1

3 ~P & ~Q
Rem DNeg, 2

Mild Shock schrieb am Samstag, 3. Juni 2023 um 20:58:39 UTC+2:
> I guess Rossy Boys Herpes has now jumped to you.
> Dan Christensen schrieb am Samstag, 3. Juni 2023 um 20:56:23 UTC+2:
> > On Saturday, June 3, 2023 at 2:20:18 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> >
> > [snip childish abuse]
> > > that you can replace a=a by TRUE.
> > "TRUE" is not usually used like this in textbook math proofs. Save it for your philosophy class, Mr. Collapse.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

That your tool provides intuitionistic de Morgan is explained here:

Three out of the four implications of de Morgan's laws hold in
intuitionistic logic.
https://en.wikipedia.org/wiki/De_Morgan%27s_laws#In_intuitionistic_logic

The workaround for intuitionistic logic is then to use for example:

A v B ~~> ~(~A & ~B)

This is also detailed on Wikipedia.

Dan Christensen schrieb:
> On Saturday, June 3, 2023 at 2:13:41 PM UTC-4, Mild Shock wrote:
>> I guess its rather the paradox of irrelevance.
>
>
> Actually, it's not a paradox at all. It's more of a cautionary tale to avoid if possible constructs of the form ALL(a):[a in x & P]
>
>
>> There are so many theorems that are irrelevant,
>> und would never make it into a paper, since
>>
>> they use either inconsistent assumptions,
>
> No inconsistent assumptions here.
>
>> or then are non-construction and can therefore not be
>> applied.
>
> Constructive proofs are not usually required. The rules of logic that I use are widely accepted by the vast majority of mathematicians. Some rules may be rejected by certain elements outside the mainstream.
>
> [snip childish abuse]
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>
>

On Saturday, June 3, 2023 at 2:42:39 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:

[snip childish abuse]

> DC proof tools has these two inference rules:
> - Quantifier switch (annoyingly introduces an extra negation sign)
> - Double negation removal
>

[snip childish abuse]

Maybe you didn't know, but both of these rules of logic are widely accepted by the vast majority of mathematicians.

Change universal to existential:

1. ALL(a):P(a)
Premise

2. ~EXIST(a):~P(a)
Quant, 1

3. ALL(a):P(a) => ~EXIST(a):~P(a)
Conclusion, 1

Change existential to universal:

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

2. ~ALL(a):~P(a)
Quant, 1

3. EXIST(a):P(a) => ~ALL(a):~P(a)
Conclusion, 1

Remove double negation
1. ~~P
Premise

2. P
Rem DNeg, 1

3. ~~P => P
Conclusion, 1

For some unknown reason, you have recently relegated yourself to the intuitionist fringes of mathematics, Mr. Collapse. Why would you do that?

Dan

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

You also need extra steps, in the form of double negation
removal, for quantifiers if they are negated. Here you see that:

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

2 ~~ALL(a):~P(a)
Quant, 1

3 ALL(a):~P(a)
Rem DNeg, 2

This is also detailed here, that this is the intuitionistic approach,
just check out what wikipedia writes about quantifiers:

https://en.wikipedia.org/wiki/De_Morgan%27s_laws#In_intuitionistic_logic

But since you are an uneducated fool, and have never teached
yourself the slightest bit of non-classical logic, you might
even not be aware of any of these things. You have possibly

never heard of the square of opposition and how it works out
in some non-classical logic. But why has your moron tool non-classical
inference rules? You sure you wrote it yourself?

Mild Shock schrieb:
> That your tool provides intuitionistic de Morgan is explained here:
>
> Three out of the four implications of de Morgan's laws hold in
> intuitionistic logic.
> https://en.wikipedia.org/wiki/De_Morgan%27s_laws#In_intuitionistic_logic
>
> The workaround for intuitionistic logic is then to use for example:
>
> A v B ~~> ~(~A & ~B)
>
> This is also detailed on Wikipedia.
>
> Dan Christensen schrieb:
>> On Saturday, June 3, 2023 at 2:13:41 PM UTC-4, Mild Shock wrote:
>>> I guess its rather the paradox of irrelevance.
>>
>>
>> Actually, it's not a paradox at all. It's more of a cautionary tale to
>> avoid if possible constructs of the form ALL(a):[a in x & P]
>>
>>
>>> There are so many theorems that are irrelevant,
>>> und would never make it into a paper, since
>>>
>>> they use either inconsistent assumptions,
>>
>> No inconsistent assumptions here.
>>
>>> or then are non-construction and can therefore not be
>>> applied.
>>
>> Constructive proofs are not usually required. The rules of logic that
>> I use are widely accepted by the vast majority of mathematicians. Some
>> rules may be rejected by certain elements outside the mainstream.
>>
>> [snip childish abuse]
>>
>> Dan
>>
>> Download my DC Proof 2.0 freeware at http://www.dcproof.com
>> Visit my Math Blog at http://www.dcproof.wordpress.com
>>
>>
>

On Saturday, June 3, 2023 at 3:08:53 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:

[snip childish abuse]

> Your tool doesn't
> provide de Morgan rules. You cannot do with one click:
>
> ~(A v B) ~~> ~A & ~B
>
[snip]

Wrong again, Mr. Collapse. See the De Morgan option on the Logic menu, Mr. Collapse.

OR ---> AND

1. A | B
Premise

2. ~[~A & ~B]
DeMorgan, 1

3. A | B => ~[~A & ~B]
Conclusion, 1

AND ---> OR

1. A & B
Premise

2. ~[~A | ~B]
DeMorgan, 1

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

On Saturday, June 3, 2023 at 3:12:47 PM UTC-4, Mild Shock wrote:
> That your tool provides intuitionistic de Morgan is explained here:
>
> Three out of the four implications of de Morgan's laws hold in
> intuitionistic logic.

[snip]

Not used in most textbook math proofs. Must be frustrating as hell for you.

Dan

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

On Saturday, June 3, 2023 at 2:47:41 PM UTC-4, Ross Finlayson wrote:
[snip]

> You're unequipped to deal with these "paradoxes" unless you
> get them out of the way up front.
>

As I told Mr. Collapse here, it's not a paradox at all. It's more of a cautionary tale to avoid if possible constructs of the form ALL(a):[a in x & P] since they will always be false regardless of the truth value of P.

Dan

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

Do you need glasses? What on earth
makes you think that what I picked here:

~(A v B) ~~> ~A & ~B
https://en.wikipedia.org/wiki/De_Morgan%27s_laws

Is NOT THE SAME as this nonsense:

Dan Christensen schrieb am Samstag, 3. Juni 2023 um 21:25:26 UTC+2:
> 3. A | B => ~[~A & ~B]
> Conclusion, 1
https://groups.google.com/g/sci.logic/c/8F9_EdEOXa0/m/1oKmQttZBgAJ

Its NOT THE SAME . You were supposed to
prove ~[A | B] => [~A & ~B]

Whats wrong with you? Still not getting
what the CLASSICAL de Morgan laws are,
and sticking to your INTUITINISTIC FRINGE?

(Your own words)

Dan Christensen schrieb:
> On Saturday, June 3, 2023 at 3:12:47 PM UTC-4, Mild Shock wrote:
>> That your tool provides intuitionistic de Morgan is explained here:
>>
>> Three out of the four implications of de Morgan's laws hold in
>> intuitionistic logic.
>
> [snip]
>
> Not used in most textbook math proofs. Must be frustrating as hell for you.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>

Do you need glasses? What on earth
makes you think that what I picked here:

~(A v B) ~~> ~A & ~B
https://en.wikipedia.org/wiki/De_Morgan%27s_laws

Is the same as this nonsense:

Dan Christensen schrieb am Samstag, 3. Juni 2023 um 21:25:26 UTC+2:
> 3. A | B => ~[~A & ~B]
> Conclusion, 1
https://groups.google.com/g/sci.logic/c/8F9_EdEOXa0/m/1oKmQttZBgAJ

Its NOT THE SAME . You were supposed to
prove ~[A | B] => [~A & ~B]

Whats wrong with you? Still not getting
what the CLASSICAL de Morgan laws are,
and sticking to your INTUITINISTIC FRINGE?

(Your own words)

Dan Christensen schrieb:
> On Saturday, June 3, 2023 at 3:12:47 PM UTC-4, Mild Shock wrote:
>> That your tool provides intuitionistic de Morgan is explained here:
>>
>> Three out of the four implications of de Morgan's laws hold in
>> intuitionistic logic.
>
> [snip]
>
> Not used in most textbook math proofs. Must be frustrating as hell for you.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>

On Saturday, June 3, 2023 at 3:41:42 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:

> Dan Christensen schrieb:
> > On Saturday, June 3, 2023 at 3:12:47 PM UTC-4, Mild Shock wrote:
> >> That your tool provides intuitionistic de Morgan is explained here:
> >>
> >> Three out of the four implications of de Morgan's laws hold in
> >> intuitionistic logic.
> >
> > [snip]
> >
> > Not used in most textbook math proofs. Must be frustrating as hell for you.
> >
> >

> Do you need glasses? What on earth
> makes you think that what I picked here:
> ~(A v B) ~~> ~A & ~B
> https://en.wikipedia.org/wiki/De_Morgan%27s_laws
>
> Is the same as this nonsense:
> Dan Christensen schrieb am Samstag, 3. Juni 2023 um 21:25:26 UTC+2:
> > 3. A | B => ~[~A & ~B]
> > Conclusion, 1
> https://groups.google.com/g/sci.logic/c/8F9_EdEOXa0/m/1oKmQttZBgAJ
>
> Its NOT THE SAME . You were supposed to
> prove ~[A | B] => [~A & ~B]
>
> Whats wrong with you?

It seems YOU are getting more desperate by the hour, Mr. Collapse!

There is nothing wrong the De Morgan rule in DC Proof. Or any other rules AFAIK. Must be frustrating as hell for you.

Dan

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

I didn't say that your inference rules
are not valid. They are clumsy nonsense.

And they don't deserve the name they have.
You can check yourself, the deMorgan laws

are other laws, like for example:

~(A v B) ~~> ~A & ~B
https://en.wikipedia.org/wiki/De_Morgan%27s_laws

I don't know how to care your dumbass tool.
You have to figure this out by yourself.

Good Luck!

Dan Christensen schrieb:
> On Saturday, June 3, 2023 at 3:41:42 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
>
>> Dan Christensen schrieb:
>>> On Saturday, June 3, 2023 at 3:12:47 PM UTC-4, Mild Shock wrote:
>>>> That your tool provides intuitionistic de Morgan is explained here:
>>>>
>>>> Three out of the four implications of de Morgan's laws hold in
>>>> intuitionistic logic.
>>>
>>> [snip]
>>>
>>> Not used in most textbook math proofs. Must be frustrating as hell for you.
>>>
>>>
>
>> Do you need glasses? What on earth
>> makes you think that what I picked here:
>> ~(A v B) ~~> ~A & ~B
>> https://en.wikipedia.org/wiki/De_Morgan%27s_laws
>>
>> Is the same as this nonsense:
>> Dan Christensen schrieb am Samstag, 3. Juni 2023 um 21:25:26 UTC+2:
>>> 3. A | B => ~[~A & ~B]
>>> Conclusion, 1
>> https://groups.google.com/g/sci.logic/c/8F9_EdEOXa0/m/1oKmQttZBgAJ
>>
>> Its NOT THE SAME . You were supposed to
>> prove ~[A | B] => [~A & ~B]
>>
>> Whats wrong with you?
>
> It seems YOU are getting more desperate by the hour, Mr. Collapse!
>
> There is nothing wrong the De Morgan rule in DC Proof. Or any other rules AFAIK. Must be frustrating as hell for you.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>

On Saturday, June 3, 2023 at 4:07:15 PM UTC-4, Mild Shock wrote:

> Dan Christensen schrieb:
> > On Saturday, June 3, 2023 at 3:41:42 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> >
> >> Dan Christensen schrieb:
> >>> On Saturday, June 3, 2023 at 3:12:47 PM UTC-4, Mild Shock wrote:
> >>>> That your tool provides intuitionistic de Morgan is explained here:
> >>>>
> >>>> Three out of the four implications of de Morgan's laws hold in
> >>>> intuitionistic logic.
> >>>
> >>> [snip]
> >>>
> >>> Not used in most textbook math proofs. Must be frustrating as hell for you.
> >>>
> >>>
> >
> >> Do you need glasses? What on earth
> >> makes you think that what I picked here:
> >> ~(A v B) ~~> ~A & ~B
> >> https://en.wikipedia.org/wiki/De_Morgan%27s_laws
> >>
> >> Is the same as this nonsense:
> >> Dan Christensen schrieb am Samstag, 3. Juni 2023 um 21:25:26 UTC+2:
> >>> 3. A | B => ~[~A & ~B]
> >>> Conclusion, 1
> >> https://groups.google.com/g/sci.logic/c/8F9_EdEOXa0/m/1oKmQttZBgAJ
> >>
> >> Its NOT THE SAME . You were supposed to
> >> prove ~[A | B] => [~A & ~B]
> >>
> >> Whats wrong with you?
> >
> > It seems YOU are getting more desperate by the hour, Mr. Collapse!
> >
> > There is nothing wrong the De Morgan rule in DC Proof. Or any other rules AFAIK. Must be frustrating as hell for you.
> >

> I didn't say that your inference rules
> are not valid.

Well, that's progress!

> They are clumsy nonsense.
>
[snip childish abuse]

There you go again, Mr. Collapse. The rules of inference of inference in DC Proof are designed to be easily learned and applied. Are you envious? How is that proof assistant of yours coming along? Maybe you are beginning to understand some basic principles of design for learning when you actually try to use your program? Who is your target audience anyway--philosophers or mathematicians? Beginners or experts? You really should decide before going any further.

Dan

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

Its pretty obvious that they are clumsy nonsense.
For example you implement only two rules:

EXIST(x):A(x) ~~> ~ALL(x):~A(x)
ALL(x):A(x) ~~~> ~EXIST(x):~A(x)

But the Greeks where already discussing the
square of opposition. Which hat 4 differnent

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

formulas to start with and not only two.
Notice something dumbo? So it wouldn't

cost you much to allow the end user to
additional perform the following operations:

a) If the end user clicks on a negation sign ~
in front of an EXIST, this rule fires:

~EXIST(x):A(x) ~~> ALL(x):~A(x)

b) If the end user clicks on a negation sign ~
in front of an ALL, this rule fires:

~ALL(x):A(x) ~~> EXIST(x):~A(x)

Hope this Helps!

Dan Christensen schrieb am Samstag, 3. Juni 2023 um 22:27:57 UTC+2:
> > They are clumsy nonsense.

The rules you implemented are even not part
of the square of opposition, nor part of de Morgan,
you implemented some replacement rules, the

balance of these rules is that they add two negation
signs, thats why they are clumsy:

/* Replacement Rules */
EXIST(x):A(x) ~~> ~ALL(x):~A(x)
ALL(x):A(x) ~~> ~EXIST(x):~A(x)

The square of opposition has these 4 rules,
the balance of these rules are that they remove
two negations, or keep the number of negations the same:

~EXIST(x):~A(x) ~~> ALL(x):A(x)
~ALL(x):~A(x) ~~> EXIST(x):A(x)
~EXIST(x):A(x) ~~> ALL(x):~A(x)
~ALL(x):A(x) ~~> EXIST(x):~A(x)
https://en.wikipedia.org/wiki/Square_of_opposition

Two of them are de Morgan. The de Morgan has these
4 rules. The balance of these rules is that they
always keep the number of negations the same:

ALL(x):~A(x) ~~> ~EXIST(x):A(x)
EXIST(x):~A(x) ~~> ~ALL(x):A(x)
~EXIST(x):A(x) ~~> ALL(x):~A(x)
~ALL(x):A(x) ~~> EXIST(x):~A(x)
https://en.wikipedia.org/wiki/De_Morgan%27s_laws

So you picked the worst inference rules, those
that add negation signs. Whereas for classical
logic there exist inference rules that remove

negation signs or keep the number of negation
signs constant. Well Shit Happens!

Mild Shock schrieb am Samstag, 3. Juni 2023 um 22:49:06 UTC+2:
> Its pretty obvious that they are clumsy nonsense.
> For example you implement only two rules:
>
> EXIST(x):A(x) ~~> ~ALL(x):~A(x)
> ALL(x):A(x) ~~~> ~EXIST(x):~A(x)
>
> But the Greeks where already discussing the
> square of opposition. Which hat 4 differnent
>
> https://en.wikipedia.org/wiki/Square_of_opposition
>
> formulas to start with and not only two.
> Notice something dumbo? So it wouldn't
>
> cost you much to allow the end user to
> additional perform the following operations:
>
> a) If the end user clicks on a negation sign ~
> in front of an EXIST, this rule fires:
>
> ~EXIST(x):A(x) ~~> ALL(x):~A(x)
>
> b) If the end user clicks on a negation sign ~
> in front of an ALL, this rule fires:
>
> ~ALL(x):A(x) ~~> EXIST(x):~A(x)
>
> Hope this Helps!
>
> Dan Christensen schrieb am Samstag, 3. Juni 2023 um 22:27:57 UTC+2:
> > > They are clumsy nonsense.