Maybe call it "little-set theory". It is well known that most mathematics
needs only a little set theory. I guess little set theory would work
with sets from V_ω+ω. Can you prove the existence of V_ω+ω in

DC Proof, with the existing axioms of DC Proof? You even don't have
an axiom of infinity. So you cannot prove existence of ω. But lets
assume ω exists, could you show that V_ω+ω exists in DC Proof ?

V_ω+ω is called the universe for ordinary mathematics. See also
here, which a reference to a book by Smullyan & Fitting:

"V_ω+ω is the universe of "ordinary mathematics",
and is a model of Zermelo set theory.
https://en.wikipedia.org/wiki/Von_Neumann_universe

Mild Shock schrieb am Freitag, 14. Juli 2023 um 22:49:49 UTC+2:
> Well why do you name it set theory than, if its not set theory.
> I mean you can read the 1908 paper of Zermelo. He uses singletons
> to model natural numbers:
>
> 1 = {{}}
> 2 = {{{}}}
> 3 = {{{{}}}}
> Etc...
>
> The so called Zermelo successor is succ(x) = {x}. Something
> you don't have in DC Proof. So why call it "set theory" when its not set theory?
> Dan Christensen schrieb am Freitag, 14. Juli 2023 um 17:22:46 UTC+2:
> > On Friday, July 14, 2023 at 4:22:23 AM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> > > The problem is, everytime Dan-O-Matik refers to "set theory",
> > > on sci.logic or sci.math, as a recommendation or as explication
> > > what he is doing, he is not refering to "set theory" proper.
> > >
> > [snip]
> >
> > I am referring to axioms implicitly used in most textbook proofs--not ZFC as it turns out. Deal with it, 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

On Friday, July 14, 2023 at 4:49:49 PM UTC-4, Mild Shock wrote:

> Dan Christensen schrieb am Freitag, 14. Juli 2023 um 17:22:46 UTC+2:
> > On Friday, July 14, 2023 at 4:22:23 AM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> > > The problem is, everytime Dan-O-Matik refers to "set theory",
> > > on sci.logic or sci.math, as a recommendation or as explication
> > > what he is doing, he is not refering to "set theory" proper.
> > >
> > [snip]
> >
> > I am referring to axioms implicitly used in most textbook proofs--not ZFC as it turns out. Deal with it, Mr. Collapse.

> Well why do you name it set theory

Again, it is the "set theory" is actually used in most textbook proofs.

than, if its not set theory.
> I mean you can read the 1908 paper of Zermelo. He uses singletons
> to model natural numbers:
>
> 1 = {{}}
> 2 = {{{}}}
> 3 = {{{{}}}}
> Etc...
>

3 is not usually considered to be a set in most textbook proofs. Must be frustrating as hell for you.

> The so called Zermelo successor is succ(x) = {x}.

I prefer Peano's Axioms as follows:

1. Set(n)
Axiom

2. 0 in n
Axiom

3. ALL(a):[a in n => s(a) in n]
Axiom

4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
Axiom

5. ALL(a):[a in n => ~s(a)=0]
Axiom

6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in a => s(b) in a] => ALL(b):[b in n => b in a]]]
Axiom

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, July 14, 2023 at 5:00:42 PM UTC-4, Mild Shock wrote:
> Maybe call it "little-set theory". It is well known that most mathematics
> needs only a little set theory.

I have formalized the set theory used in most mathematics in DC Proof

> I guess little set theory would work
> with sets from V_ω+ω. Can you prove the existence of V_ω+ω in
>
[snip]
V cannot even be proven to exist in ZFC, so why bother?

> You even don't have
> an axiom of infinity.

No set or other object is postulated to exist in DC Proof, but users can introduce their own versions of an axiom of infinity. I prefer simply stating Peano's Axioms at the beginning of a proof (see my previous posting here).

> So you cannot prove existence of ω.

[snip]

If you are determined to prove the existence of the set of natural numbers, you can start by assuming the existence of an arbitrary Dedekind infinite set (an alternative axiom of infinity) :

1. EXIST(a):EXIST(f):[Set(a) & ALL(b):[b in a => f(b) in a] <------------- f: a --> a
& ALL(b):ALL(c):[b in a & c in a => [f(b)=f(c) => b=c]] <-------------------- f is injective
& EXIST(b):[b in a & ALL(c):[c in a => ~f(c)=b]]] <---------------------------- f is not surjective

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, July 14, 2023 at 5:00:42 PM UTC-4, Mild Shock wrote:
> Maybe call it "little-set theory". It is well known that most mathematics
> needs only a little set theory.

In DC Proof, I have formalized the set theory used in most mathematics.

> I guess little set theory would work
> with sets from V_ω+ω. Can you prove the existence of V_ω+ω in
>
[snip]

V cannot even be proven to exist in ZFC, so why bother?

> You even don't have
> an axiom of infinity.

No set or other object is postulated to exist in DC Proof, but users can introduce their own versions of an axiom of infinity. I prefer simply stating Peano's Axioms at the beginning of a proof (see my previous posting here).

> So you cannot prove existence of ω.

[snip]

If you are determined to prove the existence of the set of natural numbers, you can start by assuming the existence of an arbitrary Dedekind infinite set (an alternative axiom of infinity) :

