On Friday, January 14, 2022 at 9:04:25 AM UTC-8, Mostowski Collapse wrote:
> Well set theory, your prime enemy, solves the problem differently.
> When you use ordinals as for example von Neuman did when
> he was a youngster:
>
> This motivates the **standard** definition, suggested by John von
> Neumann at the age of 19, now called definition of von Neumann
> ordinals: "each ordinal is the well-ordered set of all smaller ordinals."
> https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_definition_of_ordinals
>
> Then you have an easy canonical member inside set theory
> for every order type. In DC Proof for every arbitrary function f
> that is Dedekind infinite, there is some Peano structure,
>
> which one is canonical?

There is nothing 'canonical' about the von Neumann representation

https://en.wikipedia.org/wiki/Benacerraf%27s_identification_problem

On Friday, January 14, 2022 at 12:04:25 PM UTC-5, Mostowski Collapse wrote:
> Well set theory, your prime enemy, solves the problem differently.
> When you use ordinals as for example von Neuman did when
> he was a youngster:
>
> This motivates the **standard** definition, suggested by John von
> Neumann at the age of 19, now called definition of von Neumann
> ordinals: "each ordinal is the well-ordered set of all smaller ordinals."
> https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_definition_of_ordinals
>

Another pedagogical nightmare! In extremely few math textbooks will you find, for example, that 2 is a subset of 4 as at your link. Thanks, but not no thanks, Jan Burse. If students require axioms for the natural numbers, you can't beat simply starting with Peano's Axioms.

Dan

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

Well you can prove the Mostowsky Collapse Lemma.
So inside a model, the transitive set B is unique:

* Mostowski Collapse Lemma: Suppose we have a set 𝐴
* and a relation 𝑅 on 𝐴 which is well-founded and extensional
* ("extensional" means: for all 𝑥,𝑦∈𝐴, if {𝑧∈𝐴∣𝑧𝑅𝑥}={𝑧∈𝐴∣𝑧𝑅𝑦},
* then 𝑥=𝑦 -- and a well-order is automatically extensional).
* Then there exists a unique transitive set 𝐵 such that (𝐴,𝑅)≃(𝐵,∈|𝐵×𝐵).

FredJeffries schrieb am Freitag, 14. Januar 2022 um 18:20:34 UTC+1:
> On Friday, January 14, 2022 at 9:04:25 AM UTC-8, Mostowski Collapse wrote:
> > Well set theory, your prime enemy, solves the problem differently.
> > When you use ordinals as for example von Neuman did when
> > he was a youngster:
> >
> > This motivates the **standard** definition, suggested by John von
> > Neumann at the age of 19, now called definition of von Neumann
> > ordinals: "each ordinal is the well-ordered set of all smaller ordinals.."
> > https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_definition_of_ordinals
> >
> > Then you have an easy canonical member inside set theory
> > for every order type. In DC Proof for every arbitrary function f
> > that is Dedekind infinite, there is some Peano structure,
> >
> > which one is canonical?
> There is nothing 'canonical' about the von Neumann representation
>
> https://en.wikipedia.org/wiki/Benacerraf%27s_identification_problem

But you could also choose another representative.
The reason to choose von Neuman, and why its called
canonical, because its the **standard** in set theory:

So, the von Neumann ordinals get around the issues
with "too big" sets which cannot be constructed in ZFC,
as a "feature not a bug" of ZFC to avoid contradictions
such as Russell's paradox, or the Burali-Forti paradox
specifically related to the class of ordinal numbers (while
these issues are glossed over in naive set theory). Also,
having a representative of each well-order in which the
relation is gotten just from a basic term of the language
of ZFC has numerous technical advantages.
https://math.stackexchange.com/a/2976857/1002973

DC Proof hasn't spent more time than taking a shit
in the morning over many problems of numerosity
and ordering. Nevertheless Dan-O-Matik is the biggest

anti troll against WM and John Gabriel. Whereas
DC Proof is fake nonsense, there is still no proof
of existence of some natural numbers in DC Proof.

Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:24:59 UTC+1:
> Well you can prove the Mostowsky Collapse Lemma.
> So inside a model, the transitive set B is unique:
> * Mostowski Collapse Lemma: Suppose we have a set 𝐴
> * and a relation 𝑅 on 𝐴 which is well-founded and extensional
> * ("extensional" means: for all 𝑥,𝑦∈𝐴, if {𝑧∈𝐴∣𝑧𝑅𝑥}={𝑧∈𝐴∣𝑧𝑅𝑦},
> * then 𝑥=𝑦 -- and a well-order is automatically extensional).
> * Then there exists a unique transitive set 𝐵 such that (𝐴,𝑅)≃(𝐵,∈|𝐵×𝐵).
> FredJeffries schrieb am Freitag, 14. Januar 2022 um 18:20:34 UTC+1:
> > On Friday, January 14, 2022 at 9:04:25 AM UTC-8, Mostowski Collapse wrote:
> > > Well set theory, your prime enemy, solves the problem differently.
> > > When you use ordinals as for example von Neuman did when
> > > he was a youngster:
> > >
> > > This motivates the **standard** definition, suggested by John von
> > > Neumann at the age of 19, now called definition of von Neumann
> > > ordinals: "each ordinal is the well-ordered set of all smaller ordinals."
> > > https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_definition_of_ordinals
> > >
> > > Then you have an easy canonical member inside set theory
> > > for every order type. In DC Proof for every arbitrary function f
> > > that is Dedekind infinite, there is some Peano structure,
> > >
> > > which one is canonical?
> > There is nothing 'canonical' about the von Neumann representation
> >
> > https://en.wikipedia.org/wiki/Benacerraf%27s_identification_problem

Dan-O-Matik doesn't choose some representation.
Well we could say he doesn't have to do so. He could
also work with an equivalence class, or like

for example the class of all Peano structures.
But Dan-O-Matik cannot prove that the class of
Peano structures is non-empty. On the otherhand

in set theory the proof of a representative element c of
course implies also that the corresponding class
C is non-empty, since alas the representative element

is member of the class, c e C. So in the worst case
the class is only {c}, possibly bigger, but it is non-empty.

