Did I find a formula in DC Proof that isn't provable,
but is provable in FOL? Not yet 100% sure.

Somehow a charming idea, although a little far fetched
I guess, that the Drinker Paradox would be ataching
device for quantifier scope? Maybe it is the smallest

formula which is a valid/invalid like here:

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

∃xDx → ∀yDy is invalid.
https://www.umsu.de/trees/#~7xDx~5~6yDy

Works also after Herbandization:

∃x(Dx → Df(x)) is valid.
https://www.umsu.de/trees/#~7x%28Dx~5Df%28x%29%29

∃xDx → Df is invalid.
https://www.umsu.de/trees/#~7xDx~5Df

Can we prove ∃x(Dx → Df(x)) in DC Proof? I guess it
is not possible, because of some set domain requirement
for f(x) in the tweaked forall rule of DC Proof.

What would be the DC Proof for ∃x(Dx → Df(x)) ?

Dan Christensen schrieb am Dienstag, 18. Oktober 2022 um 23:12:55 UTC+2:
> Minor bug fix. Release date: today.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Sunday, October 23, 2022 at 5:01:20 AM UTC-4, Mostowski Collapse wrote:
[snip]

>
> Can we prove ∃x(Dx → Df(x)) in DC Proof? I guess it
> is not possible, because of some set domain requirement
> for f(x) in the tweaked forall rule of DC Proof.
>

Yes, you really need to formally define the f.

Dan

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

f is a FOL function symbol. This here is provable in FOL:

∃x(Dx → Df(x)) is valid.
https://www.umsu.de/trees/#~7x%28Dx~5Df%28x%29%29

Can you prove it in DC Proof. It yields to another proof
of the drinker paradox. Which goes as follows:

1) Every guest points to some other guest, this is
the function f : V -> V, where V is "everybody".

2) Then we pick a random guest, call him c,
if ~Dc we are finished, i.e. if the guest is not a drinker,
the formula is true, because the material implication
makes it vacously true. c is suitable as a witness for ∃x.

3) On the other hand if Dc we check Df(c), i.e.
the guest the guest c is point to, i.e. f(c), if this
guest is a drinker, i.e. Df(c), we are also finished.
c is again suitable as a witness for ∃x.

4) If ~Df(c) then we are also finished, the formula
is true, because the material implication
makes it vacously true. This time f(c) is
suitable as a witness for ∃x.

Dan Christensen schrieb am Sonntag, 23. Oktober 2022 um 17:26:18 UTC+2:
> On Sunday, October 23, 2022 at 5:01:20 AM UTC-4, Mostowski Collapse wrote:
> [snip]
> >
> > Can we prove ∃x(Dx → Df(x)) in DC Proof? I guess it
> > is not possible, because of some set domain requirement
> > for f(x) in the tweaked forall rule of DC Proof.
> >
> Yes, you really need to formally define the f.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

FOL itself can prove this direction
of the Herbrandization:

(∃xPx → ∀yQy) → (∃xPx → Qf) is valid.
https://www.umsu.de/trees/#%28~7xPx~5~6yQy%29~5%28~7xPx~5Qf%29

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

For the second formula one can use
P=D and Q=D to get the Drinker Paradox.

The other direction needs a different f quantification,
than what is implicit in FOL. Don't know how to
show it with FOL, is this possible?

Mostowski Collapse schrieb am Montag, 24. Oktober 2022 um 00:41:19 UTC+2:
> f is a FOL function symbol. This here is provable in FOL:
> ∃x(Dx → Df(x)) is valid.
> https://www.umsu.de/trees/#~7x%28Dx~5Df%28x%29%29
> Can you prove it in DC Proof. It yields to another proof
> of the drinker paradox. Which goes as follows:
>
> 1) Every guest points to some other guest, this is
> the function f : V -> V, where V is "everybody".
>
> 2) Then we pick a random guest, call him c,
> if ~Dc we are finished, i.e. if the guest is not a drinker,
> the formula is true, because the material implication
> makes it vacously true. c is suitable as a witness for ∃x.
>
> 3) On the other hand if Dc we check Df(c), i.e.
> the guest the guest c is point to, i.e. f(c), if this
> guest is a drinker, i.e. Df(c), we are also finished.
> c is again suitable as a witness for ∃x.
>
> 4) If ~Df(c) then we are also finished, the formula
> is true, because the material implication
> makes it vacously true. This time f(c) is
> suitable as a witness for ∃x.
> Dan Christensen schrieb am Sonntag, 23. Oktober 2022 um 17:26:18 UTC+2:
> > On Sunday, October 23, 2022 at 5:01:20 AM UTC-4, Mostowski Collapse wrote:
> > [snip]
> > >
> > > Can we prove ∃x(Dx → Df(x)) in DC Proof? I guess it
> > > is not possible, because of some set domain requirement
> > > for f(x) in the tweaked forall rule of DC Proof.
> > >
> > Yes, you really need to formally define the f.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Wonky Man aka Dan Christensen halucinated:
> Moral of the story: In mathematics, it is probably
> a mistake to existentially quantify an implication

It was probably a mistake that your mother baught
you a computer with visual basic. Here is a proof
of the requested theorem in DC Proof:

19 EXIST(x):[D(x) => D(f(x))]
Rem DNeg, 18

For the full proof see here:

----------------- begin proof ------------------------------------

1 EXIST(x):x ε u
Axiom

