On 10/18/2022 8:40 PM, Dan Christensen wrote:
> On Tuesday, October 18, 2022 at 11:01:20 PM UTC-4, Chris M. Thomasson wrote:
>> On 10/18/2022 5:01 PM, Dan Christensen wrote:
>>> On Tuesday, October 18, 2022 at 7:45:53 PM UTC-4, Chris M. Thomasson wrote:
>>>> On 10/18/2022 2:12 PM, Dan Christensen wrote:
>>>>> 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
>>>> Are you going to release your source code?
>>>
>>> No.
>>>
>>> Is it in VB 6?
>>>
>>> Yes.
>> I still have VB 6 installed on several old computers for maintaining
>> legacy DB programs from more than 20 years ago. Have you hooked it up
>> with msWord yet? Its fun to use the vbo, or was it vba? Create detailed
>> reports, all formatted and pretty. ;^) Have use used ms access? It
>> interfaces quite nicely with VB 6.
>
> Files in DC Proof are just low-tech flat (binary?) files. It has been a several years since I did anything with the file structure--not since I created the Windows version in 2004. Before that I had a VBDOS version, but it wasn't available online. The current version is a very small app--only about 1.2 Mb. The downloadable exe file (about 2.9 Mb) can be downloaded and installed in less than a minute with a high speed connection.

When you get some free time to burn, and are really bored... Try
creating output using msword wrt your existing vb6 code and making your
reports of a proof very pretty. Vb6 can talk to msword, access, excel,
ect... Like a glorified report generator. That's what I did a long time
ago wrt a inspection system for houses/pools/ect... I had a very large
database about comments, and codes, and local codes, ect... Fence
heights around a pool, ect... something you could get sued for if there
was one mistake. I could create deep narrative reports, and short action
item like reports. The comments were important because they had to be up
to current code, and still have to! I still maintain the database and
software. Even have a farm of old computers running the code. Actually,
I got up to 90% of it working on win11. DosBox was useful.

Maybe do SET SPACES before you do FUNCTION SPACES.
So far, from judging how you deal with the Drinker Paradox,
you didn't notice that your Set(_):

The s such that Set(s)

Doesn't span a lattice. It only spans an incomplete-lattice. This
explains why Set(_) cannot cover the below scenario
when its not further restricted:

Universe = {Anna, Bert, Carlo}
Drinkers = {Anna, Bert, Carlo}

What is an incomplete-lattice?
https://en.wikipedia.org/wiki/Complete_lattice

Making Russells paradox key for the Drinker Paradox,
clearly indicates that you used the wrong lattice for
modelling the Drinker Paradox.

A lattice with only bottom and no top.

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 Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
> Maybe do SET SPACES before you do FUNCTION SPACES.
> So far, from judging how you deal with the Drinker Paradox,
> you didn't notice that your Set(_):
>
> The s such that Set(s)
>
> Doesn't span a lattice. It only spans an incomplete-lattice. This
> explains why Set(_) cannot cover the below scenario
> when its not further restricted:
>
> Universe = {Anna, Bert, Carlo}
> Drinkers = {Anna, Bert, Carlo}
>

You really seem to be grasping at straws here, Mr. Collapse. What do you hope to prove by giving a set two different names? That they are equal? Universe = Drinkers? Very unimpressive.

> What is an incomplete-lattice?
> https://en.wikipedia.org/wiki/Complete_lattice
>
> Making Russells paradox key for the Drinker Paradox,
[snip]

An application on RP allows you to easily prove that, for any set S and proposition Q (be it true or false), we have EXIST(x):[x in S => Q]

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

Deal with it, Mr. Collapse. And get a life!

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, May 6, 2023 at 6:06:08 PM UTC-4, Dan Christensen wrote:
> On Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
> > Maybe do SET SPACES before you do FUNCTION SPACES.
> > So far, from judging how you deal with the Drinker Paradox,
> > you didn't notice that your Set(_):
> >
> > The s such that Set(s)
> >

Some objects, say the number 4, are not usually considered to be sets. Unlike actual sets, 4 does not, for example, have a powerset. In DC Proof, the Powerset Axiom is applicable only to objects that have been declared to be a set by means of the Set predicate. Likewise the other axioms of set theory in DC Proof.

EXAMPLE

Let x be a set

1. Set(x)
Premise

Construct the power set of x

Apply the Power Set Axiom

2. ALL(a):[Set(a) => EXIST(b):[Set(b)
& ALL(c):[c in b <=> Set(c) & ALL(d):[d in c => d in a]]]]
Power Set

Specify x