LoL

Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:30:21 UTC+1:
> But you could also choose another representative.
> The reason to choose von Neuman, and why its called
> canonical, because its the **standard** in set theory:
>
> So, the von Neumann ordinals get around the issues
> with "too big" sets which cannot be constructed in ZFC,
> as a "feature not a bug" of ZFC to avoid contradictions
> such as Russell's paradox, or the Burali-Forti paradox
> specifically related to the class of ordinal numbers (while
> these issues are glossed over in naive set theory). Also,
> having a representative of each well-order in which the
> relation is gotten just from a basic term of the language
> of ZFC has numerous technical advantages.
> https://math.stackexchange.com/a/2976857/1002973
>
> DC Proof hasn't spent more time than taking a shit
> in the morning over many problems of numerosity
> and ordering. Nevertheless Dan-O-Matik is the biggest
>
> anti troll against WM and John Gabriel. Whereas
> DC Proof is fake nonsense, there is still no proof
> of existence of some natural numbers in DC Proof.
> Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:24:59 UTC+1:
> > Well you can prove the Mostowsky Collapse Lemma.
> > So inside a model, the transitive set B is unique:
> > * Mostowski Collapse Lemma: Suppose we have a set 𝐴
> > * and a relation 𝑅 on 𝐴 which is well-founded and extensional
> > * ("extensional" means: for all 𝑥,𝑦∈𝐴, if {𝑧∈𝐴∣𝑧𝑅𝑥}={𝑧∈𝐴∣𝑧𝑅𝑦},
> > * then 𝑥=𝑦 -- and a well-order is automatically extensional).
> > * Then there exists a unique transitive set 𝐵 such that (𝐴,𝑅)≃(𝐵,∈|𝐵×𝐵).
> > FredJeffries schrieb am Freitag, 14. Januar 2022 um 18:20:34 UTC+1:
> > > On Friday, January 14, 2022 at 9:04:25 AM UTC-8, Mostowski Collapse wrote:
> > > > Well set theory, your prime enemy, solves the problem differently.
> > > > When you use ordinals as for example von Neuman did when
> > > > he was a youngster:
> > > >
> > > > This motivates the **standard** definition, suggested by John von
> > > > Neumann at the age of 19, now called definition of von Neumann
> > > > ordinals: "each ordinal is the well-ordered set of all smaller ordinals."
> > > > https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_definition_of_ordinals
> > > >
> > > > Then you have an easy canonical member inside set theory
> > > > for every order type. In DC Proof for every arbitrary function f
> > > > that is Dedekind infinite, there is some Peano structure,
> > > >
> > > > which one is canonical?
> > > There is nothing 'canonical' about the von Neumann representation
> > >
> > > https://en.wikipedia.org/wiki/Benacerraf%27s_identification_problem

Dan-O-Matik halucinated:
> that 2 is a subset of 4 as at your link

You don't have to choose 2 and 4 this way.
You can also choose differently. The main point
would be to show that this collection exists:

{0,1,2,3,...}

Can you show existence of natural numbers in DC Proof.
In set theory omega exists so the class of infinite countable
well ordered sets is non empty.

Is the class of your Peano structures non-empty? I
doubt that you can executed the proof, because of
your recent changes. You cannot prove anymore:

> This is the proof that worked in dcproof2.exe, but
> does not work anymore in dcproof5.exe:
> [...]
> 8 ~Field(constr(a))
> U Spec, 6, 7
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/LGiS4I8UAwAJ

My speculation, technically you possibly cannot executed
the required proof anymore in DC Proof.
Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:36:15 UTC+1:
> Dan-O-Matik doesn't choose some representation.
> Well we could say he doesn't have to do so. He could
> also work with an equivalence class, or like
>
> for example the class of all Peano structures.
> But Dan-O-Matik cannot prove that the class of
> Peano structures is non-empty. On the otherhand
>
> in set theory the proof of a representative element c of
> course implies also that the corresponding class
> C is non-empty, since alas the representative element
>
> is member of the class, c e C. So in the worst case
> the class is only {c}, possibly bigger, but it is non-empty.
>
> LoL
> Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:30:21 UTC+1:
> > But you could also choose another representative.
> > The reason to choose von Neuman, and why its called
> > canonical, because its the **standard** in set theory:
> >
> > So, the von Neumann ordinals get around the issues
> > with "too big" sets which cannot be constructed in ZFC,
> > as a "feature not a bug" of ZFC to avoid contradictions
> > such as Russell's paradox, or the Burali-Forti paradox
> > specifically related to the class of ordinal numbers (while
> > these issues are glossed over in naive set theory). Also,
> > having a representative of each well-order in which the
> > relation is gotten just from a basic term of the language
> > of ZFC has numerous technical advantages.
> > https://math.stackexchange.com/a/2976857/1002973
> >
> > DC Proof hasn't spent more time than taking a shit
> > in the morning over many problems of numerosity
> > and ordering. Nevertheless Dan-O-Matik is the biggest
> >
> > anti troll against WM and John Gabriel. Whereas
> > DC Proof is fake nonsense, there is still no proof
> > of existence of some natural numbers in DC Proof.
> > Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:24:59 UTC+1:
> > > Well you can prove the Mostowsky Collapse Lemma.
> > > So inside a model, the transitive set B is unique:
> > > * Mostowski Collapse Lemma: Suppose we have a set 𝐴
> > > * and a relation 𝑅 on 𝐴 which is well-founded and extensional
> > > * ("extensional" means: for all 𝑥,𝑦∈𝐴, if {𝑧∈𝐴∣𝑧𝑅𝑥}={𝑧∈𝐴∣𝑧𝑅𝑦},
> > > * then 𝑥=𝑦 -- and a well-order is automatically extensional).
> > > * Then there exists a unique transitive set 𝐵 such that (𝐴,𝑅)≃(𝐵,∈|𝐵×𝐵).
> > > FredJeffries schrieb am Freitag, 14. Januar 2022 um 18:20:34 UTC+1:
> > > > On Friday, January 14, 2022 at 9:04:25 AM UTC-8, Mostowski Collapse wrote:
> > > > > Well set theory, your prime enemy, solves the problem differently..
> > > > > When you use ordinals as for example von Neuman did when
> > > > > he was a youngster:
> > > > >
> > > > > This motivates the **standard** definition, suggested by John von
> > > > > Neumann at the age of 19, now called definition of von Neumann
> > > > > ordinals: "each ordinal is the well-ordered set of all smaller ordinals."
> > > > > https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_definition_of_ordinals
> > > > >
> > > > > Then you have an easy canonical member inside set theory
> > > > > for every order type. In DC Proof for every arbitrary function f
> > > > > that is Dedekind infinite, there is some Peano structure,
> > > > >
> > > > > which one is canonical?
> > > > There is nothing 'canonical' about the von Neumann representation
> > > >
> > > > https://en.wikipedia.org/wiki/Benacerraf%27s_identification_problem