2 ALL(x):[x ε u => f(x) ε u]
Axiom

3 ~EXIST(x):[D(x) => D(f(x))]
Premise

4 ~~ALL(x):~[D(x) => D(f(x))]
Quant, 3

5 ALL(x):~[D(x) => D(f(x))]
Rem DNeg, 4

6 ALL(x):~~[D(x) & ~D(f(x))]
Imply-And, 5

7 ALL(x):[D(x) & ~D(f(x))]
Rem DNeg, 6

8 a ε u
E Spec, 1

9 D(a) & ~D(f(a))
U Spec, 7

10 D(a)
Split, 9

11 ~D(f(a))
Split, 9

12 a ε u => f(a) ε u
U Spec, 2

13 f(a) ε u
Detach, 12, 8

14 D(f(a)) & ~D(f(f(a)))
U Spec, 7, 13

15 D(f(a))
Split, 14

16 ~D(f(f(a)))
Split, 14

17 ~D(f(a)) & D(f(a))
Join, 11, 15

18 ~~EXIST(x):[D(x) => D(f(x))]
Conclusion, 3

19 EXIST(x):[D(x) => D(f(x))]
Rem DNeg, 18

------------------ end proof --------------------------------------

Kibo better than Dr.Tao in math-- yet Kibo Parry M still believes 938 is 12% short of 945. But Dr. Terence Tao of UCLA, runs and hides, hides and runs whenever the question arises-- is slant cut of cone a ellipse or as AP proves-- it is a Oval. No, Dr. Tao should be drummed out of math completely. For here is the awful situation of a person not in math-- Kibo Parry M. who is on his way of the "realization slant cut of cone is a OVAL, never the ellipse". Yet there you have the idiot of math Dr. Tao at UCLA, run and hide, run Terry, hide Terry. Same thing can be said of Ruth Charney the recent head of AMS, run Ruth, hide Ruth, even though your so called specialty was geometry, Ruth, Ruth, run and hide.

On Sunday, October 23, 2022 at 12:51:25 AM UTC-5, Michael Moroney wrote:
> On 10/23/2022 1:06 AM, Earle Jones wrote:
> > *
> > Anyone who has taught mathematics at the college freshman level (as I have at Georgia Tech as a TA) went through the fairly simple process, using analytic geometry to define what is a conic section. If you can follow this, just perform these steps: First, write the definition of a cone (in x, y, z space). It is not difficult. Then, write the equation of an inclined plane in three-space. Then, if you have done the work accurately, you can solve these two equations simultaneously. That gives the locus of all points common to the cone and the inclined plane. (This is the definition of a section.) The resulting equation will be an ellipse, a circle, a parabola, or a hyperbola, depending on the exact inclined plane you have chosen. By the way, this was first demonstrated in about 300 BC, even before the original Archmedes (not the Plutonium version.)
> >
> > earle
> > *
> Plutonium's argument is based on axes of symmetry. While his so-called
> "proof" is rambling and in no way a valid math proof, its basic argument
> is a tilted plane intersecting a cone will have the side nearest the
> apex of the cone will be smaller than the side tilting away from the
> apex, simply because the cone itself gets smaller near the apex and
> larger away from it. Thus his "proof" is that the cone isn't symmetric
> _around the axis of the cone_. However the cone's formula will have
> something like (x-k)^2 in it, which is obviously symmetric around the
> x=k plane.
>
> I know if you look at a drawing, it doesn't look like it could be an
> ellipse. I think of this as like a "mathematical optical illusion".
>
> This is easier to visualize if the cone is tilted around the y axis,
> with its apex at the point (x=0,y=0,z=0) and is intersected by the plane
> z=m for some m.
>
>
> Here's a proof someone (I forget who) wrote earlier in response to AP,
> that tilts the cone and the cone is intersected by the plane
> z=<constant>. It may be unclear in the last line why that is the
> equation of an ellipse if C>0, but the left side is a constant, and the
> right side is C*(x-K)^2 + y^2, which is the formula of an ellipse. K=k*S/C.
>
>
>
> I'll start with the cone z^2 = x^2 + y^2, and rotate it through an angle
> 'theta' around the 'y' axis, and consider the intersection of that
> rotated cone with the plane z = <constant>
>
> To simplify things, let c = cos(theta) and s = sin(theta). Then the
> rotation is defined by
>
> z --> cz + sx
> x --> -sz + cx
> y --> y
>
> So the equation of the rotated cone is
>
> (cz+sx)^2 = (-sz+cx)^2 + y^2
>
> and now let C = c^2-s^2 and S = 2sc (again, just to simplify the look
> of things)
>
> so we get
>
> Cz^2 = Cx^2 - 2Szx + y^2
>
> and letting 'z' equal the constant 'k' gives
>
> Ck^2 + k^2*S^2/C = C(x - k*S/C)^2 + y^2
>
> which is the equation of an ellipse if C > 0.

On 10/23/2022 1:51 AM, Michael Moroney wrote:
> It may be unclear in the last line why that is the
> equation of an ellipse if C>0, but the left side is a constant, and the
> right side is C*(x-K)^2 + y^2, which is the formula of an ellipse. K=k*S/C.

This proof skips several steps before the last line, so it's far from
obvious. I will have to make it clearer, and add the skipped steps back in.

---------

Kibo of course is a loud math in sci.math and sci.physics and should never have posted but watched and listened.

3rd published book