1. EXIST(a):EXIST(f):[Set(a) & ALL(b):[b in a => f(b) in a] <------------- f: a --> a
& ALL(b):ALL(c):[b in a & c in a => [f(b)=f(c) => b=c]] <-------------------- f is injective
& EXIST(b):[b in a & ALL(c):[c in a => ~f(c)=b]]] <---------------------------- f is not surjective

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, July 14, 2023 at 4:05:55 AM UTC-4, Mild Shock wrote:
[snip]

> The truth is that there is only one satisfactory way of avoiding
> the paradoxes: namely, the use of some form of the theory of types.
> That was at the basis of both Russell's and Zermelo's intuitions.

[snip]

DC Proof avoids Russell's Paradox and the existence of a universal set by not assuming (as in Frege's axioms) that for every unary predicate P, we can infer the existence of a set {x : P(x)}. Using the my Subset Axiom, however, for any set S and predicate P, we can infer the existence of a set {x in S: P(x)} -- no type theory required.

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, July 14, 2023 at 4:05:55 AM UTC-4, Mild Shock wrote:
[snip]

> The truth is that there is only one satisfactory way of avoiding
> the paradoxes: namely, the use of some form of the theory of types.
> That was at the basis of both Russell's and Zermelo's intuitions.

[snip]

DC Proof avoids Russell's Paradox and the existence of a universal set by not assuming (as in Frege's axioms) that for every unary predicate P, we can infer the existence of a set {x : P(x)}.

Using my Subset Axiom, however, for any set S and unary predicate P, we can infer the existence of a set {x in S: P(x)}, no type theory required.

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, July 14, 2023 at 11:45:21 PM UTC-4, Dan Christensen wrote:
> On Friday, July 14, 2023 at 4:05:55 AM UTC-4, Mild Shock wrote:
> [snip]
> > The truth is that there is only one satisfactory way of avoiding
> > the paradoxes: namely, the use of some form of the theory of types.
> > That was at the basis of both Russell's and Zermelo's intuitions.
> [snip]
>
> DC Proof avoids Russell's Paradox and the existence of a universal set by not assuming (as in Frege's axioms) that for every unary predicate P, we can infer the existence of a set {x : P(x)}.
>
> Using my Subset Axiom, however, for any set S and unary predicate P, we can infer the existence of a set {x in S: P(x)}, no type theory required.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
here is a sample of real sets that are bit encoded in my system
pspace to qspace transform uses bit encoded sets
here is the code (equations) for transforming a set of boolean models to a set of valid quantifications
it depends on add in set theory which depends on bignum counting
vee is a number less than n the number of variables
the set is bit encoded by 32 bit nums and needs space to hold set members
boolean variables encode each member

the transform is from pspace in dnf to qspace in monotone dnf
the result is the solution of all qbfs in twelve lines
the original set of members transforms to quantifications

there is a followup transform from monotone dnf to monotone cnf
daniel2380+++

// plan left right of all set members with set union/intersection
void plan (num vee, numnums& set)
{ when(set.size()==zero || vee == qvars.size()) return;
numnums left; numnums right; split(vee, set, left, right);
plan(vee + one, left); plan(vee + one, right); juggle (vee, left, right);
// ezistential q variables are in left universal remain on right
for (num g = zero; g < left.size(); g++) ezis(*(left[g]), vee);}

// left right union and intersection
void juggle (num vee, numnums& left, numnums& right)
{if(left.size()==zero){for(num g=zero;g<right.size();g++)left.add(right[g]);right.setsize(zero);return;}
when(vee == qvars.size()) return;
numnums al; numnums ar; split(vee + one, left, al, ar); left.setsize(zero);
numnums bl; numnums br; split(vee + one, right, bl, br); right.setsize(zero);
juggle(vee + one, al, bl); juggle(vee + one, ar, br);
for (num g=zero; g < al.size(); g++) left.add(al[g]); for (num g=zero; g < ar.size(); g++) left.add(ar[g]);
for (num g=zero; g < bl.size(); g++) right.add(bl[g]); for (num g=zero; g < br.size(); g++) right.add(br[g]); }

static num be(nums& s, num b) { return (s[b >> five] & (ones[b & fifthtau])); } //
static joy ezis(nums& s, num b) { s[b >> five] &= zeroes[b & fifthtau]; } //
static joy split /*leftright around bit*/(num b, numnums& s, numnums& l, numnums& r) // left right on bit b
{for (num g = zero; g < s.size(); g++) if (be((*s[g]), b)) r.add(s[g]); else l.add(s[g]); } //

On Friday, July 14, 2023 at 11:45:21 PM UTC-4, Dan Christensen wrote:
> On Friday, July 14, 2023 at 4:05:55 AM UTC-4, Mild Shock wrote:
> [snip]
> > The truth is that there is only one satisfactory way of avoiding
> > the paradoxes: namely, the use of some form of the theory of types.
> > That was at the basis of both Russell's and Zermelo's intuitions.
> [snip]
>
> DC Proof avoids Russell's Paradox and the existence of a universal set by not assuming (as in Frege's axioms) that for every unary predicate P, we can infer the existence of a set {x : P(x)}.
>
> Using my Subset Axiom, however, for any set S and unary predicate P, we can infer the existence of a set {x in S: P(x)}, no type theory required.