3. Set(x) => EXIST(b):[Set(b)
& ALL(c):[c in b <=> Set(c) & ALL(d):[d in c => d in x]]]
U Spec, 2

4. EXIST(b):[Set(b)
& ALL(c):[c in b <=> Set(c) & ALL(d):[d in c => d in x]]]
Detach, 3, 1

Define: px (the power set of x)

5. Set(px)
& ALL(c):[c in px <=> Set(c) & ALL(d):[d in c => d in x]]
E Spec, 4

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 wrote :
> On Saturday, May 6, 2023 at 6:06:08 PM UTC-4, Dan Christensen wrote:
>> On Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
>>> Maybe do SET SPACES before you do FUNCTION SPACES.
>>> So far, from judging how you deal with the Drinker Paradox,
>>> you didn't notice that your Set(_):
>>>
>>> The s such that Set(s)
>>>
>
> Some objects, say the number 4, are not usually considered to be sets.

Under Frege, Zermelo, and von Neumann they are.

On Saturday, May 6, 2023 at 8:28:10 PM UTC-4, FromTheRafters wrote:
> Dan Christensen wrote :
> > On Saturday, May 6, 2023 at 6:06:08 PM UTC-4, Dan Christensen wrote:
> >> On Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
> >>> Maybe do SET SPACES before you do FUNCTION SPACES.
> >>> So far, from judging how you deal with the Drinker Paradox,
> >>> you didn't notice that your Set(_):
> >>>
> >>> The s such that Set(s)
> >>>
> >
> > Some objects, say the number 4, are not usually considered to be sets.

> Under Frege, Zermelo, and von Neumann they are.

Reflecting the more common usage of today...

"[A]mong all the objects studied in mathematics, some of the objects happen to be sets; and if x is an object and A is a set, then either x ∈ A is true or x ∈ A is false. (If A is not a set, we leave the statement x ∈ A undefined; for instance, we consider the statement 3 ∈ 4 to neither be true or false, but simply meaningless, since 4 is not a set.)"
--Terence Tao, "Analysis I," p.34

Dan

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

Thats not relevant to being a complete lattice.
Your predicate Set(_) spans a class of sets which
is not a complete lattice:

Counter Example to Being a complete lattice:
ALL(s):[Set(s) => EXIST(a):~a e s]
http://www.dcproof.com/UniversalSet.htm

If the predicate Set(_) would span a class of sets,
which would be a complete lattice, we would
have some element in the lattice which is the

top, which can be expressed as:

EXIST(s):[Set(s) & ALL(a):[a e s]]

Thats is why your Set(_) alone is not suitable
for the drinker paradox. Because intuitively we
expect a complete lattice, so that scenarios

such as the following are possible:

Universe = {Anna, Bert}
Drinkers = {Anna, Bert}

Dan Christensen schrieb am Sonntag, 7. Mai 2023 um 05:31:04 UTC+2:
> On Saturday, May 6, 2023 at 8:28:10 PM UTC-4, FromTheRafters wrote:
> > Dan Christensen wrote :
> > > On Saturday, May 6, 2023 at 6:06:08 PM UTC-4, Dan Christensen wrote:
> > >> On Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
> > >>> Maybe do SET SPACES before you do FUNCTION SPACES.
> > >>> So far, from judging how you deal with the Drinker Paradox,
> > >>> you didn't notice that your Set(_):
> > >>>
> > >>> The s such that Set(s)
> > >>>
> > >
> > > Some objects, say the number 4, are not usually considered to be sets..
>
> > Under Frege, Zermelo, and von Neumann they are.
> Reflecting the more common usage of today...
>
> "[A]mong all the objects studied in mathematics, some of the objects happen to be sets; and if x is an object and A is a set, then either x ∈ A is true or x ∈ A is false. (If A is not a set, we leave the statement x ∈ A undefined; for instance, we consider the statement 3 ∈ 4 to neither be true or false, but simply meaningless, since 4 is not a set.)"
> --Terence Tao, "Analysis I," p.34
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

The finite complete boolean lattice for the

Universe = {Anna, Bert}

isn't a moon walk, you can depict it asfollows, it
shows the possible Drinkers configurations:

____{Anna, Bert}
___/ ____________\
{Anna}________{Bert}
___\____________/
_________{}

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

So that Dan Christensen can apply the Russell Paradox
to the Drinker Paradox, is because of his error that
he doesn't take Drinkers from a complete lattice.

The fix isn't that difficult though.