AP's Proof-Ellipse was never a Conic Section // Math proof series, book 1 Kindle Edition
by Archimedes Plutonium (Author)

Ever since Ancient Greek Times it was thought the slant cut into a cone is the ellipse. That was false. For the slant cut in every cone is a Oval, never an Ellipse. This book is a proof that the slant cut is a oval, never the ellipse. A slant cut into the Cylinder is in fact a ellipse, but never in a cone.

Product details
• ASIN ‏ : ‎ B07PLSDQWC
• Publication date ‏ : ‎ March 11, 2019
• Language ‏ : ‎ English
• File size ‏ : ‎ 1621 KB
• Text-to-Speech ‏ : ‎ Enabled
• Enhanced typesetting ‏ : ‎ Enabled
• X-Ray ‏ : ‎ Not Enabled
• Word Wise ‏ : ‎ Not Enabled
• Print length ‏ : ‎ 20 pages
• Lending ‏ : ‎ Enabled
•
•

Proofs Ellipse is never a Conic section, always a Cylinder section and a Well Defined Oval definition//Student teaches professor series, book 5 Kindle Edition
by Archimedes Plutonium (Author)

Last revision was 14May2022. This is AP's 68th published book of science.

Preface: A similar book on single cone cut is a oval, never a ellipse was published in 11Mar2019 as AP's 3rd published book, but Amazon Kindle converted it to pdf file, and since then, I was never able to edit this pdf file, and decided rather than struggle and waste time, decided to leave it frozen as is in pdf format. Any new news or edition of ellipse is never a conic in single cone is now done in this book. The last thing a scientist wants to do is wade and waddle through format, when all a scientist ever wants to do is science itself. So all my new news and thoughts of Conic Sections is carried out in this 68th book of AP. And believe you me, I have plenty of new news.

In the course of 2019 through 2022, I have had to explain this proof often on Usenet, sci.math and sci.physics. And one thing that constant explaining does for a mind of science, is reduce the proof to its stripped down minimum format, to bare bones skeleton proof. I can prove the slant cut in single cone is a Oval, never the ellipse in just a one sentence proof. Proof-- A single cone and oval have just one axis of symmetry, while a ellipse requires 2 axes of symmetry, hence slant cut is always a oval, never the ellipse..

Product details
• ASIN ‏ : ‎ B081TWQ1G6
• Publication date ‏ : ‎ November 21, 2019
• Language ‏ : ‎ English
• File size ‏ : ‎ 827 KB
• Simultaneous device usage ‏ : ‎ Unlimited
• Text-to-Speech ‏ : ‎ Enabled
• Screen Reader ‏ : ‎ Supported
• Enhanced typesetting ‏ : ‎ Enabled
• X-Ray ‏ : ‎ Not Enabled
• Word Wise ‏ : ‎ Not Enabled
• Print length ‏ : ‎ 51 pages
• Lending ‏ : ‎ Enabled

#12-2, 11th published book

World's First Geometry Proof of Fundamental Theorem of Calculus// Math proof series, book 2 Kindle Edition
by Archimedes Plutonium (Author)

Last revision was 15Dec2021. This is AP's 11th published book of science.
Preface:
Actually my title is too modest, for the proof that lies within this book makes it the World's First Valid Proof of Fundamental Theorem of Calculus, for in my modesty, I just wanted to emphasis that calculus was geometry and needed a geometry proof. Not being modest, there has never been a valid proof of FTC until AP's 2015 proof. This also implies that only a geometry proof of FTC constitutes a valid proof of FTC.

Calculus needs a geometry proof of Fundamental Theorem of Calculus. But none could ever be obtained in Old Math so long as they had a huge mass of mistakes, errors, fakes and con-artist trickery such as the "limit analysis". And very surprising that most math professors cannot tell the difference between a "proving something" and that of "analyzing something". As if an analysis is the same as a proof. We often analyze various things each and every day, but few if none of us consider a analysis as a proof. Yet that is what happened in the science of mathematics where they took an analysis and elevated it to the stature of being a proof, when it was never a proof.

To give a Geometry Proof of Fundamental Theorem of Calculus requires math be cleaned-up and cleaned-out of most of math's mistakes and errors. So in a sense, a Geometry FTC proof is a exercise in Consistency of all of Mathematics. In order to prove a FTC geometry proof, requires throwing out the error filled mess of Old Math. Can the Reals be the true numbers of mathematics if the Reals cannot deliver a Geometry proof of FTC? Can the functions that are not polynomial functions allow us to give a Geometry proof of FTC? Can a Coordinate System in 2D have 4 quadrants and still give a Geometry proof of FTC? Can a equation of mathematics with a number that is _not a positive decimal Grid Number_ all alone on the right side of the equation, at all times, allow us to give a Geometry proof of the FTC?

On Sunday, October 23, 2022 at 6:41:19 PM UTC-4, Mostowski Collapse wrote:
> f is a FOL function symbol. This here is provable in FOL:
> ∃x(Dx → Df(x)) is valid.
> https://www.umsu.de/trees/#~7x%28Dx~5Df%28x%29%29

Only, it seems from your reply at sci.logic, if you make certain mysterious assumptions that you do not make explicit in your FOL "proof" They are somehow built into your FOL system and not visible to the reader. No wonder authors of math textbook authors felt they had to devise their own system of logic.

Dan

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

I just proved it:

Mostowski Collapse schrieb am Montag, 24. Oktober 2022 um 22:14:53 UTC+2:
> 19 EXIST(x):[D(x) => D(f(x))]
> Rem DNeg, 18
https://groups.google.com/g/sci.math/c/PwyRME9DOdY/m/4cA5lCPIBAAJ

Whats wrong with you? Do you say your proof is incorrect?

P.S.: I didn't mirror the mysterious domain, which also
exists in DC Proof, into a predicate, I didn't make an axiom:

ALL(x):U(x)

Does this make your DC Proof result mysterious and
a little occult, just as you claim FOL proofs are?

LMAO!

Dan Christensen schrieb am Dienstag, 25. Oktober 2022 um 02:24:46 UTC+2:
> On Sunday, October 23, 2022 at 6:41:19 PM UTC-4, Mostowski Collapse wrote:
> > f is a FOL function symbol. This here is provable in FOL:
> > ∃x(Dx → Df(x)) is valid.
> > https://www.umsu.de/trees/#~7x%28Dx~5Df%28x%29%29
> Only, it seems from your reply at sci.logic, if you make certain mysterious assumptions that you do not make explicit in your FOL "proof" They are somehow built into your FOL system and not visible to the reader. No wonder authors of math textbook authors felt they had to devise their own system of logic.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, October 25, 2022 at 1:15:06 PM UTC+2, Mostowski Collapse wrote:

> What's wrong with you? Do you say your proof is incorrect?
>
> P.S.: I didn't mirror the mysterious domain, which also
> exists in DC Proof, into a predicate, I didn't make an axiom:
>
> ALL(x):U(x)

On the other hand, this demented fool wrote HIMSELF:

> > [We] only have to prove: EXIST(b):[D(b) => ALL(a):D(a)]
> >
> > 1. EXIST(a):U(a)
> > Axiom
> > :

And it's indeed necessary to formulate something like this _in DC Proof_, otherweise you cannot prove an existence claim like

EXIST(b): ...b...

Now _he_ did't see any problems with _his_ axiom

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

[ but he is whining about your (quite innocent) axiom "EXIST(x):x ε u" ].

So _we_ now may ask:

> Does this make your DC Proof result mysterious and
> a little occult, just as you claim FOL proofs are?
>
> LMAO!

What an idiot!

On Tuesday, October 25, 2022 at 7:15:06 AM UTC-4, Mostowski Collapse wrote:

[snip]

> P.S.: I didn't mirror the mysterious domain, which also
> exists in DC Proof, into a predicate, I didn't make an axiom:
>
> ALL(x):U(x)
>

What Jan Burse has proven, in effect, is that:

ALL(u): ALL(f):[EXIST(x):x ε u & ALL(x):[x ε u => f(x) ε u]
=> EXIST(b):[D(b) => ALL(a):D(a)]]

In the FOL system, the first line is never made explicit. We are simply to imagine that something like this it is true -- a lazy philosopher's shortcut? Not a good basis for mathematical proof in any case.

The above result could have been obtained in DC Proof by using the Premise Rule instead of the Axiom Rule at the beginning of the proof.

Dan

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

On Tuesday, October 25, 2022 at 7:15:06 AM UTC-4, Mostowski Collapse wrote:

[snip]

> P.S.: I didn't mirror the mysterious domain, which also
> exists in DC Proof, into a predicate, I didn't make an axiom:
>
> ALL(x):U(x)
>

What Jan Burse has proven, in effect, is that:

ALL(u): ALL(f):[EXIST(x):x ε u & ALL(x):[x ε u => f(x) ε u]
=> EXIST(b):[D(b) => ALL(a):D(a)]]

In the FOL system, the first line is never made explicit. We are simply to imagine that something like this is true -- a lazy philosopher's shortcut? Not a good basis for mathematical proof in any case.

The above result could have been obtained in DC Proof by using the Premise Rule instead of the Axiom Rule at the beginning of the proof.

Dan

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

On Tuesday, October 25, 2022 at 3:02:17 PM UTC+2, Dan Christensen wrote:

> What Jan Burse has proven, in effect, is that:
>
> ALL(u): ALL(f): [EXIST(x):x ε u & ALL(x):[x ε u => f(x) ε u]
> => EXIST(b):[D(b) => ALL(a):D(a)]]
>
> In the FOL system, the first line is never made explicit.

Yeah, because it doesn't concern FOPL but set theory, you silly crank. Note that in pure FOPL we can't quantify over "functions". [If your DC Proof can do that it's not based on a system of first-order predicate logic. (Hint: Not even Free Logic can do that.)]

Wrong again. FOL doesn't assume:

EXIST(x):x ε u

Where do you see FOL assuming this?
It has 2 extra features, a) a membership relation
ε which is not part of FOL, b) a set object u,

which is not part of FOL. FOL doesn't talk about
sets. You still don't understand the difference
between predicates aka classes and sets, right?

What you could do in FOL, is the following:

EXIST(x):U(x)

It has only 1 extra feature a) a predicate symbol
U. And the result is relatively innocent, it doesn't
pressuppose membership or set objects.