Corr.:

Can you show existence of natural numbers in DC Proof.
In set theory omega exists so the class of infinite countable
well ordered sets without limit points is non empty.

Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:44:05 UTC+1:
> Dan-O-Matik halucinated:
> > that 2 is a subset of 4 as at your link
> You don't have to choose 2 and 4 this way.
> You can also choose differently. The main point
> would be to show that this collection exists:
>
> {0,1,2,3,...}
>
> Can you show existence of natural numbers in DC Proof.
> In set theory omega exists so the class of infinite countable
> well ordered sets is non empty.
>
> Is the class of your Peano structures non-empty? I
> doubt that you can executed the proof, because of
> your recent changes. You cannot prove anymore:
> > This is the proof that worked in dcproof2.exe, but
> > does not work anymore in dcproof5.exe:
> > [...]
> > 8 ~Field(constr(a))
> > U Spec, 6, 7
> https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/LGiS4I8UAwAJ
>
> My speculation, technically you possibly cannot executed
> the required proof anymore in DC Proof.
> Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:36:15 UTC+1:
> > Dan-O-Matik doesn't choose some representation.
> > Well we could say he doesn't have to do so. He could
> > also work with an equivalence class, or like
> >
> > for example the class of all Peano structures.
> > But Dan-O-Matik cannot prove that the class of
> > Peano structures is non-empty. On the otherhand
> >
> > in set theory the proof of a representative element c of
> > course implies also that the corresponding class
> > C is non-empty, since alas the representative element
> >
> > is member of the class, c e C. So in the worst case
> > the class is only {c}, possibly bigger, but it is non-empty.
> >
> > LoL
> > Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:30:21 UTC+1:
> > > But you could also choose another representative.
> > > The reason to choose von Neuman, and why its called
> > > canonical, because its the **standard** in set theory:
> > >
> > > So, the von Neumann ordinals get around the issues
> > > with "too big" sets which cannot be constructed in ZFC,
> > > as a "feature not a bug" of ZFC to avoid contradictions
> > > such as Russell's paradox, or the Burali-Forti paradox
> > > specifically related to the class of ordinal numbers (while
> > > these issues are glossed over in naive set theory). Also,
> > > having a representative of each well-order in which the
> > > relation is gotten just from a basic term of the language
> > > of ZFC has numerous technical advantages.
> > > https://math.stackexchange.com/a/2976857/1002973
> > >
> > > DC Proof hasn't spent more time than taking a shit
> > > in the morning over many problems of numerosity
> > > and ordering. Nevertheless Dan-O-Matik is the biggest
> > >
> > > anti troll against WM and John Gabriel. Whereas
> > > DC Proof is fake nonsense, there is still no proof
> > > of existence of some natural numbers in DC Proof.
> > > Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:24:59 UTC+1:
> > > > Well you can prove the Mostowsky Collapse Lemma.
> > > > So inside a model, the transitive set B is unique:
> > > > * Mostowski Collapse Lemma: Suppose we have a set 𝐴
> > > > * and a relation 𝑅 on 𝐴 which is well-founded and extensional
> > > > * ("extensional" means: for all 𝑥,𝑦∈𝐴, if {𝑧∈𝐴∣𝑧𝑅𝑥}={𝑧∈𝐴∣𝑧𝑅𝑦},
> > > > * then 𝑥=𝑦 -- and a well-order is automatically extensional).
> > > > * Then there exists a unique transitive set 𝐵 such that (𝐴,𝑅)≃(𝐵,∈|𝐵×𝐵).
> > > > FredJeffries schrieb am Freitag, 14. Januar 2022 um 18:20:34 UTC+1:
> > > > > On Friday, January 14, 2022 at 9:04:25 AM UTC-8, Mostowski Collapse wrote:
> > > > > > Well set theory, your prime enemy, solves the problem differently.
> > > > > > When you use ordinals as for example von Neuman did when
> > > > > > he was a youngster:
> > > > > >
> > > > > > This motivates the **standard** definition, suggested by John von
> > > > > > Neumann at the age of 19, now called definition of von Neumann
> > > > > > ordinals: "each ordinal is the well-ordered set of all smaller ordinals."
> > > > > > https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_definition_of_ordinals
> > > > > >
> > > > > > Then you have an easy canonical member inside set theory
> > > > > > for every order type. In DC Proof for every arbitrary function f
> > > > > > that is Dedekind infinite, there is some Peano structure,
> > > > > >
> > > > > > which one is canonical?
> > > > > There is nothing 'canonical' about the von Neumann representation
> > > > >
> > > > > https://en.wikipedia.org/wiki/Benacerraf%27s_identification_problem

On Friday, January 14, 2022 at 12:30:21 PM UTC-5, Mostowski Collapse wrote:

> ... there is still no proof
> of existence of some natural numbers in DC Proof.

In DC Proof, there is no assumption of a non-empty universe. None of its axioms of set theory postulate the existence of any set or other object, not even the empty set. So, there are no existential theorems in DC Proof, i.e. no theorems of the form EXIST(a):P(a). Peano's Axioms, which effectively define the natural numbers, are self-evident and very intuitive and can be introduced by the user at the beginning of any proof.

Dan

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

WHATS WRONG WITH YOU???????????????

Dan-O-Matik went bozo:
> None of its axioms of set theory postulate the existence
of any set or other object, not even the empty set.

Wrong I can use a menu item for Peano:

1 Set(n)
Axiom

2 1 ε n
Axiom

Etc...

No I can prove the empty set:

1 Set(n)
Axiom

2 1 ε n
Axiom

3 ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
Axiom

4 ALL(a):[a ε n => ~a+1=1]
Axiom

5 ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
Axiom

6 ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
Axiom

7 ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a] => ALL(b):[b ε n => b ε a]]
Axiom

8 EXIST(e):[Set(e) & ALL(x):[x ε e <=> x ε n & x+1=1]]
Subset, 1

9 ~EXIST(e):[Set(e) & ALL(x):~x ε e]
Premise

10 Set(b) & ALL(x):[x ε b <=> x ε n & x+1=1]
E Spec, 8

11 Set(b)
Split, 10

12 ALL(x):[x ε b <=> x ε n & x+1=1]
Split, 10