This feature would seem to avoid the internal contradictions of Frege's axioms as exhibited by Russell's Paradox and the notion of a universal set.

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

Maybe start with something simpler.
Can this here proved in DC Proof to exist:

ω+ω

It looks as follows:

0, 1, 2, 3, ... 0', 1', 2', 3', ...

See also:
https://en.wikipedia.org/wiki/Ordinal_arithmetic#Addition

Mild Shock schrieb am Freitag, 14. Juli 2023 um 23:00:42 UTC+2:
> Maybe call it "little-set theory". It is well known that most mathematics
> needs only a little set theory. I guess little set theory would work
> with sets from V_ω+ω. Can you prove the existence of V_ω+ω in
>
> DC Proof, with the existing axioms of DC Proof? You even don't have
> an axiom of infinity. So you cannot prove existence of ω. But lets
> assume ω exists, could you show that V_ω+ω exists in DC Proof ?
>
> V_ω+ω is called the universe for ordinary mathematics. See also
> here, which a reference to a book by Smullyan & Fitting:
>
> "V_ω+ω is the universe of "ordinary mathematics",
> and is a model of Zermelo set theory.
> https://en.wikipedia.org/wiki/Von_Neumann_universe
> Mild Shock schrieb am Freitag, 14. Juli 2023 um 22:49:49 UTC+2:
> > Well why do you name it set theory than, if its not set theory.
> > I mean you can read the 1908 paper of Zermelo. He uses singletons
> > to model natural numbers:
> >
> > 1 = {{}}
> > 2 = {{{}}}
> > 3 = {{{{}}}}
> > Etc...
> >
> > The so called Zermelo successor is succ(x) = {x}. Something
> > you don't have in DC Proof. So why call it "set theory" when its not set theory?
> > Dan Christensen schrieb am Freitag, 14. Juli 2023 um 17:22:46 UTC+2:
> > > On Friday, July 14, 2023 at 4:22:23 AM UTC-4, Mild Shock (aka Mr. Collapse) wrote:
> > > > The problem is, everytime Dan-O-Matik refers to "set theory",
> > > > on sci.logic or sci.math, as a recommendation or as explication
> > > > what he is doing, he is not refering to "set theory" proper.
> > > >
> > > [snip]
> > >
> > > I am referring to axioms implicitly used in most textbook proofs--not ZFC as it turns out. Deal with it, 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

On Saturday, July 15, 2023 at 2:50:33 PM UTC-4, Mild Shock wrote:
> Maybe start with something simpler.
> Can this here proved in DC Proof to exist:
>
> ω+ω
>
> It looks as follows:
>
> 0, 1, 2, 3, ... 0', 1', 2', 3', ...
>

You might use the following axiom to specify N={0, 1, 2, ... } and N'={0', 1', 2', ... } and take the union N U N'.

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

> See also:
> https://en.wikipedia.org/wiki/Ordinal_arithmetic#Addition

I'm not sure, but you might be able to formalize the axioms there in DC Proof. It is not something that interests me. Thanks anyway.

Dan

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

(Correction)

On Saturday, July 15, 2023 at 2:50:33 PM UTC-4, Mild Shock wrote:
> Maybe start with something simpler.
> Can this here proved in DC Proof to exist:
>
> ω+ω
>
> It looks as follows:
>
> 0, 1, 2, 3, ... 0', 1', 2', 3', ...
>

You might use the following axiom to specify N={0, 1, 2, ... } and N'={0', 1', 2', ... } and take the union N U N'.

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

> See also:
> https://en.wikipedia.org/wiki/Ordinal_arithmetic#Addition

I'm not sure, but you might be able to formalize the axioms there in DC Proof. It is not something that interests me. Thanks anyway.

Dan

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

How do you produce N' in DC Proof?

Dan Christensen schrieb am Sonntag, 16. Juli 2023 um 21:36:51 UTC+2:
> (Correction)
> On Saturday, July 15, 2023 at 2:50:33 PM UTC-4, Mild Shock wrote:
> > Maybe start with something simpler.
> > Can this here proved in DC Proof to exist:
> >
> > ω+ω
> >
> > It looks as follows:
> >
> > 0, 1, 2, 3, ... 0', 1', 2', 3', ...
> >
> You might use the following axiom to specify N={0, 1, 2, ... } and N'={0', 1', 2', ... } and take the union N U N'.
>
> 1. EXIST(m):EXIST(m0):EXIST(f): [Set(m) & m0 in m & ALL(a):[a in m => f(a) in m]
> & ALL(a):ALL(b):[a in m & b in m => [f(a)=f(b) => a=b]]
> & ALL(a):[a in m => ~f(a)=m0]
> & ALL(a):[Set(a) & ALL(b):[b in a => b in m] => [m0 in a & ALL(b):[b in a => f(b) in a] => ALL(b):[b in m => b in a]]]]
> Axiom
>
> > See also:
> > https://en.wikipedia.org/wiki/Ordinal_arithmetic#Addition
>
> I'm not sure, but you might be able to formalize the axioms there in DC Proof. It is not something that interests me. Thanks anyway.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Ref: https://github.com/wo/tpg/issues/23

Wolfgang Schwarz fixed his tool. This one can
now be automatically proved.