Mostowski Collapse schrieb am Sonntag, 7. Mai 2023 um 11:35:19 UTC+2:
> Thats not relevant to being a complete lattice.
> Your predicate Set(_) spans a class of sets which
> is not a complete lattice:
>
> Counter Example to Being a complete lattice:
> ALL(s):[Set(s) => EXIST(a):~a e s]
> http://www.dcproof.com/UniversalSet.htm" rel="nofollow" target="_blank">http://www.dcproof.com/UniversalSet.htm
>
> If the predicate Set(_) would span a class of sets,
> which would be a complete lattice, we would
> have some element in the lattice which is the
>
> top, which can be expressed as:
>
> EXIST(s):[Set(s) & ALL(a):[a e s]]
>
> Thats is why your Set(_) alone is not suitable
> for the drinker paradox. Because intuitively we
> expect a complete lattice, so that scenarios
>
> such as the following are possible:
>
> Universe = {Anna, Bert}
> Drinkers = {Anna, Bert}
> Dan Christensen schrieb am Sonntag, 7. Mai 2023 um 05:31:04 UTC+2:
> > On Saturday, May 6, 2023 at 8:28:10 PM UTC-4, FromTheRafters wrote:
> > > Dan Christensen wrote :
> > > > On Saturday, May 6, 2023 at 6:06:08 PM UTC-4, Dan Christensen wrote:
> > > >> On Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
> > > >>> Maybe do SET SPACES before you do FUNCTION SPACES.
> > > >>> So far, from judging how you deal with the Drinker Paradox,
> > > >>> you didn't notice that your Set(_):
> > > >>>
> > > >>> The s such that Set(s)
> > > >>>
> > > >
> > > > Some objects, say the number 4, are not usually considered to be sets.
> >
> > > Under Frege, Zermelo, and von Neumann they are.
> > Reflecting the more common usage of today...
> >
> > "[A]mong all the objects studied in mathematics, some of the objects happen to be sets; and if x is an object and A is a set, then either x ∈ A is true or x ∈ A is false. (If A is not a set, we leave the statement x ∈ A undefined; for instance, we consider the statement 3 ∈ 4 to neither be true or false, but simply meaningless, since 4 is not a set.)"
> > --Terence Tao, "Analysis I," p.34
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

It happens that Dan Christensen formulated :
> On Saturday, May 6, 2023 at 8:28:10 PM UTC-4, FromTheRafters wrote:
>> Dan Christensen wrote :
>>> On Saturday, May 6, 2023 at 6:06:08 PM UTC-4, Dan Christensen wrote:
>>>> On Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
>>>>> Maybe do SET SPACES before you do FUNCTION SPACES.
>>>>> So far, from judging how you deal with the Drinker Paradox,
>>>>> you didn't notice that your Set(_):
>>>>>
>>>>> The s such that Set(s)
>>>>>
>>>
>>> Some objects, say the number 4, are not usually considered to be sets.
>
>> Under Frege, Zermelo, and von Neumann they are.
>
> Reflecting the more common usage of today...
>
> "[A]mong all the objects studied in mathematics, some of the objects happen
> to be sets; and if x is an object and A is a set, then either x ∈ A is true
> or x ∈ A is false. (If A is not a set, we leave the statement x ∈ A
> undefined; for instance, we consider the statement 3 ∈ 4 to neither be true
> or false, but simply meaningless, since 4 is not a set.)" --Terence Tao,
> "Analysis I," p.34

Oh, *that* set theory.

On Sunday, May 7, 2023 at 7:31:14 AM UTC-4, FromTheRafters wrote:
> It happens that Dan Christensen formulated :
> > On Saturday, May 6, 2023 at 8:28:10 PM UTC-4, FromTheRafters wrote:
> >> Dan Christensen wrote :
> >>> On Saturday, May 6, 2023 at 6:06:08 PM UTC-4, Dan Christensen wrote:
> >>>> On Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
> >>>>> Maybe do SET SPACES before you do FUNCTION SPACES.
> >>>>> So far, from judging how you deal with the Drinker Paradox,
> >>>>> you didn't notice that your Set(_):
> >>>>>
> >>>>> The s such that Set(s)
> >>>>>
> >>>
> >>> Some objects, say the number 4, are not usually considered to be sets..
> >
> >> Under Frege, Zermelo, and von Neumann they are.
> >
> > Reflecting the more common usage of today...
> >
> > "[A]mong all the objects studied in mathematics, some of the objects happen
> > to be sets; and if x is an object and A is a set, then either x ∈ A is true
> > or x ∈ A is false. (If A is not a set, we leave the statement x ∈ A
> > undefined; for instance, we consider the statement 3 ∈ 4 to neither be true
> > or false, but simply meaningless, since 4 is not a set.)" --Terence Tao,
> > "Analysis I," p.34
> Oh, *that* set theory.