13 ~~ALL(e):~[Set(e) & ALL(x):~x ε e]
Quant, 9

14 ALL(e):~[Set(e) & ALL(x):~x ε e]
Rem DNeg, 13

15 ~[Set(b) & ALL(x):~x ε b]
U Spec, 14

16 ~~[~Set(b) | ~ALL(x):~x ε b]
DeMorgan, 15

17 ~Set(b) | ~ALL(x):~x ε b
Rem DNeg, 16

18 ~~Set(b) => ~ALL(x):~x ε b
Imply-Or, 17

19 Set(b) => ~ALL(x):~x ε b
Rem DNeg, 18

20 ~ALL(x):~x ε b
Detach, 19, 11

21 ~~EXIST(x):~~x ε b
Quant, 20

22 EXIST(x):~~x ε b
Rem DNeg, 21

23 EXIST(x):x ε b
Rem DNeg, 22

24 c ε b
E Spec, 23

25 c ε b <=> c ε n & c+1=1
U Spec, 12

26 [c ε b => c ε n & c+1=1] & [c ε n & c+1=1 => c ε b]
Iff-And, 25

27 c ε b => c ε n & c+1=1
Split, 26

28 c ε n & c+1=1 => c ε b
Split, 26

29 c ε n => ~c+1=1
U Spec, 4

30 c ε n & c+1=1
Detach, 27, 24

31 c ε n
Split, 30

32 c+1=1
Split, 30

33 ~c+1=1
Detach, 29, 31

34 c+1=1 & ~c+1=1
Join, 32, 33

35 ~~EXIST(e):[Set(e) & ALL(x):~x ε e]
Conclusion, 9

36 EXIST(e):[Set(e) & ALL(x):~x ε e]
Rem DNeg, 35

Dan Christensen schrieb am Freitag, 14. Januar 2022 um 18:46:47 UTC+1:
> On Friday, January 14, 2022 at 12:30:21 PM UTC-5, Mostowski Collapse wrote:
>
> > ... there is still no proof
> > of existence of some natural numbers in DC Proof.
> In DC Proof, there is no assumption of a non-empty universe. None of its axioms of set theory postulate the existence of any set or other object, not even the empty set. So, there are no existential theorems in DC Proof, i.e. no theorems of the form EXIST(a):P(a). Peano's Axioms, which effectively define the natural numbers, are self-evident and very intuitive and can be introduced by the user at the beginning of any 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 Sunday, January 16, 2022 at 3:06:10 PM UTC-5, Mostowski Collapse wrote:
> WHATS WRONG WITH YOU???????????????
>
> Dan-O-Matik went bozo:
> > None of its axioms of set theory postulate the existence
> of any set or other object, not even the empty set.
> Wrong I can use a menu item for Peano:
>
> 1 Set(n)
> Axiom
>

This axiom is not built into the set theory of DC Proof. It would have to have been manually keyed in by the user. But you knew this, didn't you, Jan Burse? What is your problem???

Dan

On Sunday, January 16, 2022 at 3:06:10 PM UTC-5, Mostowski Collapse wrote:
> WHATS WRONG WITH YOU???????????????
>

Do you enjoy being an asshole, Jan Burse?

> Dan-O-Matik went bozo:
> > None of its axioms of set theory postulate the existence
> of any set or other object, not even the empty set.
> Wrong I can use a menu item for Peano:
>

The set theory in DC Proof is included the Sets and Logic menus. The axioms you list here are supplementary material for the tutorial so students or teachers wouldn't have to key them in. I never use them in my own proofs here or at the blog. I only the Sets and Logic menus for writing proofs.

> 1 Set(n)
> Axiom
>
> 2 1 ε n
> Axiom
>
> Etc...
>

Dan

Now I am waiting for dcproof6.exe, it will have
a new Subset axiom, that forbids that empty
sets are created. The similarity to WM are

cunning. WM has already ranted about the
empty set, so make it the scape goat of
DC Proofs failure? LoL

Mostowski Collapse schrieb am Sonntag, 16. Januar 2022 um 21:06:10 UTC+1:
> WHATS WRONG WITH YOU???????????????
>
> Dan-O-Matik went bozo:
> > None of its axioms of set theory postulate the existence
> of any set or other object, not even the empty set.
> Wrong I can use a menu item for Peano:
>
> 1 Set(n)
> Axiom
>
> 2 1 ε n
> Axiom
>
> Etc...
>
> No I can prove the empty set:
>
> 1 Set(n)
> Axiom
>
> 2 1 ε n
> Axiom
>
> 3 ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
> Axiom
>
> 4 ALL(a):[a ε n => ~a+1=1]
> Axiom
>
> 5 ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
> Axiom
>
> 6 ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
> Axiom
>
> 7 ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a] => ALL(b):[b ε n => b ε a]]
> Axiom
>
> 8 EXIST(e):[Set(e) & ALL(x):[x ε e <=> x ε n & x+1=1]]
> Subset, 1
>
> 9 ~EXIST(e):[Set(e) & ALL(x):~x ε e]
> Premise
>
> 10 Set(b) & ALL(x):[x ε b <=> x ε n & x+1=1]
> E Spec, 8
>
> 11 Set(b)
> Split, 10
>
> 12 ALL(x):[x ε b <=> x ε n & x+1=1]
> Split, 10
>
> 13 ~~ALL(e):~[Set(e) & ALL(x):~x ε e]
> Quant, 9
>
> 14 ALL(e):~[Set(e) & ALL(x):~x ε e]
> Rem DNeg, 13
>
> 15 ~[Set(b) & ALL(x):~x ε b]
> U Spec, 14
>
> 16 ~~[~Set(b) | ~ALL(x):~x ε b]
> DeMorgan, 15
>
> 17 ~Set(b) | ~ALL(x):~x ε b
> Rem DNeg, 16
>
> 18 ~~Set(b) => ~ALL(x):~x ε b
> Imply-Or, 17
>
> 19 Set(b) => ~ALL(x):~x ε b
> Rem DNeg, 18
>
> 20 ~ALL(x):~x ε b
> Detach, 19, 11
>
> 21 ~~EXIST(x):~~x ε b
> Quant, 20
>
> 22 EXIST(x):~~x ε b
> Rem DNeg, 21
>
> 23 EXIST(x):x ε b
> Rem DNeg, 22
>
> 24 c ε b
> E Spec, 23
>
> 25 c ε b <=> c ε n & c+1=1
> U Spec, 12
>
> 26 [c ε b => c ε n & c+1=1] & [c ε n & c+1=1 => c ε b]
> Iff-And, 25
>
> 27 c ε b => c ε n & c+1=1
> Split, 26
>
> 28 c ε n & c+1=1 => c ε b
> Split, 26
>
> 29 c ε n => ~c+1=1
> U Spec, 4
>
> 30 c ε n & c+1=1
> Detach, 27, 24
>
> 31 c ε n
> Split, 30
>
> 32 c+1=1
> Split, 30
>
> 33 ~c+1=1
> Detach, 29, 31
>
> 34 c+1=1 & ~c+1=1
> Join, 32, 33
>
> 35 ~~EXIST(e):[Set(e) & ALL(x):~x ε e]
> Conclusion, 9
>
> 36 EXIST(e):[Set(e) & ALL(x):~x ε e]
> Rem DNeg, 35
> Dan Christensen schrieb am Freitag, 14. Januar 2022 um 18:46:47 UTC+1:
> > On Friday, January 14, 2022 at 12:30:21 PM UTC-5, Mostowski Collapse wrote:
> >
> > > ... there is still no proof
> > > of existence of some natural numbers in DC Proof.
> > In DC Proof, there is no assumption of a non-empty universe. None of its axioms of set theory postulate the existence of any set or other object, not even the empty set. So, there are no existential theorems in DC Proof, i.e. no theorems of the form EXIST(a):P(a). Peano's Axioms, which effectively define the natural numbers, are self-evident and very intuitive and can be introduced by the user at the beginning of any proof.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Ha Ha, cringe:

> The axioms you list here are supplementary
material for the tutorial so students or teachers
wouldn't have to key them in. I never use them in my
own proofs here or at the blog.

Well I don't need them. I only need:

> 1 Set(n)
> Axiom
>
> 2 1 ε n
> Axiom

I could also do comprehension (Subset Axiom) with:

~1 ε n & 1 ε n

But using x+1=1 was shorter. Although the proof got lengthier.

So you say there will be no empty set when I use:

1 Set(n)
Axiom

2 0 ε n
Axiom

Why? I can then do comprehension (Subset Axiom) with:

~0 ε n & 0 ε n

Got it? LoL

Mostowski Collapse schrieb am Sonntag, 16. Januar 2022 um 22:22:06 UTC+1:
> Now I am waiting for dcproof6.exe, it will have
> a new Subset axiom, that forbids that empty
> sets are created. The similarity to WM are
>
> cunning. WM has already ranted about the
> empty set, so make it the scape goat of
> DC Proofs failure? LoL
> Mostowski Collapse schrieb am Sonntag, 16. Januar 2022 um 21:06:10 UTC+1:
> > WHATS WRONG WITH YOU???????????????
> >
> > Dan-O-Matik went bozo:
> > > None of its axioms of set theory postulate the existence
> > of any set or other object, not even the empty set.
> > Wrong I can use a menu item for Peano:
> >
> > 1 Set(n)
> > Axiom
> >
> > 2 1 ε n
> > Axiom
> >
> > Etc...
> >
> > No I can prove the empty set:
> >
> > 1 Set(n)
> > Axiom
> >
> > 2 1 ε n
> > Axiom
> >
> > 3 ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
> > Axiom
> >
> > 4 ALL(a):[a ε n => ~a+1=1]
> > Axiom
> >
> > 5 ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
> > Axiom
> >
> > 6 ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
> > Axiom
> >
> > 7 ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a] => ALL(b):[b ε n => b ε a]]
> > Axiom
> >
> > 8 EXIST(e):[Set(e) & ALL(x):[x ε e <=> x ε n & x+1=1]]
> > Subset, 1
> >
> > 9 ~EXIST(e):[Set(e) & ALL(x):~x ε e]
> > Premise
> >
> > 10 Set(b) & ALL(x):[x ε b <=> x ε n & x+1=1]
> > E Spec, 8
> >
> > 11 Set(b)
> > Split, 10
> >
> > 12 ALL(x):[x ε b <=> x ε n & x+1=1]
> > Split, 10
> >
> > 13 ~~ALL(e):~[Set(e) & ALL(x):~x ε e]
> > Quant, 9
> >
> > 14 ALL(e):~[Set(e) & ALL(x):~x ε e]
> > Rem DNeg, 13
> >
> > 15 ~[Set(b) & ALL(x):~x ε b]
> > U Spec, 14
> >
> > 16 ~~[~Set(b) | ~ALL(x):~x ε b]
> > DeMorgan, 15
> >
> > 17 ~Set(b) | ~ALL(x):~x ε b
> > Rem DNeg, 16
> >
> > 18 ~~Set(b) => ~ALL(x):~x ε b
> > Imply-Or, 17
> >
> > 19 Set(b) => ~ALL(x):~x ε b
> > Rem DNeg, 18
> >
> > 20 ~ALL(x):~x ε b
> > Detach, 19, 11
> >
> > 21 ~~EXIST(x):~~x ε b
> > Quant, 20
> >
> > 22 EXIST(x):~~x ε b
> > Rem DNeg, 21
> >
> > 23 EXIST(x):x ε b
> > Rem DNeg, 22
> >
> > 24 c ε b
> > E Spec, 23
> >
> > 25 c ε b <=> c ε n & c+1=1
> > U Spec, 12
> >
> > 26 [c ε b => c ε n & c+1=1] & [c ε n & c+1=1 => c ε b]
> > Iff-And, 25
> >
> > 27 c ε b => c ε n & c+1=1
> > Split, 26
> >
> > 28 c ε n & c+1=1 => c ε b
> > Split, 26
> >
> > 29 c ε n => ~c+1=1
> > U Spec, 4
> >
> > 30 c ε n & c+1=1
> > Detach, 27, 24
> >
> > 31 c ε n
> > Split, 30
> >
> > 32 c+1=1
> > Split, 30
> >
> > 33 ~c+1=1
> > Detach, 29, 31
> >
> > 34 c+1=1 & ~c+1=1
> > Join, 32, 33
> >
> > 35 ~~EXIST(e):[Set(e) & ALL(x):~x ε e]
> > Conclusion, 9
> >
> > 36 EXIST(e):[Set(e) & ALL(x):~x ε e]
> > Rem DNeg, 35
> > Dan Christensen schrieb am Freitag, 14. Januar 2022 um 18:46:47 UTC+1:
> > > On Friday, January 14, 2022 at 12:30:21 PM UTC-5, Mostowski Collapse wrote:
> > >
> > > > ... there is still no proof
> > > > of existence of some natural numbers in DC Proof.
> > > In DC Proof, there is no assumption of a non-empty universe. None of its axioms of set theory postulate the existence of any set or other object, not even the empty set. So, there are no existential theorems in DC Proof, i.e. no theorems of the form EXIST(a):P(a). Peano's Axioms, which effectively define the natural numbers, are self-evident and very intuitive and can be introduced by the user at the beginning of any proof.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