∀a∀b∃c∀d(Edc ↔ (d=a ∨ d=b)) → ∀b∃c∀d(Edc ↔ d=b) is valid.
https://www.umsu.de/trees/#~6a~6b~7c~6d%28Edc~4%28d=a~2d=b%29%29~5~6b~7c~6d%28Edc~4d=b%29

Nice!

Mild Shock schrieb am Donnerstag, 13. Juli 2023 um 23:36:19 UTC+2:
> You don't have the Pairing Axiom in DC Proof.
> Who cares? Dana Scott didn't work with DC Proof.
>
> As soon as you have the Lemma, its like riding
> the back of a tornado. You can prove it in a blink!
> ∀xAx → ∀y∀x(Exy → Ax) is valid.
> https://www.umsu.de/trees/#~6xAx~5~6y~6x%28Exy~5Ax%29
> (∀b∃c∀d(Edc ↔ d=b) ∧ ∀y∀x(Exy → Ax)) → ∀xAx is valid.
> https://www.umsu.de/trees/#~6b~7c~6d%28Edc~4d=b%29~1~6y~6x%28Exy~5Ax%29~5~6xAx
> Mild Shock schrieb am Donnerstag, 13. Juli 2023 um 23:31:26 UTC+2:
> > Are you sleep walking? Read the thread carefully.
> > How many times do you find the phrase in this thread?
> >
> > "unordered pair"
> >
> > How many times do you find a link to this axiom:
> >
> > https://en.wikipedia.org/wiki/Axiom_of_pairing
> >
> > You even find a DC Proof of this Lemma:
> > 44 ALL(a):ALL(b):EXIST(c):ALL(d):[d ε c <=> d=a | d=b]
> > => ALL(b):EXIST(c):ALL(d):[d ε c <=> d=b]
> > Conclusion, 1
> > Dan Christensen schrieb am Donnerstag, 13. Juli 2023 um 23:26:10 UTC+2:
> > > On Thursday, July 13, 2023 at 4:52:49 PM UTC-4, Mild Shock wrote:
> > > > So lets go back to the sketch, and finalize the proof:
> > > > > Its not so difficult to prove. The => direction
> > > > > is trivial. And the <= direction you can consider the
> > > > > sub case y={x} that (*), which needs unordered pair:
> > > > Lets see wether the => direction is trivial. Yes it needs nothing:
> > > >
> > > > ∀xAx → ∀y∀x(Exy → Ax) is valid.
> > > > https://www.umsu.de/trees/#~6xAx~5~6y~6x%28Exy~5Ax%29
> > > >
> > > > And now the <= direction using the Singleton lemma:
> > > >
> > > > (∀b∃c∀d(Edc ↔ d=b) ∧ ∀y∀x(Exy → Ax)) → ∀xAx is valid.
> > > > https://www.umsu.de/trees/#~6b~7c~6d%28Edc~4d=b%29~1~6y~6x%28Exy~5Ax%29~5~6xAx
> > > >
> > > Doesn't your Singleton lemma require ZFC (e.g. a Pairing Axiom)? You will probably want to specify a set to be the "domain of discourse" and include it in your theorem.
> > > 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, July 17, 2023 at 3:17:29 AM UTC-4, Mild Shock wrote:

> Dan Christensen schrieb am Sonntag, 16. Juli 2023 um 21:36:51 UTC+2:
> > (Correction)
> > On Saturday, July 15, 2023 at 2:50:33 PM UTC-4, Mild Shock wrote:
> > > Maybe start with something simpler.
> > > Can this here proved in DC Proof to exist:
> > >
> > > ω+ω
> > >
> > > It looks as follows:
> > >
> > > 0, 1, 2, 3, ... 0', 1', 2', 3', ...
> > >
> > You might use the following axiom to specify N={0, 1, 2, ... } and N'={0', 1', 2', ... } and take the union N U N'.
> >
> > 1. EXIST(m):EXIST(m0):EXIST(f): [Set(m) & m0 in m & ALL(a):[a in m => f(a) in m]
> > & ALL(a):ALL(b):[a in m & b in m => [f(a)=f(b) => a=b]]
> > & ALL(a):[a in m => ~f(a)=m0]
> > & ALL(a):[Set(a) & ALL(b):[b in a => b in m] => [m0 in a & ALL(b):[b in a => f(b) in a] => ALL(b):[b in m => b in a]]]]
> > Axiom
> >
[snip]

> How do you produce N' in DC Proof?

You would apply the above axiom twice, specifying different names the second time: n, 0, s then n', 0', s'

Dan

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

Your such a Ordinal Baby Dan-O-Matik
And how would you prove the existence of:

ω
ω+ω
ω+ω+ω
ω+ω+ω+ω
Etc..

Namely the existence of ω*n?
Hint: ω+ω is the special case ω*2.