Terry seems to have done well by it. I have attempted to formalize it in my DC Proof system. It seems to work.

Dan

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

You used it wrongly for the drinker paradox. Even Terrence Tao
doesn't make the same blunder. You don't find him use Set(_).
Even not implicitly when he talks about an arbitrary subset like here:

/* Terrence Tao rather uses s ⊆ U */
> Exercise 10.3.5 from Analysis Vol.1 by Terence Tao.
> Give an example of a subset X⊆R and a function f:X→R
> which is differentiable on X, is such that f′(x)>0
> for all x∈X, but f is not strictly monotone increasing.

Maybe the problem is that DC Proof has only ∈ set membership,
and not ⊆ subset relationship. There is surely something missing
in your dealing with sets, you are subject to some mental

blockade. Whereas you have no problem to somehow adopt
the notion of a function space, i.e. to have some approaches
to what one usually writes:

/* A Mountain Dan O Matik tried to clime */
f : A -> B

You seem to be totally obnoxious of set spaces. What
would one write for drinkers, so that they are from a
complete boolean lattice?

/* Mountain of Ignorance for Dan O Matik */
drinkers : ??

Can you tell us?

Dan Christensen schrieb am Sonntag, 7. Mai 2023 um 16:33:00 UTC+2:
> On Sunday, May 7, 2023 at 7:31:14 AM UTC-4, FromTheRafters wrote:
> > It happens that Dan Christensen formulated :
> > > On Saturday, May 6, 2023 at 8:28:10 PM UTC-4, FromTheRafters wrote:
> > >> Dan Christensen wrote :
> > >>> On Saturday, May 6, 2023 at 6:06:08 PM UTC-4, Dan Christensen wrote:
> > >>>> On Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
> > >>>>> Maybe do SET SPACES before you do FUNCTION SPACES.
> > >>>>> So far, from judging how you deal with the Drinker Paradox,
> > >>>>> you didn't notice that your Set(_):
> > >>>>>
> > >>>>> The s such that Set(s)
> > >>>>>
> > >>>
> > >>> Some objects, say the number 4, are not usually considered to be sets.
> > >
> > >> Under Frege, Zermelo, and von Neumann they are.
> > >
> > > Reflecting the more common usage of today...
> > >
> > > "[A]mong all the objects studied in mathematics, some of the objects happen
> > > to be sets; and if x is an object and A is a set, then either x ∈ A is true
> > > or x ∈ A is false. (If A is not a set, we leave the statement x ∈ A
> > > undefined; for instance, we consider the statement 3 ∈ 4 to neither be true
> > > or false, but simply meaningless, since 4 is not a set.)" --Terence Tao,
> > > "Analysis I," p.34
> > Oh, *that* set theory.
> Terry seems to have done well by it. I have attempted to formalize it in my DC Proof system. It seems to work.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Could you define:

ALL(a):ALL(b):[a ⊆ b <=> ALL(x):[x ∈ a => x ∈ b]]

And then infer in DC Poop:

Set(U) & D ⊆ U => Set(D) ?

Maybe via power set axiom? Is this possible to infer
a certain transitivity of the Set(_) property along the
subset relationship ⊆ ? Didn't check exactly how

ZFCU works. ZFCU is ZFC with U-relements:

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