Actually I need only:

1 Set(n)
Axiom

I could then use Subset axiom with the formula:

~Set(n)

This would be the shortest. Or is there a FALSUM
constant in DC Proof? On the other hand, the most
important is not the formula that is used in your

Subset axiom, but that I have at least one set, here n,
as the the set over which to perform the comprehension
in your Subset axiom.

Mostowski Collapse schrieb am Sonntag, 16. Januar 2022 um 22:27:22 UTC+1:
> Ha Ha, cringe:
> > The axioms you list here are supplementary
> material for the tutorial so students or teachers
> wouldn't have to key them in. I never use them in my
> own proofs here or at the blog.
> Well I don't need them. I only need:
> > 1 Set(n)
> > Axiom
> >
> > 2 1 ε n
> > Axiom
> I could also do comprehension (Subset Axiom) with:
>
> ~1 ε n & 1 ε n
>
> But using x+1=1 was shorter. Although the proof got lengthier.
>
> So you say there will be no empty set when I use:
>
> 1 Set(n)
> Axiom
>
> 2 0 ε n
> Axiom
>
> Why? I can then do comprehension (Subset Axiom) with:
>
> ~0 ε n & 0 ε n
>
> Got it? LoL
> Mostowski Collapse schrieb am Sonntag, 16. Januar 2022 um 22:22:06 UTC+1:
> > Now I am waiting for dcproof6.exe, it will have
> > a new Subset axiom, that forbids that empty
> > sets are created. The similarity to WM are
> >
> > cunning. WM has already ranted about the
> > empty set, so make it the scape goat of
> > DC Proofs failure? LoL
> > Mostowski Collapse schrieb am Sonntag, 16. Januar 2022 um 21:06:10 UTC+1:
> > > WHATS WRONG WITH YOU???????????????
> > >
> > > Dan-O-Matik went bozo:
> > > > None of its axioms of set theory postulate the existence
> > > of any set or other object, not even the empty set.
> > > Wrong I can use a menu item for Peano:
> > >
> > > 1 Set(n)
> > > Axiom
> > >
> > > 2 1 ε n
> > > Axiom
> > >
> > > Etc...
> > >
> > > No I can prove the empty set:
> > >
> > > 1 Set(n)
> > > Axiom
> > >
> > > 2 1 ε n
> > > Axiom
> > >
> > > 3 ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
> > > Axiom
> > >
> > > 4 ALL(a):[a ε n => ~a+1=1]
> > > Axiom
> > >
> > > 5 ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
> > > Axiom
> > >
> > > 6 ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
> > > Axiom
> > >
> > > 7 ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a] => ALL(b):[b ε n => b ε a]]
> > > Axiom
> > >
> > > 8 EXIST(e):[Set(e) & ALL(x):[x ε e <=> x ε n & x+1=1]]
> > > Subset, 1
> > >
> > > 9 ~EXIST(e):[Set(e) & ALL(x):~x ε e]
> > > Premise
> > >
> > > 10 Set(b) & ALL(x):[x ε b <=> x ε n & x+1=1]
> > > E Spec, 8
> > >
> > > 11 Set(b)
> > > Split, 10
> > >
> > > 12 ALL(x):[x ε b <=> x ε n & x+1=1]
> > > Split, 10
> > >
> > > 13 ~~ALL(e):~[Set(e) & ALL(x):~x ε e]
> > > Quant, 9
> > >
> > > 14 ALL(e):~[Set(e) & ALL(x):~x ε e]
> > > Rem DNeg, 13
> > >
> > > 15 ~[Set(b) & ALL(x):~x ε b]
> > > U Spec, 14
> > >
> > > 16 ~~[~Set(b) | ~ALL(x):~x ε b]
> > > DeMorgan, 15
> > >
> > > 17 ~Set(b) | ~ALL(x):~x ε b
> > > Rem DNeg, 16
> > >
> > > 18 ~~Set(b) => ~ALL(x):~x ε b
> > > Imply-Or, 17
> > >
> > > 19 Set(b) => ~ALL(x):~x ε b
> > > Rem DNeg, 18
> > >
> > > 20 ~ALL(x):~x ε b
> > > Detach, 19, 11
> > >
> > > 21 ~~EXIST(x):~~x ε b
> > > Quant, 20
> > >
> > > 22 EXIST(x):~~x ε b
> > > Rem DNeg, 21
> > >
> > > 23 EXIST(x):x ε b
> > > Rem DNeg, 22
> > >
> > > 24 c ε b
> > > E Spec, 23
> > >
> > > 25 c ε b <=> c ε n & c+1=1
> > > U Spec, 12
> > >
> > > 26 [c ε b => c ε n & c+1=1] & [c ε n & c+1=1 => c ε b]
> > > Iff-And, 25
> > >
> > > 27 c ε b => c ε n & c+1=1
> > > Split, 26
> > >
> > > 28 c ε n & c+1=1 => c ε b
> > > Split, 26
> > >
> > > 29 c ε n => ~c+1=1
> > > U Spec, 4
> > >
> > > 30 c ε n & c+1=1
> > > Detach, 27, 24
> > >
> > > 31 c ε n
> > > Split, 30
> > >
> > > 32 c+1=1
> > > Split, 30
> > >
> > > 33 ~c+1=1
> > > Detach, 29, 31
> > >
> > > 34 c+1=1 & ~c+1=1
> > > Join, 32, 33
> > >
> > > 35 ~~EXIST(e):[Set(e) & ALL(x):~x ε e]
> > > Conclusion, 9
> > >
> > > 36 EXIST(e):[Set(e) & ALL(x):~x ε e]
> > > Rem DNeg, 35
> > > Dan Christensen schrieb am Freitag, 14. Januar 2022 um 18:46:47 UTC+1:
> > > > On Friday, January 14, 2022 at 12:30:21 PM UTC-5, Mostowski Collapse wrote:
> > > >
> > > > > ... there is still no proof
> > > > > of existence of some natural numbers in DC Proof.
> > > > In DC Proof, there is no assumption of a non-empty universe. None of its axioms of set theory postulate the existence of any set or other object, not even the empty set. So, there are no existential theorems in DC Proof, i.e. no theorems of the form EXIST(a):P(a). Peano's Axioms, which effectively define the natural numbers, are self-evident and very intuitive and can be introduced by the user at the beginning of any proof.
> > > > Dan
> > > >
> > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > Visit my Math Blog at http://www.dcproof.wordpress.com