Dan Christensen schrieb:
> On Monday, July 17, 2023 at 3:17:29 AM UTC-4, Mild Shock wrote:
>
>> Dan Christensen schrieb am Sonntag, 16. Juli 2023 um 21:36:51 UTC+2:
>>> (Correction)
>>> On Saturday, July 15, 2023 at 2:50:33 PM UTC-4, Mild Shock wrote:
>>>> Maybe start with something simpler.
>>>> Can this here proved in DC Proof to exist:
>>>>
>>>> ω+ω
>>>>
>>>> It looks as follows:
>>>>
>>>> 0, 1, 2, 3, ... 0', 1', 2', 3', ...
>>>>
>>> You might use the following axiom to specify N={0, 1, 2, ... } and N'={0', 1', 2', ... } and take the union N U N'.
>>>
>>> 1. EXIST(m):EXIST(m0):EXIST(f): [Set(m) & m0 in m & ALL(a):[a in m => f(a) in m]
>>> & ALL(a):ALL(b):[a in m & b in m => [f(a)=f(b) => a=b]]
>>> & ALL(a):[a in m => ~f(a)=m0]
>>> & ALL(a):[Set(a) & ALL(b):[b in a => b in m] => [m0 in a & ALL(b):[b in a => f(b) in a] => ALL(b):[b in m => b in a]]]]
>>> Axiom
>>>
> [snip]
>
>> How do you produce N' in DC Proof?
>
> You would apply the above axiom twice, specifying different names the second time: n, 0, s then n', 0', s'
>
> 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, July 17, 2023 at 2:11:11 PM UTC-4, Mild Shock (aka Mr. Collapse) wrote:

> [snip childish abuse]

> And how would you prove the existence of:
>
> ω
> ω+ω
> ω+ω+ω
> ω+ω+ω+ω
> Etc..
>

Again, this is simply not something that interests me. See my blog for the kinds of things that do interest me.

Dan

Dana Scott fan club challenge. Show that "obj" as a set
and naively modelled here by Dan Christensen:

Toward a Formal, Machine-Parsable Definition of a Category
https://groups.google.com/g/sci.math/c/gDtJtH8RHvc

Cannot be a set if we assume certain category theory equations,
which might be seen as consistent in category theory itself.

Disclaimer: I don't have such equations just now at hand, working on it.

Dan Christensen schrieb am Montag, 17. Juli 2023 um 20:58:43 UTC+2:
> > ω
> > ω+ω
> > ω+ω+ω
> > ω+ω+ω+ω
> > Etc..
> >
> Again, this is simply not something that interests me.

On Thursday, August 3, 2023 at 2:45:29 AM UTC-7, Mild Shock wrote:
> Dana Scott fan club challenge. Show that "obj" as a set
> and naively modelled here by Dan Christensen:
>
> Toward a Formal, Machine-Parsable Definition of a Category
> https://groups.google.com/g/sci.math/c/gDtJtH8RHvc
>
> Cannot be a set if we assume certain category theory equations,
> which might be seen as consistent in category theory itself.
>
> Disclaimer: I don't have such equations just now at hand, working on it.
> Dan Christensen schrieb am Montag, 17. Juli 2023 um 20:58:43 UTC+2:
> > > ω
> > > ω+ω
> > > ω+ω+ω
> > > ω+ω+ω+ω
> > > Etc..
> > >
> > Again, this is simply not something that interests me.

Picked up a copy of a translation one of Kant's less-than-usually-ambitiously-titled
"On the old saw: That may be right in theory but it won't work in practice",
and it helps remind me that lots of modern neo-Platonists are pseudo-Platonists
and that a strong Platonism again is sort of superior for stronger logicists.

It's like when Russell quipped "mathematics is I dunno" ("mathematics is that where
we never know what we're doing nor whether it's true") and it's like, no, Russell,
it's pretty much the opposite.

On Thursday, August 3, 2023 at 10:43:59 PM UTC-7, Ross Finlayson wrote:
> On Thursday, August 3, 2023 at 2:45:29 AM UTC-7, Mild Shock wrote:
> > Dana Scott fan club challenge. Show that "obj" as a set
> > and naively modelled here by Dan Christensen:
> >
> > Toward a Formal, Machine-Parsable Definition of a Category
> > https://groups.google.com/g/sci.math/c/gDtJtH8RHvc
> >
> > Cannot be a set if we assume certain category theory equations,
> > which might be seen as consistent in category theory itself.
> >
> > Disclaimer: I don't have such equations just now at hand, working on it..
> > Dan Christensen schrieb am Montag, 17. Juli 2023 um 20:58:43 UTC+2:
> > > > ω
> > > > ω+ω
> > > > ω+ω+ω
> > > > ω+ω+ω+ω
> > > > Etc..
> > > >
> > > Again, this is simply not something that interests me.
> Picked up a copy of a translation one of Kant's less-than-usually-ambitiously-titled
> "On the old saw: That may be right in theory but it won't work in practice",
> and it helps remind me that lots of modern neo-Platonists are pseudo-Platonists
> and that a strong Platonism again is sort of superior for stronger logicists.
>
> It's like when Russell quipped "mathematics is I dunno" ("mathematics is that where
> we never know what we're doing nor whether it's true") and it's like, no, Russell,
> it's pretty much the opposite.

Your rejection of strong platonism won't work in the practice of strong platonism.

It's pretty simple: you don't have to accept being Russell's dupe.
The Russellian duplicity of the Russellian hypocrisy of the Russell "paradox"
being axiomatized away, it's just a mental convenience for agreeably a large
class of concerns, that if you don't know the difference, and maintain through
all derivations why it's not so, Russell's "I usurped Frege", then, that would
result an ignoramus, who agreeably doesn't need to know the difference,
or a hypocrite, or a charlatan.

For foundation's sake though, it's unacceptable.