Dan Christensen schrieb am Dienstag, 25. Oktober 2022 um 15:02:17 UTC+2:
> On Tuesday, October 25, 2022 at 7:15:06 AM UTC-4, Mostowski Collapse wrote:
>
> [snip]
> > P.S.: I didn't mirror the mysterious domain, which also
> > exists in DC Proof, into a predicate, I didn't make an axiom:
> >
> > ALL(x):U(x)
> >
> What Jan Burse has proven, in effect, is that:
>
> ALL(u): ALL(f):[EXIST(x):x ε u & ALL(x):[x ε u => f(x) ε u]
> => EXIST(b):[D(b) => ALL(a):D(a)]]
>
> In the FOL system, the first line is never made explicit. We are simply to imagine that something like this is true -- a lazy philosopher's shortcut? Not a good basis for mathematical proof in any case.
>
> The above result could have been obtained in DC Proof by using the Premise Rule instead of the Axiom Rule at the beginning of the proof.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

I think most authors avoid a new predicate symbol
all together, and try to capture the non-emptyness
of the domain of discourse by this statement:

EXIST(x):[x=x]

But this requires another feature, namely FOL with
equality, you could write it FOL=. Wolfgang Schwartz
tool implements FOL=, and you can prove:

∃xx=x is valid.
https://www.umsu.de/trees/#~7x%28x=x%29

If you further abbreviate. With ‘E!’ we can express classical logic’s
blanket presumption that singular terms denote members
of D, where D is the quantificational domain:

E!t :<=> ∃x(x=t)

Or in DC Proof:

Quantifiable(t) :<=> EXIST(x):[x=t]

You can also try another formula, to check whether the
quantificational domain is non-empty. You could try
this one as well, Rossy Boy mentioned it already:

∃yE!t

Or in DC Proof:

EXIST(y):Quantifiable(y)

Expand the definition of E!, it is also a provable in FOL:

∃y∃xx=y is valid.
https://www.umsu.de/trees/#~7y~7x%28x=y%29

The term quantificational domain appears when the
domain of discourse is split up, in those objects that
are reached via quantifier, and other objects that are

not, which could be an approach to certain logics.

See also:

SEP - Free Logic
https://plato.stanford.edu/entries/logic-free/

Mostowski Collapse schrieb am Dienstag, 25. Oktober 2022 um 16:28:59 UTC+2:
> Wrong again. FOL doesn't assume:
>
> EXIST(x):x ε u
>
> Where do you see FOL assuming this?
> It has 2 extra features, a) a membership relation
> ε which is not part of FOL, b) a set object u,
>
> which is not part of FOL. FOL doesn't talk about
> sets. You still don't understand the difference
> between predicates aka classes and sets, right?
>
> What you could do in FOL, is the following:
>
> EXIST(x):U(x)
>
> It has only 1 extra feature a) a predicate symbol
> U. And the result is relatively innocent, it doesn't
> pressuppose membership or set objects.
> Dan Christensen schrieb am Dienstag, 25. Oktober 2022 um 15:02:17 UTC+2:
> > On Tuesday, October 25, 2022 at 7:15:06 AM UTC-4, Mostowski Collapse wrote:
> >
> > [snip]
> > > P.S.: I didn't mirror the mysterious domain, which also
> > > exists in DC Proof, into a predicate, I didn't make an axiom:
> > >
> > > ALL(x):U(x)
> > >
> > What Jan Burse has proven, in effect, is that:
> >
> > ALL(u): ALL(f):[EXIST(x):x ε u & ALL(x):[x ε u => f(x) ε u]
> > => EXIST(b):[D(b) => ALL(a):D(a)]]
> >
> > In the FOL system, the first line is never made explicit. We are simply to imagine that something like this is true -- a lazy philosopher's shortcut? Not a good basis for mathematical proof in any case.
> >
> > The above result could have been obtained in DC Proof by using the Premise Rule instead of the Axiom Rule at the beginning of the proof.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

But free logics might have a defect.

4.2 Substitutivity Failures
Classical predicate logic has the desirable feature
that co-extensive open formulas may be substituted
for one another in any formula salva veritate—i.e.,
without changing that formula’s truth value.
https://plato.stanford.edu/entries/logic-free/#subfail

It could be that DC Proof has the same failure?
For example in FOL I can play around with making
definition as follows:

∀t(Qt ↔ ∃x(x=t))

There is a shift in the meaning now, since I use
a forall quantifier, which ranges over the quantificational
domain, the above does not anymore mean

singular term t. We also abused it already in Rossy
Boys formula, in that we supplied a variable to E!
in the example ∃yE!y. But in FOL we can prove:

∃y∃xx=y is valid.
https://www.umsu.de/trees/#~7y~7x%28x=y%29

But we can also prove this:

∀t(Qt ↔ ∃xx=t) → ∃yQy is valid.
https://www.umsu.de/trees/#~6t%28Qt~4~7x%28x=t%29%29~5~7yQy