Mostowski Collapse schrieb am Sonntag, 7. Mai 2023 um 17:36:53 UTC+2:
> You used it wrongly for the drinker paradox. Even Terrence Tao
> doesn't make the same blunder. You don't find him use Set(_).
> Even not implicitly when he talks about an arbitrary subset like here:
>
> /* Terrence Tao rather uses s ⊆ U */
> > Exercise 10.3.5 from Analysis Vol.1 by Terence Tao.
> > Give an example of a subset X⊆R and a function f:X→R
> > which is differentiable on X, is such that f′(x)>0
> > for all x∈X, but f is not strictly monotone increasing.
>
> Maybe the problem is that DC Proof has only ∈ set membership,
> and not ⊆ subset relationship. There is surely something missing
> in your dealing with sets, you are subject to some mental
>
> blockade. Whereas you have no problem to somehow adopt
> the notion of a function space, i.e. to have some approaches
> to what one usually writes:
>
> /* A Mountain Dan O Matik tried to clime */
> f : A -> B
>
> You seem to be totally obnoxious of set spaces. What
> would one write for drinkers, so that they are from a
> complete boolean lattice?
>
> /* Mountain of Ignorance for Dan O Matik */
> drinkers : ??
>
> Can you tell us?
> Dan Christensen schrieb am Sonntag, 7. Mai 2023 um 16:33:00 UTC+2:
> > On Sunday, May 7, 2023 at 7:31:14 AM UTC-4, FromTheRafters wrote:
> > > It happens that Dan Christensen formulated :
> > > > On Saturday, May 6, 2023 at 8:28:10 PM UTC-4, FromTheRafters wrote:
> > > >> Dan Christensen wrote :
> > > >>> On Saturday, May 6, 2023 at 6:06:08 PM UTC-4, Dan Christensen wrote:
> > > >>>> On Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
> > > >>>>> Maybe do SET SPACES before you do FUNCTION SPACES.
> > > >>>>> So far, from judging how you deal with the Drinker Paradox,
> > > >>>>> you didn't notice that your Set(_):
> > > >>>>>
> > > >>>>> The s such that Set(s)
> > > >>>>>
> > > >>>
> > > >>> Some objects, say the number 4, are not usually considered to be sets.
> > > >
> > > >> Under Frege, Zermelo, and von Neumann they are.
> > > >
> > > > Reflecting the more common usage of today...
> > > >
> > > > "[A]mong all the objects studied in mathematics, some of the objects happen
> > > > to be sets; and if x is an object and A is a set, then either x ∈ A is true
> > > > or x ∈ A is false. (If A is not a set, we leave the statement x ∈ A
> > > > undefined; for instance, we consider the statement 3 ∈ 4 to neither be true
> > > > or false, but simply meaningless, since 4 is not a set.)" --Terence Tao,
> > > > "Analysis I," p.34
> > > Oh, *that* set theory.
> > Terry seems to have done well by it. I have attempted to formalize it in my DC Proof system. It seems to work.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Possibly the powerset axiom helps in deriving

Set(U) & D ⊆ U => Set(D)

It says in DC Proof:

1 ALL(a):[Set(a) => EXIST(b):[Set(b)
& ALL(c):[c ∈ b <=> Set(c) & ALL(d):[d ∈ c => d ∈ a]]]]
Power Set

But if you had also ⊆, you could define it easier as follows:

1 ALL(a):[Set(a) => EXIST(b):[Set(b)
& ALL(c):[c ∈ b <=> Set(c) & c ⊆ a]]]
Power Set

Mostowski Collapse schrieb am Sonntag, 7. Mai 2023 um 17:43:36 UTC+2:
> Could you define:
>
> ALL(a):ALL(b):[a ⊆ b <=> ALL(x):[x ∈ a => x ∈ b]]
>
> And then infer in DC Poop:
>
> Set(U) & D ⊆ U => Set(D) ?
>
> Maybe via power set axiom? Is this possible to infer
> a certain transitivity of the Set(_) property along the
> subset relationship ⊆ ? Didn't check exactly how
>
> ZFCU works. ZFCU is ZFC with U-relements:
>
> https://en.wikipedia.org/wiki/Urelement
> Mostowski Collapse schrieb am Sonntag, 7. Mai 2023 um 17:36:53 UTC+2:
> > You used it wrongly for the drinker paradox. Even Terrence Tao
> > doesn't make the same blunder. You don't find him use Set(_).
> > Even not implicitly when he talks about an arbitrary subset like here:
> >
> > /* Terrence Tao rather uses s ⊆ U */
> > > Exercise 10.3.5 from Analysis Vol.1 by Terence Tao.
> > > Give an example of a subset X⊆R and a function f:X→R
> > > which is differentiable on X, is such that f′(x)>0
> > > for all x∈X, but f is not strictly monotone increasing.
> >
> > Maybe the problem is that DC Proof has only ∈ set membership,
> > and not ⊆ subset relationship. There is surely something missing
> > in your dealing with sets, you are subject to some mental
> >
> > blockade. Whereas you have no problem to somehow adopt
> > the notion of a function space, i.e. to have some approaches
> > to what one usually writes:
> >
> > /* A Mountain Dan O Matik tried to clime */
> > f : A -> B
> >
> > You seem to be totally obnoxious of set spaces. What
> > would one write for drinkers, so that they are from a
> > complete boolean lattice?
> >
> > /* Mountain of Ignorance for Dan O Matik */
> > drinkers : ??
> >
> > Can you tell us?
> > Dan Christensen schrieb am Sonntag, 7. Mai 2023 um 16:33:00 UTC+2:
> > > On Sunday, May 7, 2023 at 7:31:14 AM UTC-4, FromTheRafters wrote:
> > > > It happens that Dan Christensen formulated :
> > > > > On Saturday, May 6, 2023 at 8:28:10 PM UTC-4, FromTheRafters wrote:
> > > > >> Dan Christensen wrote :
> > > > >>> On Saturday, May 6, 2023 at 6:06:08 PM UTC-4, Dan Christensen wrote:
> > > > >>>> On Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
> > > > >>>>> Maybe do SET SPACES before you do FUNCTION SPACES.
> > > > >>>>> So far, from judging how you deal with the Drinker Paradox,
> > > > >>>>> you didn't notice that your Set(_):
> > > > >>>>>
> > > > >>>>> The s such that Set(s)
> > > > >>>>>
> > > > >>>
> > > > >>> Some objects, say the number 4, are not usually considered to be sets.
> > > > >
> > > > >> Under Frege, Zermelo, and von Neumann they are.
> > > > >
> > > > > Reflecting the more common usage of today...
> > > > >
> > > > > "[A]mong all the objects studied in mathematics, some of the objects happen
> > > > > to be sets; and if x is an object and A is a set, then either x ∈ A is true
> > > > > or x ∈ A is false. (If A is not a set, we leave the statement x ∈ A
> > > > > undefined; for instance, we consider the statement 3 ∈ 4 to neither be true
> > > > > or false, but simply meaningless, since 4 is not a set.)" --Terence Tao,
> > > > > "Analysis I," p.34
> > > > Oh, *that* set theory.
> > > Terry seems to have done well by it. I have attempted to formalize it in my DC Proof system. It seems to work.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