It is in SETS FOR MATHEMATICS, how things are not sets.
Even with only reading half of the book.

"Subsets are not mere sets with a special property but are
explicit inclusion maps. (This helps one to realize that
many constructions involving subsets are simplified and
usefully generalized when applied appropriately to maps that
are not necessarily subsets.)"
http://patryshev.com/books/Sets%20for%20Mathematics.pdf

You just reject this definition:

A ⊆ B <=> ∀x(x ∈ A => x ∈ B)

And go with this definition, note in WILLIAM LAWVERE, the
arrows are basically sets:

"Historically many mathematicians such as Dedekind
and Banach used the same symbol ⊆ for both membership
and inclusion, and indeed it is quite reasonable to
define x belongs to y for any two maps with codomain A
and even to use the same symbol for it"
http://patryshev.com/books/Sets%20for%20Mathematics.pdf

x ⊆ y <=> ∃z(x = y*z)

Ross Finlayson schrieb am Freitag, 4. August 2023 um 08:12:45 UTC+2:
> On Thursday, August 3, 2023 at 10:43:59 PM UTC-7, Ross Finlayson wrote:
> > On Thursday, August 3, 2023 at 2:45:29 AM UTC-7, Mild Shock wrote:
> > > Dana Scott fan club challenge. Show that "obj" as a set
> > > and naively modelled here by Dan Christensen:
> > >
> > > Toward a Formal, Machine-Parsable Definition of a Category
> > > https://groups.google.com/g/sci.math/c/gDtJtH8RHvc
> > >
> > > Cannot be a set if we assume certain category theory equations,
> > > which might be seen as consistent in category theory itself.
> > >
> > > Disclaimer: I don't have such equations just now at hand, working on it.
> > > Dan Christensen schrieb am Montag, 17. Juli 2023 um 20:58:43 UTC+2:
> > > > > ω
> > > > > ω+ω
> > > > > ω+ω+ω
> > > > > ω+ω+ω+ω
> > > > > Etc..
> > > > >
> > > > Again, this is simply not something that interests me.
> > Picked up a copy of a translation one of Kant's less-than-usually-ambitiously-titled
> > "On the old saw: That may be right in theory but it won't work in practice",
> > and it helps remind me that lots of modern neo-Platonists are pseudo-Platonists
> > and that a strong Platonism again is sort of superior for stronger logicists.
> >
> > It's like when Russell quipped "mathematics is I dunno" ("mathematics is that where
> > we never know what we're doing nor whether it's true") and it's like, no, Russell,
> > it's pretty much the opposite.
> Your rejection of strong platonism won't work in the practice of strong platonism.
>
> It's pretty simple: you don't have to accept being Russell's dupe.
> The Russellian duplicity of the Russellian hypocrisy of the Russell "paradox"
> being axiomatized away, it's just a mental convenience for agreeably a large
> class of concerns, that if you don't know the difference, and maintain through
> all derivations why it's not so, Russell's "I usurped Frege", then, that would
> result an ignoramus, who agreeably doesn't need to know the difference,
> or a hypocrite, or a charlatan.
>
>
> For foundation's sake though, it's unacceptable.

Now I am having fun with minimal logic, which rejects not
only ex falso quodlibet, but equivalently it rejects counter
example theorem:

~(P -> Q) => P /\ ~Q

Usually this can be used in set theory, to say if A ⊆ B
doesn't hold, then there must be a point c such that
c ∈ A and ~c ∈ B. By the usual logical transformation,

whereby the elimination of ∀x and the introduction of
∃x is not problematic, since ∃x would be anyway typically
defined as ~∀x~:

~∀x(x ∈ A => x ∈ B)
---------------------------------
∃x(x ∈ A /\ ~x ∈ B)

I guess in category you cannot say te same. ~(x ⊆ y) does
not automatically imply that there is such a point. The book
is full of examples from analysis and geometry,

but I think the book is not very accessible. Maybe starting
with minimal logic would be more productive. Disclaimer:
There might be also differences between minimal logic, and

category theory. Just discovering a few things right now,
such like the above involvedment of counter example theorem.