If you insist, that I should not use Peano with your Set Theory!!
How should I do that? I would like to do that, but your DC Proof

got broken recently. You changed the forall rule, and now
the forall rule asks for some f(x) e S. So set-less Peano does
not work anymore, I can even not prove this here anymore:

∀x∃y(y=f(x) ∧ ∀z(z=f(x) → y=z)) is valid.
https://www.umsu.de/trees/#~6x~7y%28y=f%28x%29~1~6z%28z=f%28x%29~5y=z%29%29

Its not anymore provable in DC Proof. LoL But you can check
yourself, this part of Landau was set-less, no x e N side
conditions in Landau screenshot:

MSE Question has Landau screenshot
[(e,f,g)∈d⟹(e,S(f),S(g))∈d]
Dan-O-Matiks Add Construction
https://math.stackexchange.com/a/784504/1002973

So whats going on here?

Dan Christensen schrieb am Montag, 17. Januar 2022 um 02:19:29 UTC+1:
> The axioms of set theory do NOT include Peano's Axioms. In DC Proof, the axioms of set theory are listed on the Sets menu. But you know this, don't you, Jan Burse? Why are you behaving like this, Jan Burse?

Mostowski Collapse wrote:

> If you insist, that I should not use Peano with your Set Theory!!
> How should I do that? I would like to do that, but your DC Proof
>
> got broken recently. You changed the forall rule, and now the forall
> rule asks for some f(x) e S. So set-less Peano does not work anymore, I
> can even not prove this here anymore:

PRESIDENT OF EU PARLIAMENT DIES FROM RAPID ONSET OF AIDS DUE TO VACCINE...
https://www.bitchute.com/video/mdK8K1KHDIAC/

On Sunday, January 16, 2022 at 4:27:22 PM UTC-5, Mostowski Collapse wrote:

> Well I don't need them. I only need:
> > 1 Set(n)
> > Axiom
> >
> > 2 1 ε n

You don't even need that. See below.

> > Axiom
> I could also do comprehension (Subset Axiom) with:
>
> ~1 ε n & 1 ε n
>
> But using x+1=1 was shorter. Although the proof got lengthier.
>
> So you say there will be no empty set when I use:
>
> 1 Set(n)
> Axiom
>
> 2 0 ε n
> Axiom
>
> Why? I can then do comprehension (Subset Axiom) with:
>
> ~0 ε n & 0 ε n
>

Hint: Try...

1. Set(x)
Premise

2. EXIST(a):[Set(a) & ALL(b):[b in a <=> b in x & ~b in x]]
Subset, 1

3. Set(y) & ALL(b):[b in y <=> b in x & ~b in x]
E Spec, 2

Then prove by contradiction that y is empty. I hope this helps.

Dan

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

Q: How do you use DC poop to prove Landau's:

∀x∀y(x + y = y + x)

A: Not at all, it doesn't use x e N. LoL

P.S.: Here is a proof in Landau, using tree tool https://www.umsu.de/trees:

1) First prove by induction that ∀x(0 + x = x).
Base Case: 0 + 0 = 0
∀xa(x,0)=x → a(0,0)=0 is valid.
Induction Step: 0 + x = x => 0 + s(x) = s(x)
∀x∀ya(x,s(y))=s(a(x,y)) → ∀x(a(0,x)=x → a(0,s(x))=s(x)) is valid.

2) Now prove by induction that ∀x∀y(s(y) + x = s(y + x))
Base Case: ∀y(s(y) + 0 = s(y + 0))
∀xa(x,0)=x → ∀ya(s(y),0)=s(a(y,0)) is valid.
Induction Step: ∀y(s(y) + x = s(y + x)) => ∀y(s(y) + s(x) = s(y + s(x)))
∀x∀ya(x,s(y))=s(a(x,y)) → ∀x(∀ya(s(y),x)=s(a(y,x)) → ∀ya(s(y),s(x))=s(a(y,s(x)))) is valid.

3) Finally prove by induction that ∀x∀y(x + y = y + x)
Base Case: 0 + y = y + 0, using 1)
(∀xa(x,0)=x ∧ ∀xa(0,x)=x) → ∀ya(0,y)=a(y,0) is valid.
Induction Step: x + y = y + x => s(x) + y = y + s(x), using 2)
(∀x∀ya(x,s(y))=s(a(x,y)) ∧ ∀x∀ya(s(y),x)=s(a(x,y))) → ∀x(∀ya(x,y)=a(y,x) → ∀ya(s(x),y)=a(y,s(x))) is valid.

Q.E.D.

Mostowski Collapse wrote:

> Q: How do you use DC poop to prove Landau's: ∀x∀y(x + y = y + x)
> A: Not at all, it doesn't use x e N. LoL

why did you fake money capitalists bombed Yugoslavia, then?

Ha Ha, Crypto Rich too much fondlig with his pedophile
pope, made is brain melt. Every goog logician knows:

human(DavidSassoli)
∀x(human(x) => mortal(x))
----------------------------------------------
mortal(DavidSassoli)

So who cares?

Crypto Rich schrieb am Mittwoch, 19. Januar 2022 um 18:26:25 UTC+1:
> Mostowski Collapse wrote:
>
> > If you insist, that I should not use Peano with your Set Theory!!
> > How should I do that? I would like to do that, but your DC Proof
> >
> > got broken recently. You changed the forall rule, and now the forall
> > rule asks for some f(x) e S. So set-less Peano does not work anymore, I
> > can even not prove this here anymore:
> PRESIDENT OF EU PARLIAMENT DIES FROM RAPID ONSET OF AIDS DUE TO VACCINE....
> https://www.bitchute.com/video/mdK8K1KHDIAC/

Only exception is in DC poop, we cannot prove:

human(VicePresident(EuropeanParliament)))
∀x(human(x) => mortal(x))
----------------------------------------------
mortal(VicePresident(EuropeanParliament)))