After serious thinking Dan Christensen wrote :
> On Sunday, May 7, 2023 at 7:31:14 AM UTC-4, FromTheRafters wrote:
>> It happens that Dan Christensen formulated :
>>> On Saturday, May 6, 2023 at 8:28:10 PM UTC-4, FromTheRafters wrote:
>>>> Dan Christensen wrote :
>>>>> On Saturday, May 6, 2023 at 6:06:08 PM UTC-4, Dan Christensen wrote:
>>>>>> On Friday, May 5, 2023 at 7:56:58 AM UTC-4, Mostowski Collapse wrote:
>>>>>>> Maybe do SET SPACES before you do FUNCTION SPACES.
>>>>>>> So far, from judging how you deal with the Drinker Paradox,
>>>>>>> you didn't notice that your Set(_):
>>>>>>>
>>>>>>> The s such that Set(s)
>>>>>>>
>>>>>
>>>>> Some objects, say the number 4, are not usually considered to be sets.
>>>> Under Frege, Zermelo, and von Neumann they are.
>>>
>>> Reflecting the more common usage of today...
>>>
>>> "[A]mong all the objects studied in mathematics, some of the objects happen
>>> to be sets; and if x is an object and A is a set, then either x ∈ A is true
>>> or x ∈ A is false. (If A is not a set, we leave the statement x ∈ A
>>> undefined; for instance, we consider the statement 3 ∈ 4 to neither be true
>>> or false, but simply meaningless, since 4 is not a set.)" --Terence Tao,
>>> "Analysis I," p.34
>> Oh, *that* set theory.
>
> Terry seems to have done well by it. I have attempted to formalize it in my
> DC Proof system. It seems to work.

Yes, but none of them yet are perfect as foundational to mathematics.

See my reply just now to your identical posting at sci.logic

Dan

On Sunday, May 7, 2023 at 11:36:53 AM UTC-4, Mostowski Collapse wrote:
> You used it wrongly for the drinker paradox. Even Terrence Tao
> doesn't make the same blunder. You don't find him use Set(_).
> Even not implicitly when he talks about an arbitrary subset like here:
>
[snip]

On Sunday, May 7, 2023 at 11:43:36 AM UTC-4, Mostowski Collapse wrote:
> Could you define:
>
> ALL(a):ALL(b):[a ⊆ b <=> ALL(x):[x ∈ a => x ∈ b]]
>
Yes.

Define: Sub

ALL(a):ALL(b):[Set(a) & Set(b) => [Sub(a,b) <=> ALL(c):[c in a => c in b]]]
Axiom

> And then infer in DC Proof:
>
> Set(U) & D ⊆ U => Set(D) ?

Set(u) & Sub(d,u) => Set(d) ?

Not with the above definition. To "decode" Sub(d,u), you would already need to know that d was a set.

Dan

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

Thats probably a defect of DC proof or maybe a
defect of ZFCU. It only means that your sets possibly
have companions with the same extension