Mild Shock schrieb am Freitag, 4. August 2023 um 12:03:16 UTC+2:
> It is in SETS FOR MATHEMATICS, how things are not sets.
> Even with only reading half of the book.
>
> "Subsets are not mere sets with a special property but are
> explicit inclusion maps. (This helps one to realize that
> many constructions involving subsets are simplified and
> usefully generalized when applied appropriately to maps that
> are not necessarily subsets.)"
> http://patryshev.com/books/Sets%20for%20Mathematics.pdf
>
> You just reject this definition:
>
> A ⊆ B <=> ∀x(x ∈ A => x ∈ B)
>
> And go with this definition, note in WILLIAM LAWVERE, the
> arrows are basically sets:
>
> "Historically many mathematicians such as Dedekind
> and Banach used the same symbol ⊆ for both membership
> and inclusion, and indeed it is quite reasonable to
> define x belongs to y for any two maps with codomain A
> and even to use the same symbol for it"
> http://patryshev.com/books/Sets%20for%20Mathematics.pdf
>
> x ⊆ y <=> ∃z(x = y*z)
> Ross Finlayson schrieb am Freitag, 4. August 2023 um 08:12:45 UTC+2:
> > On Thursday, August 3, 2023 at 10:43:59 PM UTC-7, Ross Finlayson wrote:
> > > On Thursday, August 3, 2023 at 2:45:29 AM UTC-7, Mild Shock wrote:
> > > > Dana Scott fan club challenge. Show that "obj" as a set
> > > > and naively modelled here by Dan Christensen:
> > > >
> > > > Toward a Formal, Machine-Parsable Definition of a Category
> > > > https://groups.google.com/g/sci.math/c/gDtJtH8RHvc
> > > >
> > > > Cannot be a set if we assume certain category theory equations,
> > > > which might be seen as consistent in category theory itself.
> > > >
> > > > Disclaimer: I don't have such equations just now at hand, working on it.
> > > > Dan Christensen schrieb am Montag, 17. Juli 2023 um 20:58:43 UTC+2:
> > > > > > ω
> > > > > > ω+ω
> > > > > > ω+ω+ω
> > > > > > ω+ω+ω+ω
> > > > > > Etc..
> > > > > >
> > > > > Again, this is simply not something that interests me.
> > > Picked up a copy of a translation one of Kant's less-than-usually-ambitiously-titled
> > > "On the old saw: That may be right in theory but it won't work in practice",
> > > and it helps remind me that lots of modern neo-Platonists are pseudo-Platonists
> > > and that a strong Platonism again is sort of superior for stronger logicists.
> > >
> > > It's like when Russell quipped "mathematics is I dunno" ("mathematics is that where
> > > we never know what we're doing nor whether it's true") and it's like, no, Russell,
> > > it's pretty much the opposite.
> > Your rejection of strong platonism won't work in the practice of strong platonism.
> >
> > It's pretty simple: you don't have to accept being Russell's dupe.
> > The Russellian duplicity of the Russellian hypocrisy of the Russell "paradox"
> > being axiomatized away, it's just a mental convenience for agreeably a large
> > class of concerns, that if you don't know the difference, and maintain through
> > all derivations why it's not so, Russell's "I usurped Frege", then, that would
> > result an ignoramus, who agreeably doesn't need to know the difference,
> > or a hypocrite, or a charlatan.
> >
> >
> > For foundation's sake though, it's unacceptable.

On Friday, August 4, 2023 at 3:17:57 AM UTC-7, Mild Shock wrote:
> Now I am having fun with minimal logic, which rejects not
> only ex falso quodlibet, but equivalently it rejects counter
> example theorem:
>
> ~(P -> Q) => P /\ ~Q
>
> Usually this can be used in set theory, to say if A ⊆ B
> doesn't hold, then there must be a point c such that
> c ∈ A and ~c ∈ B. By the usual logical transformation,
>
> whereby the elimination of ∀x and the introduction of
> ∃x is not problematic, since ∃x would be anyway typically
> defined as ~∀x~:
>
> ~∀x(x ∈ A => x ∈ B)
> ---------------------------------
> ∃x(x ∈ A /\ ~x ∈ B)
>
> I guess in category you cannot say te same. ~(x ⊆ y) does
> not automatically imply that there is such a point. The book
> is full of examples from analysis and geometry,
>
> but I think the book is not very accessible. Maybe starting
> with minimal logic would be more productive. Disclaimer:
> There might be also differences between minimal logic, and
>
> category theory. Just discovering a few things right now,
> such like the above involvedment of counter example theorem.
> Mild Shock schrieb am Freitag, 4. August 2023 um 12:03:16 UTC+2:
> > It is in SETS FOR MATHEMATICS, how things are not sets.
> > Even with only reading half of the book.
> >
> > "Subsets are not mere sets with a special property but are
> > explicit inclusion maps. (This helps one to realize that
> > many constructions involving subsets are simplified and
> > usefully generalized when applied appropriately to maps that
> > are not necessarily subsets.)"
> > http://patryshev.com/books/Sets%20for%20Mathematics.pdf
> >
> > You just reject this definition:
> >
> > A ⊆ B <=> ∀x(x ∈ A => x ∈ B)
> >
> > And go with this definition, note in WILLIAM LAWVERE, the
> > arrows are basically sets:
> >
> > "Historically many mathematicians such as Dedekind
> > and Banach used the same symbol ⊆ for both membership
> > and inclusion, and indeed it is quite reasonable to
> > define x belongs to y for any two maps with codomain A
> > and even to use the same symbol for it"
> > http://patryshev.com/books/Sets%20for%20Mathematics.pdf
> >
> > x ⊆ y <=> ∃z(x = y*z)
> > Ross Finlayson schrieb am Freitag, 4. August 2023 um 08:12:45 UTC+2:
> > > On Thursday, August 3, 2023 at 10:43:59 PM UTC-7, Ross Finlayson wrote:
> > > > On Thursday, August 3, 2023 at 2:45:29 AM UTC-7, Mild Shock wrote:
> > > > > Dana Scott fan club challenge. Show that "obj" as a set
> > > > > and naively modelled here by Dan Christensen:
> > > > >
> > > > > Toward a Formal, Machine-Parsable Definition of a Category
> > > > > https://groups.google.com/g/sci.math/c/gDtJtH8RHvc
> > > > >
> > > > > Cannot be a set if we assume certain category theory equations,
> > > > > which might be seen as consistent in category theory itself.
> > > > >
> > > > > Disclaimer: I don't have such equations just now at hand, working on it.
> > > > > Dan Christensen schrieb am Montag, 17. Juli 2023 um 20:58:43 UTC+2:
> > > > > > > ω
> > > > > > > ω+ω
> > > > > > > ω+ω+ω
> > > > > > > ω+ω+ω+ω
> > > > > > > Etc..
> > > > > > >
> > > > > > Again, this is simply not something that interests me.
> > > > Picked up a copy of a translation one of Kant's less-than-usually-ambitiously-titled
> > > > "On the old saw: That may be right in theory but it won't work in practice",
> > > > and it helps remind me that lots of modern neo-Platonists are pseudo-Platonists
> > > > and that a strong Platonism again is sort of superior for stronger logicists.
> > > >
> > > > It's like when Russell quipped "mathematics is I dunno" ("mathematics is that where
> > > > we never know what we're doing nor whether it's true") and it's like, no, Russell,
> > > > it's pretty much the opposite.
> > > Your rejection of strong platonism won't work in the practice of strong platonism.
> > >
> > > It's pretty simple: you don't have to accept being Russell's dupe.
> > > The Russellian duplicity of the Russellian hypocrisy of the Russell "paradox"
> > > being axiomatized away, it's just a mental convenience for agreeably a large
> > > class of concerns, that if you don't know the difference, and maintain through
> > > all derivations why it's not so, Russell's "I usurped Frege", then, that would
> > > result an ignoramus, who agreeably doesn't need to know the difference,
> > > or a hypocrite, or a charlatan.
> > >
> > >
> > > For foundation's sake though, it's unacceptable.