Mostowski Collapse schrieb am Dienstag, 25. Oktober 2022 um 16:43:52 UTC+2:
> I think most authors avoid a new predicate symbol
> all together, and try to capture the non-emptyness
> of the domain of discourse by this statement:
>
> EXIST(x):[x=x]
>
> But this requires another feature, namely FOL with
> equality, you could write it FOL=. Wolfgang Schwartz
> tool implements FOL=, and you can prove:
>
> ∃xx=x is valid.
> https://www.umsu.de/trees/#~7x%28x=x%29
>
> If you further abbreviate. With ‘E!’ we can express classical logic’s
> blanket presumption that singular terms denote members
> of D, where D is the quantificational domain:
>
> E!t :<=> ∃x(x=t)
>
> Or in DC Proof:
>
> Quantifiable(t) :<=> EXIST(x):[x=t]
>
> You can also try another formula, to check whether the
> quantificational domain is non-empty. You could try
> this one as well, Rossy Boy mentioned it already:
>
> ∃yE!t
>
> Or in DC Proof:
>
> EXIST(y):Quantifiable(y)
>
> Expand the definition of E!, it is also a provable in FOL:
>
> ∃y∃xx=y is valid.
> https://www.umsu.de/trees/#~7y~7x%28x=y%29
>
> The term quantificational domain appears when the
> domain of discourse is split up, in those objects that
> are reached via quantifier, and other objects that are
>
> not, which could be an approach to certain logics.
>
> See also:
>
> SEP - Free Logic
> https://plato.stanford.edu/entries/logic-free/
> Mostowski Collapse schrieb am Dienstag, 25. Oktober 2022 um 16:28:59 UTC+2:
> > Wrong again. FOL doesn't assume:
> >
> > EXIST(x):x ε u
> >
> > Where do you see FOL assuming this?
> > It has 2 extra features, a) a membership relation
> > ε which is not part of FOL, b) a set object u,
> >
> > which is not part of FOL. FOL doesn't talk about
> > sets. You still don't understand the difference
> > between predicates aka classes and sets, right?
> >
> > What you could do in FOL, is the following:
> >
> > EXIST(x):U(x)
> >
> > It has only 1 extra feature a) a predicate symbol
> > U. And the result is relatively innocent, it doesn't
> > pressuppose membership or set objects.
> > Dan Christensen schrieb am Dienstag, 25. Oktober 2022 um 15:02:17 UTC+2:
> > > On Tuesday, October 25, 2022 at 7:15:06 AM UTC-4, Mostowski Collapse wrote:
> > >
> > > [snip]
> > > > P.S.: I didn't mirror the mysterious domain, which also
> > > > exists in DC Proof, into a predicate, I didn't make an axiom:
> > > >
> > > > ALL(x):U(x)
> > > >
> > > What Jan Burse has proven, in effect, is that:
> > >
> > > ALL(u): ALL(f):[EXIST(x):x ε u & ALL(x):[x ε u => f(x) ε u]
> > > => EXIST(b):[D(b) => ALL(a):D(a)]]
> > >
> > > In the FOL system, the first line is never made explicit. We are simply to imagine that something like this is true -- a lazy philosopher's shortcut? Not a good basis for mathematical proof in any case.
> > >
> > > The above result could have been obtained in DC Proof by using the Premise Rule instead of the Axiom Rule at the beginning of the proof.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, October 25, 2022 at 10:28:59 AM UTC-4, Mostowski Collapse wrote:
> Wrong again. FOL doesn't assume:
>
> EXIST(x):x ε u
>
> Where do you see FOL assuming this?
> It has 2 extra features, a) a membership relation
> ε which is not part of FOL, b) a set object u,
>

You introduced it in YOUR "proof", Jan Burse. Call it something else if you want, but it unnecessary in real-world mathematical proofs. You don't need it in real-world set theory. There, we have the much less mysterious subset axiom from which we can derive:

ALL(s):[Set(s) => EXIST(x):[x in s => Q]] for any proposition Q be it true or false.

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

Nothing very profound or all that useful except maybe as a cautionary tale about existential quantifiers: Usually existential quantifiers are attached to conjunctions, e.g. EXIST(a):[a in N & a+1=2], not to implications as above.

Dan

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

On Tuesday, October 25, 2022 at 6:35:35 PM UTC+2, Dan Christensen wrote:

> ALL(s):[Set(s) => EXIST(x):[x in s => Q]] for any proposition Q be it true or false.
>
> http://www.dcproof.com/STGeneralizedDrinkersThm.htm

This nonsense has nothing to do with the "Drinker Paradox" or "Drinker Prinziple", you silly crank.