but nevertheless non-equivalent. Take s ⊆ u, you can
construct this set. From your subset axiom we
will have Set(r) because it was Set(u):

r = { x | x e u & x e s }

The set r has the same extension as s. But with your
extensionality axiom, you cannot prove them equivalent
since Set(s) is missing. Thats your extensionality:

6 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c @ a <=> c @ b]]]
Set Equality

Do you have this ZFCU axiom in DC Proof?

ALL(x):[~Set(x) => ~EXIST(y):y e x]

Dan Christensen schrieb am Sonntag, 7. Mai 2023 um 21:38:59 UTC+2:
> On Sunday, May 7, 2023 at 11:43:36 AM UTC-4, Mostowski Collapse wrote:
> > Could you define:
> >
> > ALL(a):ALL(b):[a ⊆ b <=> ALL(x):[x ∈ a => x ∈ b]]
> >
> Yes.
>
> Define: Sub
>
> ALL(a):ALL(b):[Set(a) & Set(b) => [Sub(a,b) <=> ALL(c):[c in a => c in b]]]
> Axiom
>
> > And then infer in DC Proof:
> >
> > Set(U) & D ⊆ U => Set(D) ?
> Set(u) & Sub(d,u) => Set(d) ?
>
> Not with the above definition. To "decode" Sub(d,u), you would already need to know that d was a set.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

So how would we express a predication:

P(f,x) <=> The function f is defined at the point x?

And please make it not Homo Ergaster style. Namely
some guideline how to bake a formula with 100 parameters,
that does express the above. There are only two

parameters: f the function and x the point.

Our ultimate goal here is:

"Beyond reverse engineering the brain in order to understand
and emulate it, the idea is of "uploading" a specific brain with
every mental process intact, to be instantiated on a "suitably
powerful computational substrate".

Basically there will be no ChatGPT interaction in the future.
Instead we will augment ourselves. And these augments might
have interconnects. Sympatric Transhumanism.

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

Maybe humans will loose some genes through a
Hybrid speciation. Although some Augment does not
necessarily mean genetic engineering, or does it?

Hybrid speciation is a form of speciation where
hybridization between two different species leads
to a new species, reproductively isolated from the parent species.
https://en.wikipedia.org/wiki/Hybrid_speciation

What will be the progress of life sciences, thanks
to better AI? Some more genetic engineering.
What is this guy talking about here:

'Godfather of AI' discusses dangers the¨
developing technologies pose to society
https://www.youtube.com/watch?v=yAgQWnD31nE

Mostowski Collapse schrieb am Samstag, 13. Mai 2023 um 17:29:02 UTC+2:
> So how would we express a predication:
>
> P(f,x) <=> The function f is defined at the point x?
>
> And please make it not Homo Ergaster style. Namely
> some guideline how to bake a formula with 100 parameters,
> that does express the above. There are only two
>
> parameters: f the function and x the point.
>
> Our ultimate goal here is:
>
> "Beyond reverse engineering the brain in order to understand
> and emulate it, the idea is of "uploading" a specific brain with
> every mental process intact, to be instantiated on a "suitably
> powerful computational substrate".
>
> Basically there will be no ChatGPT interaction in the future.
> Instead we will augment ourselves. And these augments might
> have interconnects. Sympatric Transhumanism.
> 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 Monday, May 8, 2023 at 8:58:52 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Sonntag, 7. Mai 2023 um 21:38:59 UTC+2:
> > On Sunday, May 7, 2023 at 11:43:36 AM UTC-4, Mostowski Collapse wrote:
> > > Could you define:
> > >
> > > ALL(a):ALL(b):[a ⊆ b <=> ALL(x):[x ∈ a => x ∈ b]]
> > >
> > Yes.
> >
> > Define: Sub
> >
> > ALL(a):ALL(b):[Set(a) & Set(b) => [Sub(a,b) <=> ALL(c):[c in a => c in b]]]
> > Axiom
> >
> > > And then infer in DC Proof:
> > >
> > > Set(U) & D ⊆ U => Set(D) ?
> > Set(u) & Sub(d,u) => Set(d) ?
> >
> > Not with the above definition. To "decode" Sub(d,u), you would already need to know that d was a set.

> Thats probably a defect of DC proof or maybe a
> defect of ZFCU. It only means that your sets possibly
> have companions with the same extension
>
> but nevertheless non-equivalent. Take s ⊆ u, you can
> construct this set. From your subset axiom we
> will have Set(r) because it was Set(u):
>
> r = { x | x e u & x e s }
>