It's said Quine said "Quine said that ''quotation has a certain anomalous feature''."

https://en.wikipedia.org/wiki/Use%E2%80%93mention_distinction

Here it's kind of that quotation enters a syntax, about syntax, and about the lexical and
syntax, that there's a simple sort of inner and outer syntax, about what results for an
overall language that syntax becomes category and attribute, that symbols as quantities,
reflect that there's overall a context of all the objects, of a universe of objects their language.

Rossy Boy just got expelled from Dana Scott fan club
because of his extraordinary idiocy. He is so clueless
about set theory, even a cat that brings home some

friends is 100 times smarter than Rossy Boy:

Bonjour ! When your cat brings home a friend 🤣
https://www.youtube.com/watch?v=cbjvy5ruIpo

Ross Finlayson schrieb am Samstag, 5. August 2023 um 21:28:28 UTC+2:
> ... usual gibberish nobody cares about ...

On Thursday, August 24, 2023 at 6:03:01 AM UTC-7, Mild Shock wrote:
> Rossy Boy just got expelled from Dana Scott fan club
> because of his extraordinary idiocy. He is so clueless
> about set theory, even a cat that brings home some
>
> friends is 100 times smarter than Rossy Boy:
>
> Bonjour ! When your cat brings home a friend 🤣
> https://www.youtube.com/watch?v=cbjvy5ruIpo
>
> Ross Finlayson schrieb am Samstag, 5. August 2023 um 21:28:28 UTC+2:
> > ... usual gibberish nobody cares about ...

Wow, 100 times, ....

I started this chapter of a Dana Scott fan club and you're welcome
to come and go as you please, the reason why though I'm a fan of
Dana Scott is because he's noticed the hypocrisies that a lot of
people either buy or shill and went and built boolean lattices and
such which make rid of them on their own merits, his own.

I'm pretty sure it's not because of being an irrational, fatuous, flatulent,
flake (or fake). Indeed it's not. But, it's simple to employ such rhetoric,
especially when it's not a real person.

Is Dana Scott a deer, a moose or a raccon, that
you braught with you, Rossy Boy cat?

When your cat brings home a friend 🤣
https://www.youtube.com/watch?v=5g8Z02fsHfI

The biggest hypocrite here on sci.logic and sci.math
is Rossy Boy, which is ironic, the way how uneasy

he feels with logic and/or mathematics.

LoL

Ross Finlayson schrieb am Donnerstag, 24. August 2023 um 18:01:36 UTC+2:
> On Thursday, August 24, 2023 at 6:03:01 AM UTC-7, Mild Shock wrote:
> > Rossy Boy just got expelled from Dana Scott fan club
> > because of his extraordinary idiocy. He is so clueless
> > about set theory, even a cat that brings home some
> >
> > friends is 100 times smarter than Rossy Boy:
> >
> > Bonjour ! When your cat brings home a friend 🤣
> > https://www.youtube.com/watch?v=cbjvy5ruIpo
> >
> > Ross Finlayson schrieb am Samstag, 5. August 2023 um 21:28:28 UTC+2:
> > > ... usual gibberish nobody cares about ...
> Wow, 100 times, ....
>
> I started this chapter of a Dana Scott fan club and you're welcome
> to come and go as you please, the reason why though I'm a fan of
> Dana Scott is because he's noticed the hypocrisies that a lot of
> people either buy or shill and went and built boolean lattices and
> such which make rid of them on their own merits, his own.
>
> I'm pretty sure it's not because of being an irrational, fatuous, flatulent,
> flake (or fake). Indeed it's not. But, it's simple to employ such rhetoric,
> especially when it's not a real person.