Especially, since it relies on a "hidden assumption" (namely Zermelo's "subset axiom") you fucking idiot!

The "Drinking Prinziple" is a purely logical theorem.

Hint: "There is a certain principle which plays an important role in modern logic and which some of my graduate students have affectionately dubbed "The Drinking Principle." (Raymond Smullyan)

On Tuesday, October 25, 2022 at 1:21:12 PM UTC-4, Fritz Feldhase wrote:
> On Tuesday, October 25, 2022 at 6:35:35 PM UTC+2, Dan Christensen wrote:
>
> > ALL(s):[Set(s) => EXIST(x):[x in s => Q]] for any proposition Q be it true or false.
> >
> > http://www.dcproof.com/STGeneralizedDrinkersThm.htm

> This nonsense has nothing to do with the "Drinker Paradox" or "Drinker Prinziple" [snip childish abuse]
>
> Especially, since it relies on a "hidden assumption" (namely Zermelo's "subset axiom") [snip childish abuse]
>

You continue to desperately grasp at straws, Frtiz.

> The "Drinking Prinziple" is a purely logical theorem.
>
> Hint: "There is a certain principle which plays an important role in modern logic and which some of my GRADUATE students have affectionately dubbed "The Drinking Principle." (Raymond Smullyan)

I have presented a new, purely set-theoretic version that math UNDERGRADS (my target audience) should find much more accessible. Students have, after all, been familiar with set notation since childhood. Many if not most or all will never have been exposed to logical predicates. Deal with it.

Dan

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

There does not exist a set theoretic version of the Drinker
Paradox using Russell Paradox. You are grasping straws

Dan-O-Matik. What you did is the Water ruins Wine paradox.
The WrW paradox runs as follows:

"How fuck up a paradox beyond recognition in a few
strokes, and then ponder on the internet for years that
it is the original, even try to edit wikipedia, although nobody
believes you, even wikipedia didn't buy your bullshit."

Dan Christensen schrieb am Dienstag, 25. Oktober 2022 um 19:44:59 UTC+2:
> On Tuesday, October 25, 2022 at 1:21:12 PM UTC-4, Fritz Feldhase wrote:
> > On Tuesday, October 25, 2022 at 6:35:35 PM UTC+2, Dan Christensen wrote:
> >
> > > ALL(s):[Set(s) => EXIST(x):[x in s => Q]] for any proposition Q be it true or false.
> > >
> > > http://www.dcproof.com/STGeneralizedDrinkersThm.htm" rel="nofollow" target="_blank">http://www.dcproof.com/STGeneralizedDrinkersThm.htm
> > This nonsense has nothing to do with the "Drinker Paradox" or "Drinker Prinziple" [snip childish abuse]
> >
> > Especially, since it relies on a "hidden assumption" (namely Zermelo's "subset axiom") [snip childish abuse]
> >
>
> You continue to desperately grasp at straws, Frtiz.
> > The "Drinking Prinziple" is a purely logical theorem.
> >
> > Hint: "There is a certain principle which plays an important role in modern logic and which some of my GRADUATE students have affectionately dubbed "The Drinking Principle." (Raymond Smullyan)
>
> I have presented a new, purely set-theoretic version that math UNDERGRADS (my target audience) should find much more accessible. Students have, after all, been familiar with set notation since childhood. Many if not most or all will never have been exposed to logical predicates. Deal with it.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

About your audience, I guess its the same audience that
Wolfgang Mückenheim has. Poor students that must
endure a complete crank for 1 semester, but a student

does what a student must do, putting up with a stupid
professor is ok, if the grades or some other certificate
are ok. Kind of a stockholm syndrome:

> Stockholm syndrome is a theorized condition in
> which hostages develop a psychological bond with
> their captors during captivity.
> https://en.wikipedia.org/wiki/Stockholm_syndrome

Anyway we have YOU hostage Wonky Man here on
sci.logic and sci.math, raining hell on your bullshit.

Mostowski Collapse schrieb am Dienstag, 25. Oktober 2022 um 20:03:11 UTC+2:
> There does not exist a set theoretic version of the Drinker
> Paradox using Russell Paradox. You are grasping straws
>
> Dan-O-Matik. What you did is the Water ruins Wine paradox.
> The WrW paradox runs as follows:
>
> "How fuck up a paradox beyond recognition in a few
> strokes, and then ponder on the internet for years that
> it is the original, even try to edit wikipedia, although nobody
> believes you, even wikipedia didn't buy your bullshit."
> Dan Christensen schrieb am Dienstag, 25. Oktober 2022 um 19:44:59 UTC+2:
> > On Tuesday, October 25, 2022 at 1:21:12 PM UTC-4, Fritz Feldhase wrote:
> > > On Tuesday, October 25, 2022 at 6:35:35 PM UTC+2, Dan Christensen wrote:
> > >
> > > > ALL(s):[Set(s) => EXIST(x):[x in s => Q]] for any proposition Q be it true or false.
> > > >
> > > > http://www.dcproof.com/STGeneralizedDrinkersThm.htm" rel="nofollow" target="_blank">http://www.dcproof.com/STGeneralizedDrinkersThm.htm
> > > This nonsense has nothing to do with the "Drinker Paradox" or "Drinker Prinziple" [snip childish abuse]
> > >
> > > Especially, since it relies on a "hidden assumption" (namely Zermelo's "subset axiom") [snip childish abuse]
> > >
> >
> > You continue to desperately grasp at straws, Frtiz.
> > > The "Drinking Prinziple" is a purely logical theorem.
> > >
> > > Hint: "There is a certain principle which plays an important role in modern logic and which some of my GRADUATE students have affectionately dubbed "The Drinking Principle." (Raymond Smullyan)
> >
> > I have presented a new, purely set-theoretic version that math UNDERGRADS (my target audience) should find much more accessible. Students have, after all, been familiar with set notation since childhood. Many if not most or all will never have been exposed to logical predicates. Deal with it.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, October 25, 2022 at 2:03:11 PM UTC-4, Mostowski Collapse wrote:

[snip]

> > I have presented a new, purely set-theoretic version that math UNDERGRADS (my target audience) should find much more accessible. Students have, after all, been familiar with set notation since childhood. Many if not most or all will never have been exposed to logical predicates. Deal with it.

> There does not exist a set theoretic version of the Drinker
> Paradox using Russell Paradox. You are grasping straws
>

Still in denial, I see. Pathetic.

Given only that "drinkers" and "pub" are arbitrary sets, we have:

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

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

See my blog posting at https://dcproof.wordpress.com/2014/06/03/the-drinkers-paradox/

Read it and weep, Jan Burse.

Dan

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

On Tuesday, October 25, 2022 at 2:15:05 PM UTC-4, Mostowski Collapse wrote:

> Mostowski Collapse schrieb am Dienstag, 25. Oktober 2022 um 20:03:11 UTC+2:
> > There does not exist a set theoretic version of the Drinker
> > Paradox using Russell Paradox. You are grasping straws
> >
> > Dan-O-Matik. What you did is the Water ruins Wine paradox.
> > The WrW paradox runs as follows:
> >
> > "How fuck up a paradox beyond recognition in a few
> > strokes, and then ponder on the internet for years that
> > it is the original, even try to edit wikipedia, although nobody
> > believes you, even wikipedia didn't buy your bullshit."
> > Dan Christensen schrieb am Dienstag, 25. Oktober 2022 um 19:44:59 UTC+2:
> > > On Tuesday, October 25, 2022 at 1:21:12 PM UTC-4, Fritz Feldhase wrote:
> > > > On Tuesday, October 25, 2022 at 6:35:35 PM UTC+2, Dan Christensen wrote:
> > > >
> > > > > ALL(s):[Set(s) => EXIST(x):[x in s => Q]] for any proposition Q be it true or false.
> > > > >
> > > > > http://www.dcproof.com/STGeneralizedDrinkersThm.htm
> > > > This nonsense has nothing to do with the "Drinker Paradox" or "Drinker Prinziple" [snip childish abuse]
> > > >
> > > > Especially, since it relies on a "hidden assumption" (namely Zermelo's "subset axiom") [snip childish abuse]
> > > >
> > >
> > > You continue to desperately grasp at straws, Frtiz.
> > > > The "Drinking Prinziple" is a purely logical theorem.
> > > >
> > > > Hint: "There is a certain principle which plays an important role in modern logic and which some of my GRADUATE students have affectionately dubbed "The Drinking Principle." (Raymond Smullyan)
> > >
> > > I have presented a new, purely set-theoretic version that math UNDERGRADS (my target audience) should find much more accessible. Students have, after all, been familiar with set notation since childhood. Many if not most or all will never have been exposed to logical predicates. Deal with it.

> About your audience, I guess its the same audience that
> Wolfgang Mückenheim has. ...

[snip]
>
> Anyway we have YOU hostage Wonky Man here on
> sci.logic and sci.math, raining hell on your bullshit.

That "rain" is actually you pissing yourself, Jan Burse. HA, HA, HA!!!

Dan

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

Repeating bullshit doesn't make it less bullshit,
it only makes it more bullshit. We now have this
chemical equation how you created your bullshit:

WrW = DP + RP

Dan Christensen schrieb am Dienstag, 25. Oktober 2022 um 20:28:58 UTC+2:
> On Tuesday, October 25, 2022 at 2:03:11 PM UTC-4, Mostowski Collapse wrote:
>
> [snip]
> > > I have presented a new, purely set-theoretic version that math UNDERGRADS (my target audience) should find much more accessible. Students have, after all, been familiar with set notation since childhood. Many if not most or all will never have been exposed to logical predicates. Deal with it.
> > There does not exist a set theoretic version of the Drinker
> > Paradox using Russell Paradox. You are grasping straws
> >
> Still in denial, I see. Pathetic.
>
> Given only that "drinkers" and "pub" are arbitrary sets, we have:
>
> EXIST(x):[x in drinkers => ALL(a):[a in pub => a in drinkers]]
>
> http://www.dcproof.com/DrinkersThm1.htm" rel="nofollow" target="_blank">http://www.dcproof.com/DrinkersThm1.htm
>
> See my blog posting at https://dcproof.wordpress.com/2014/06/03/the-drinkers-paradox/
>
> Read it and weep, Jan Burse.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Because you are constantly repeating your bullshit we
have a new instance of John Gabriel, there is this analogy
of putting bullshit into the world, both dont work:

- John Gabriel: New Calculoose
- Dan Christensen: New Drinker (a typical Paraduck)

Mostowski Collapse schrieb am Dienstag, 25. Oktober 2022 um 21:03:18 UTC+2:
> Repeating bullshit doesn't make it less bullshit,
> it only makes it more bullshit. We now have this
> chemical equation how you created your bullshit:
>
> WrW = DP + RP
> Dan Christensen schrieb am Dienstag, 25. Oktober 2022 um 20:28:58 UTC+2:
> > On Tuesday, October 25, 2022 at 2:03:11 PM UTC-4, Mostowski Collapse wrote:
> >
> > [snip]
> > > > I have presented a new, purely set-theoretic version that math UNDERGRADS (my target audience) should find much more accessible. Students have, after all, been familiar with set notation since childhood. Many if not most or all will never have been exposed to logical predicates. Deal with it..
> > > There does not exist a set theoretic version of the Drinker
> > > Paradox using Russell Paradox. You are grasping straws
> > >
> > Still in denial, I see. Pathetic.
> >
> > Given only that "drinkers" and "pub" are arbitrary sets, we have:
> >
> > EXIST(x):[x in drinkers => ALL(a):[a in pub => a in drinkers]]
> >
> > http://www.dcproof.com/DrinkersThm1.htm" rel="nofollow" target="_blank">http://www.dcproof.com/DrinkersThm1.htm
> >
> > See my blog posting at https://dcproof.wordpress.com/2014/06/03/the-drinkers-paradox/
> >
> > Read it and weep, Jan Burse.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, October 25, 2022 at 9:04:58 PM UTC+2, Mostowski Collapse wrote:

> Because you are constantly repeating your bullshit we
> have a new instance of John Gabriel, there is this analogy
> of putting bullshit into the world, both don't work:
>
> - John Gabriel: New Calculoose
> - Dan Christensen: New Drinker (a typical Paraduck)

Completely agree with your assessment.

- WM: Dark numbers