In DC Proof that would be:

Set(r) & ALL(x):[x in r <=> x in u & x in s]

Assuming u and s were previously declared to be sets: Set(u) and Set(s)

1. Set(u)
Axiom

2. Set(s)
Axiom

3. EXIST(y):[Set(y) & ALL(x):[x in y <=> x in u & x in s]]
Subset, 1

4. Set(r) & ALL(x):[x in r <=> x in u & x in s]
E Spec, 3

r is subset of u. s is not necessarily a subset of u. If s and u are disjoint, then r will be empty.

> The set r has the same extension as s. But with your
> extensionality axiom, you cannot prove them equivalent

I hope not!

> since Set(s) is missing.

If s was not a set, what meaning would you attach to your "x in s"? Recall that, in math textbooks, unlike in ZFC, not everything assumed to be a set (see Tao).

> Thats your extensionality:
>
> 6 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c @ a <=> c @ b]]]
> Set Equality
>
> Do you have this ZFCU axiom in DC Proof?
>
> ALL(x):[~Set(x) => ~EXIST(y):y e x]

Or equivalently:

ALL(x):[EXIST(y):y in x => Set(x)]

No. It looks quite useless.

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, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> So how would we express a predication:
>
> P(f,x) <=> The function f is defined at the point x?
>

ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]

=> [P(fun,elt) <=> elt in dom]]

Dan

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

Well a binary predicate definition would only read:

ALL(f):ALL(x):[P(f,x) <=> ...]

Try again!

Dan Christensen schrieb am Samstag, 13. Mai 2023 um 20:33:05 UTC+2:
> On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > So how would we express a predication:
> >
> > P(f,x) <=> The function f is defined at the point x?
> >
> ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
>
> => [P(fun,elt) <=> elt in dom]]
> 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, May 13, 2023 at 6:02:52 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Samstag, 13. Mai 2023 um 20:33:05 UTC+2:
> > On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > > So how would we express a predication:
> > >
> > > P(f,x) <=> The function f is defined at the point x?
> > >
> > ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
> >
> > => [P(fun,elt) <=> elt in dom]]

> Well a binary predicate definition would only read:
>
> ALL(f):ALL(x):[P(f,x) <=> ...]
>

What is f? What is x?

You need something a little more specific, Mr. Collapse. Try again.

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, May 13, 2023 at 6:02:52 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Samstag, 13. Mai 2023 um 20:33:05 UTC+2:
> > On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > > So how would we express a predication:
> > >
> > > P(f,x) <=> The function f is defined at the point x?
> > >
> > ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
> >
> > => [P(fun,elt) <=> elt in dom]]

> Well a binary predicate definition would only read:
>
> ALL(f):ALL(x):[P(f,x) <=> ...]
>

What is f? What is x?

You need something a little more specific, Mr. Collapse.

Let me guess... You want to be able to infer that P(f,x) is false is f is not a function or x has not been declared to be a set. That's not usually how things work in mathematics. In that case, P(f,x) would be indeterminate.

Try again, 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

I see a big problem with your definition, it is wrong:

ALL(a):[a in dom => fun(a) in cod] => [P(fun,elt) <=> elt in dom]

Where P should express that fun is defined at elt, right?

Now take the following dom and cod:

dom={0}, cod={0}

And take the following function:

fun(0)=0
fun(1)=1

Is it defined at 1?

Dan Christensen schrieb am Sonntag, 14. Mai 2023 um 00:56:31 UTC+2:
> On Saturday, May 13, 2023 at 6:02:52 PM UTC-4, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Samstag, 13. Mai 2023 um 20:33:05 UTC+2:
> > > On Saturday, May 13, 2023 at 11:29:02 AM UTC-4, Mostowski Collapse wrote:
> > > > So how would we express a predication:
> > > >
> > > > P(f,x) <=> The function f is defined at the point x?
> > > >
> > > ALL(fun):ALL(dom):ALL(cod):ALL(elt):[Set(dom) & Set(cod) & ALL(a):[a in dom => fun(a) in cod]
> > >
> > > => [P(fun,elt) <=> elt in dom]]
> > Well a binary predicate definition would only read:
> >
> > ALL(f):ALL(x):[P(f,x) <=> ...]
> >
> What is f? What is x?
>
> You need something a little more specific, Mr. Collapse.
>
> Let me guess... You want to be able to infer that P(f,x) is false is f is not a function or x has not been declared to be a set. That's not usually how things work in mathematics. In that case, P(f,x) would be indeterminate..
>
> Try again, 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