LoL

Mostowski Collapse schrieb am Freitag, 21. Januar 2022 um 01:50:40 UTC+1:
> Ha Ha, Crypto Rich too much fondlig with his pedophile
> pope, made is brain melt. Every goog logician knows:
>
> human(DavidSassoli)
> ∀x(human(x) => mortal(x))
> ----------------------------------------------
> mortal(DavidSassoli)
>
> So who cares?
> Crypto Rich schrieb am Mittwoch, 19. Januar 2022 um 18:26:25 UTC+1:
> > Mostowski Collapse wrote:
> >
> > > If you insist, that I should not use Peano with your Set Theory!!
> > > How should I do that? I would like to do that, but your DC Proof
> > >
> > > got broken recently. You changed the forall rule, and now the forall
> > > rule asks for some f(x) e S. So set-less Peano does not work anymore, I
> > > can even not prove this here anymore:
> > PRESIDENT OF EU PARLIAMENT DIES FROM RAPID ONSET OF AIDS DUE TO VACCINE....
> > https://www.bitchute.com/video/mdK8K1KHDIAC/

Its rather the other way around. You proved too
much. Please read Landau carefully. He only said:

"To every pair of numbers x, y, we may assign
exactly one way a natural number"

This can be cast as:

∀x ∀y ∃!z (x + y = z)

Which translates to:

∀x ∀y ∃z (x + y = z)
∀x ∀y ∀z ∀t (x + y = z & x + y = t => z = t)

But this trivially valid in FOL=:

∀x∀y∃za(x,y)=z is valid.
https://www.umsu.de/trees/#~6x~6y~7z%28a%28x,y%29=z%29

∀x∀y∀z∀t((a(x,y)=z ∧ a(x,y)=t) → z=t) is valid.
https://www.umsu.de/trees/#~6x~6y~6z~6t%28a%28x,y%29=z~1a%28x,y%29=t~5z=t%29

If you want to interpret Landaus "assign" differently,
in the sense of "by finite means", your proof does nothing.
You then need to go into recursion theory, and for

example show that a certain operator Φ is not only
monotonic, but also continous, and then the fixpoint
can be computed by finite union, no hierarchy jumps:

lfp(Φ) = union_n e N Φ^n

But you don't prove anything like this.

Mostowski Collapse schrieb:
> Its rather the other way around. You proved too
> much. Please read Landau carefully. He only said:
>
> "To every pair of numbers x, y, we may assign
> exactly one way a natural number"
>
> This can be cast as:
>
> ∀x ∀y ∃!z (x + y = z)
>
> Which translates to:
>
> ∀x ∀y ∃z (x + y = z)
> ∀x ∀y ∀z ∀t (x + y = z & x + y = t => z = t)
>
> But this trivially valid in FOL=:
>
> ∀x∀y∃za(x,y)=z is valid.
> https://www.umsu.de/trees/#~6x~6y~7z%28a%28x,y%29=z%29
>
> ∀x∀y∀z∀t((a(x,y)=z ∧ a(x,y)=t) → z=t) is valid.
> https://www.umsu.de/trees/#~6x~6y~6z~6t%28a%28x,y%29=z~1a%28x,y%29=t~5z=t%29
>

The problem is, math stackexchange is not the
right place to learn anything mathematics or
anything computer science.

Just imagine that you Dan-O-Matik, the anti-
troll that is himself the biggest crank has
access to math stackexchange, then

you can imagine how cranks begat each other
on math stackexchange with utter nonsense.
The Landau question is a typical example,

and answer says:

"Whenever you define something, it's essential
to prove that the thing being defined both
exists and is unique. Otherwise the definition
is meaningless."
https://math.stackexchange.com/a/783951/1002973

The technical term for such a definition,
which is unique is "welldefined". It is not
meaningless. For example I can define:

def(X) :<=> X=1 v X=2.

So what, its not meaningless. I have accused
stackoverflow of bitrot, since it doesn't allow
deletion, and hence it is often not in sync

with actual releases of software on the market.
But math stackexchange can be accused of not
being in sync with anything real mathematics

or computer science. Its kind of a bloated rot
of clown nonsense, extremly remote from the
question that are dealt with in math and cs.

Mostowski Collapse schrieb:
> If you want to interpret Landaus "assign" differently,
> in  the sense of "by finite means", your proof does nothing.
> You then need to go into recursion theory, and for
>
> example show that a certain operator Φ is not only
> monotonic, but also continous, and then the fixpoint
> can be computed by finite union, no hierarchy jumps:
>
> lfp(Φ) = union_n e N Φ^n
>
> But you don't prove anything like this.
>
> Mostowski Collapse schrieb:
>> Its rather the other way around. You proved too
>> much. Please read Landau carefully. He only said:
>>
>> "To every pair of numbers x, y, we may assign
>> exactly one way a natural number"
>>
>> This can be cast as:
>>
>> ∀x ∀y ∃!z (x + y = z)
>>
>> Which translates to:
>>
>> ∀x ∀y ∃z (x + y = z)
>> ∀x ∀y ∀z ∀t (x + y = z & x + y = t => z = t)
>>
>> But this trivially valid in FOL=:
>>
>> ∀x∀y∃za(x,y)=z is valid.
>> https://www.umsu.de/trees/#~6x~6y~7z%28a%28x,y%29=z%29
>>
>> ∀x∀y∀z∀t((a(x,y)=z ∧ a(x,y)=t) → z=t) is valid.
>> https://www.umsu.de/trees/#~6x~6y~6z~6t%28a%28x,y%29=z~1a%28x,y%29=t~5z=t%29
>>
>

On Friday, January 21, 2022 at 1:19:17 PM UTC-5, Mostowski Collapse wrote:
> Its rather the other way around. You proved too
> much. Please read Landau carefully. He only said:
>
> "To every pair of numbers x, y, we may assign
> exactly one way a natural number"
>
> This can be cast as:
>
> ∀x ∀y ∃!z (x + y = z)
>
> Which translates to:
>
> ∀x ∀y ∃z (x + y = z)
> ∀x ∀y ∀z ∀t (x + y = z & x + y = t => z = t)
>

The same is true of ANY binary function on a given set. You have A=B and A=C, therefore B=C. Nothing profound there. This is certainly no substitute for a formal proof of existence of the addition function on N, as I have given here:

https://www.dcproof.com/ConstructAdditionNew.htm

Dan

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