Not less wonky than DC Proof. Most dcproof2.exe proofs
dont work anymore in dcproof5.exe?

And why? Because of some fear that without f(x) e S,
we would reach into some evil shadow.

LMAO!

Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 17:42:11 UTC+1:
> On Thursday, January 13, 2022 at 10:56:59 AM UTC-5, Mostowski Collapse wrote:
> > Your Dedekind -> Peano proof doesn't work anymore.
> > Its the same problem like in this proof, where
> > this step doesn't work 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
> >
> Doesn't look like any of my proofs. Looks suspiciously wonky... Jan Burse. (Hee, hee!)
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, January 13, 2022 at 1:13:32 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 17:42:11 UTC+1:
> > On Thursday, January 13, 2022 at 10:56:59 AM UTC-5, Mostowski Collapse wrote:
> > > Your Dedekind -> Peano proof doesn't work anymore.
> > > Its the same problem like in this proof, where
> > > this step doesn't work 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
> > >
> > Doesn't look like any of my proofs. Looks suspiciously wonky... Jan Burse. (Hee, hee!)

> Not less wonky than DC Proof. Most dcproof2.exe proofs
> dont work anymore in dcproof5.exe?
>

So, it wasn't my proof. Whew! I'd hate to think I had posted something that wonky.

While it may be impossible to convert your more wonky proofs, Jan Burse, I am certain it is a simple matter to convert any of my proofs. See my reply just now to your posting here in another thread on this topic.

Dan

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

We are still waiting for your Dedekind - Peano proof.
Looks like you have taken the path of WM again,
he also claimed he found an inconsistency in

ZFC; but it was never published. Now you post
proofs that arent any proofs in dcproof5.exe,
welcome to the Kingdom of Cranks.

Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 20:05:05 UTC+1:
> On Thursday, January 13, 2022 at 1:13:32 PM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 17:42:11 UTC+1:
> > > On Thursday, January 13, 2022 at 10:56:59 AM UTC-5, Mostowski Collapse wrote:
> > > > Your Dedekind -> Peano proof doesn't work anymore.
> > > > Its the same problem like in this proof, where
> > > > this step doesn't work 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
> > > >
> > > Doesn't look like any of my proofs. Looks suspiciously wonky... Jan Burse. (Hee, hee!)
> > Not less wonky than DC Proof. Most dcproof2.exe proofs
> > dont work anymore in dcproof5.exe?
> >
> So, it wasn't my proof. Whew! I'd hate to think I had posted something that wonky.
>
> While it may be impossible to convert your more wonky proofs, Jan Burse, I am certain it is a simple matter to convert any of my proofs. See my reply just now to your posting here in another thread on this topic.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, January 13, 2022 at 2:24:01 PM UTC-5, Mostowski Collapse wrote:
> We are still waiting for your Dedekind - Peano proof.

Perhaps you missed it. Here it is again. http://www.dcproof.com/ProofByInduction.html (Only 247 lines. Enjoy.)

As did Zermelo and Fraenkel, I start by postulating the existence of an infinite set and derive Peano's Axioms from it. I think you find my development much more intuitive.

Dan

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

Fraenkel did nothing. The AOI is found in a paper by Zermelo.
Its an axiom of the form:

EXIST(S): ....

And then you can derive from it, where w is omega:

EXIST(w): ...

I don't see an axiom of this shape in your proof, neither
a conclusion of this shape in your proof. It only says:

ALL(f):[Dedekind(f) -> Peano(constr(f))].

But in DC Proof, we cannot anymore derive existence
from the above, see here:

Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 02:48:21 UTC+1:
> This is the proof that worked in dcproof2.exe, but
> does not work anymore in dcproof5.exe:
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/LGiS4I8UAwAJ

JUST REPLACE Peano by Dedekind, and Field by Peano.

You also called the above proof schema wonky,
since it wasn't invented by you. But it was a way
in the past to show Peano -> Dedekind, but as

of now it is open how to do it. We are still waiting...

Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 20:39:16 UTC+1:
> On Thursday, January 13, 2022 at 2:24:01 PM UTC-5, Mostowski Collapse wrote:
> > We are still waiting for your Dedekind - Peano proof.
> Perhaps you missed it. Here it is again. http://www.dcproof.com/ProofByInduction.html" rel="nofollow" target="_blank">http://www.dcproof.com/ProofByInduction.html (Only 247 lines. Enjoy.)
>
> As did Zermelo and Fraenkel, I start by postulating the existence of an infinite set and derive Peano's Axioms from it. I think you find my development much more intuitive.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Corr.: Wrong arrow direction:

JUST REPLACE Peano by Dedekind, and Field by Peano.

You also called the above proof schema wonky,
since it wasn't invented by you. But it was a way
in the past to show Dedekind -> Peano, but as

of now it is open how to do it. We are still waiting...

Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 21:26:49 UTC+1:
> Fraenkel did nothing. The AOI is found in a paper by Zermelo.
> Its an axiom of the form:
>
> EXIST(S): ....
>
> And then you can derive from it, where w is omega:
>
> EXIST(w): ...
>
> I don't see an axiom of this shape in your proof, neither
> a conclusion of this shape in your proof. It only says:
>
> ALL(f):[Dedekind(f) -> Peano(constr(f))].
>
> But in DC Proof, we cannot anymore derive existence
> from the above, see here:
> Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 02:48:21 UTC+1:
> > This is the proof that worked in dcproof2.exe, but
> > does not work anymore in dcproof5.exe:
> https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/LGiS4I8UAwAJ
>
> JUST REPLACE Peano by Dedekind, and Field by Peano.
>
> You also called the above proof schema wonky,
> since it wasn't invented by you. But it was a way
> in the past to show Peano -> Dedekind, but as
>
> of now it is open how to do it. We are still waiting...
> Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 20:39:16 UTC+1:
> > On Thursday, January 13, 2022 at 2:24:01 PM UTC-5, Mostowski Collapse wrote:
> > > We are still waiting for your Dedekind - Peano proof.
> > Perhaps you missed it. Here it is again. http://www.dcproof.com/ProofByInduction.html" rel="nofollow" target="_blank">http://www.dcproof.com/ProofByInduction.html (Only 247 lines. Enjoy.)
> >
> > As did Zermelo and Fraenkel, I start by postulating the existence of an infinite set and derive Peano's Axioms from it. I think you find my development much more intuitive.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

In FOL the schema works:

(∃fDf ∧ ∀f(Df → Pc(f))) → ∃nPn is valid.
https://www.umsu.de/trees/#~7fDf~1~6f%28Df~5Pc%28f%29%29~5~7nPn

But in dcproof5.exe the same proof that worked
in dcproof2.exe doesn't work anymore.

P.S.: The schema works also in my proof tool,
latest take from today allows entering quantified
formulas more easily, currently ASCII based:

?- prove0('?f D(f) & !f(D(f) => P(c(f))) => ?n P(n)', 2), !.
http://www.xlog.ch/izytab/moblet/en/docs/18_live/36_bim2022/paste17/package..html

I am working on a more comfy variant with Unicode,
so that proofs can be also posted here. The resulting
proof in the above variant is a Smullyan tree

rendered in MathJax, not suitable for copy paste.

Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 21:30:39 UTC+1:
> Corr.: Wrong arrow direction:
> JUST REPLACE Peano by Dedekind, and Field by Peano.
>
> You also called the above proof schema wonky,
> since it wasn't invented by you. But it was a way
> in the past to show Dedekind -> Peano, but as
> of now it is open how to do it. We are still waiting...
> Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 21:26:49 UTC+1:
> > Fraenkel did nothing. The AOI is found in a paper by Zermelo.
> > Its an axiom of the form:
> >
> > EXIST(S): ....
> >
> > And then you can derive from it, where w is omega:
> >
> > EXIST(w): ...
> >
> > I don't see an axiom of this shape in your proof, neither
> > a conclusion of this shape in your proof. It only says:
> >
> > ALL(f):[Dedekind(f) -> Peano(constr(f))].
> >
> > But in DC Proof, we cannot anymore derive existence
> > from the above, see here:
> > Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 02:48:21 UTC+1:
> > > This is the proof that worked in dcproof2.exe, but
> > > does not work anymore in dcproof5.exe:
> > https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/LGiS4I8UAwAJ
> >
> > JUST REPLACE Peano by Dedekind, and Field by Peano.
> >
> > You also called the above proof schema wonky,
> > since it wasn't invented by you. But it was a way
> > in the past to show Peano -> Dedekind, but as
> >
> > of now it is open how to do it. We are still waiting...
> > Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 20:39:16 UTC+1:
> > > On Thursday, January 13, 2022 at 2:24:01 PM UTC-5, Mostowski Collapse wrote:
> > > > We are still waiting for your Dedekind - Peano proof.
> > > Perhaps you missed it. Here it is again. http://www.dcproof.com/ProofByInduction.html" rel="nofollow" target="_blank">http://www.dcproof.com/ProofByInduction.html (Only 247 lines. Enjoy.)
> > >
> > > As did Zermelo and Fraenkel, I start by postulating the existence of an infinite set and derive Peano's Axioms from it. I think you find my development much more intuitive.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, January 13, 2022 at 3:26:49 PM UTC-5, Mostowski Collapse wrote:

> > Perhaps you missed it. Here it is again. http://www.dcproof.com/ProofByInduction.html (Only 247 lines. Enjoy.)
> >
> > As did Zermelo and Fraenkel, I start by postulating the existence of an infinite set and derive Peano's Axioms from it. I think you find my development much more intuitive.

> Fraenkel did nothing. The AOI is found in a paper by Zermelo.
> Its an axiom of the form:
>
> EXIST(S): ....
>
> And then you can derive from it, where w is omega:
>
> EXIST(w): ...
>
> I don't see an axiom of this shape in your proof

Perhaps you didn't know, but a Dedekind infinite set is one on which there exists an injective but not surjective function.

On line 1 postulate the existence of an injective function f: S --> S. On line 5, I postulate further that f is not surjective. So S is Dedekind infinite. On lines 12-106, I derive each of the Peano Axioms in turn.

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

You dont postulate existence, you state nowhere

EXIST(f): ....

You only prove:

ALL(f):[Dedekind(f) => Peano(c(f))]

If you use a constant in FOL, it is universally quantified.
If you use a constant in premisse, this is only universally
quantified, not existentially quantified.

Thats a trivial exercise to show that a proof:

A(c) |- B(c)

is only a proof:

|- ALL(x):[A(x) => B(x)]

Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 21:50:29 UTC+1:
> On Thursday, January 13, 2022 at 3:26:49 PM UTC-5, Mostowski Collapse wrote:
>
> > > Perhaps you missed it. Here it is again. http://www.dcproof.com/ProofByInduction.html" rel="nofollow" target="_blank">http://www.dcproof.com/ProofByInduction.html (Only 247 lines. Enjoy.)
> > >
> > > As did Zermelo and Fraenkel, I start by postulating the existence of an infinite set and derive Peano's Axioms from it. I think you find my development much more intuitive.
> > Fraenkel did nothing. The AOI is found in a paper by Zermelo.
> > Its an axiom of the form:
> >
> > EXIST(S): ....
> >
> > And then you can derive from it, where w is omega:
> >
> > EXIST(w): ...
> >
> > I don't see an axiom of this shape in your proof
> Perhaps you didn't know, but a Dedekind infinite set is one on which there exists an injective but not surjective function.
>
> On line 1 postulate the existence of an injective function f: S --> S. On line 5, I postulate further that f is not surjective. So S is Dedekind infinite. On lines 12-106, I derive each of the Peano Axioms in turn.
>
> 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

Just close your proof, even DC Proof will add ALL(f):

Mostowski Collapse schrieb am Donnerstag, 13. Januar 2022 um 21:57:16 UTC+1:
> You dont postulate existence, you state nowhere
>
> EXIST(f): ....
>
> You only prove:
>
> ALL(f):[Dedekind(f) => Peano(c(f))]
>
> If you use a constant in FOL, it is universally quantified.
> If you use a constant in premisse, this is only universally
> quantified, not existentially quantified.
>
> Thats a trivial exercise to show that a proof:
>
> A(c) |- B(c)
>
> is only a proof:
>
> |- ALL(x):[A(x) => B(x)]
> Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 21:50:29 UTC+1:
> > On Thursday, January 13, 2022 at 3:26:49 PM UTC-5, Mostowski Collapse wrote:
> >
> > > > Perhaps you missed it. Here it is again. http://www.dcproof.com/ProofByInduction.html" rel="nofollow" target="_blank">http://www.dcproof.com/ProofByInduction.html (Only 247 lines. Enjoy.)
> > > >
> > > > As did Zermelo and Fraenkel, I start by postulating the existence of an infinite set and derive Peano's Axioms from it. I think you find my development much more intuitive.
> > > Fraenkel did nothing. The AOI is found in a paper by Zermelo.
> > > Its an axiom of the form:
> > >
> > > EXIST(S): ....
> > >
> > > And then you can derive from it, where w is omega:
> > >
> > > EXIST(w): ...
> > >
> > > I don't see an axiom of this shape in your proof
> > Perhaps you didn't know, but a Dedekind infinite set is one on which there exists an injective but not surjective function.
> >
> > On line 1 postulate the existence of an injective function f: S --> S. On line 5, I postulate further that f is not surjective. So S is Dedekind infinite. On lines 12-106, I derive each of the Peano Axioms in turn.
> >
> > 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

On Thursday, January 13, 2022 at 3:57:16 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 21:50:29 UTC+1:
> > On Thursday, January 13, 2022 at 3:26:49 PM UTC-5, Mostowski Collapse wrote:
> >
> > > > Perhaps you missed it. Here it is again. http://www.dcproof.com/ProofByInduction.html (Only 247 lines. Enjoy.)
> > > >
> > > > As did Zermelo and Fraenkel, I start by postulating the existence of an infinite set and derive Peano's Axioms from it. I think you find my development much more intuitive.
> > > Fraenkel did nothing. The AOI is found in a paper by Zermelo.
> > > Its an axiom of the form:
> > >
> > > EXIST(S): ....
> > >
> > > And then you can derive from it, where w is omega:
> > >
> > > EXIST(w): ...
> > >
> > > I don't see an axiom of this shape in your proof
> > Perhaps you didn't know, but a Dedekind infinite set is one on which there exists an injective but not surjective function.
> >
> > On line 1 postulate the existence of an injective function f: S --> S. On line 5, I postulate further that f is not surjective. So S is Dedekind infinite. On lines 12-106, I derive each of the Peano Axioms in turn.
> >
> > I hope this helps.

> You dont postulate existence, you state nowhere
>
> EXIST(f): ....
>
> You only prove:
>
> ALL(f):[Dedekind(f) => Peano(c(f))]
>

It amounts to the same thing. More straightforward,

BTW I found a more recent, shorter version. It proves:

ALL(x):ALL(f):[Set(x)
& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]

=> EXIST(n):EXIST(x0):[Set(n) & ALL(a):[a in n => a in x] & x0 in n
& ALL(a):[a in n => f(a) in n]
& ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
& ALL(a):[a in n => ~f(a)=x0]
& ALL(a):[Set(a)
& ALL(b):[b in a => b in n]
=> [x0 in a & ALL(b):[b in a => f(b) in a]
=> ALL(b):[b in n => b in a]]]]]

https://dcproof.com/ConstructN.htm (only 104 lines)

> If you use a constant in FOL, it is universally quantified.

Not a problem.

> If you use a constant in premisse, this is only universally
> quantified, not existentially quantified.
>

Doesn't matter.

> Thats a trivial exercise to show that a proof:
>
> A(c) |- B(c)
>
> is only a proof:
>
> |- ALL(x):[A(x) => B(x)]

As required. What's your problem, Jan Burse?

Dan

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

Whats wrong with you, one more fallacy by Dan-O-Matik:

∀f(Df → ∃nPfn) → ∃f∃n(Df ∧ Pfn) is invalid.
Countermodel:
Domain: { 0 }
D: { }
P: { (0,0) }

Some quantifier dislexia on your side?

P.S.: You need more assumption, for example this works:

(∃fDf ∧ ∀f(Df → ∃nPfn)) → ∃f∃n(Df ∧ Pfn) is valid.
https://www.umsu.de/trees/#~7fDf~1~6f%28Df~5~7nPfn%29~5~7f~7n%28Df~1Pfn%29

Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 22:42:41 UTC+1:
> On Thursday, January 13, 2022 at 3:57:16 PM UTC-5, Mostowski Collapse wrote:
>
>
> > Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 21:50:29 UTC+1:
> > > On Thursday, January 13, 2022 at 3:26:49 PM UTC-5, Mostowski Collapse wrote:
> > >
> > > > > Perhaps you missed it. Here it is again. http://www.dcproof.com/ProofByInduction.html" rel="nofollow" target="_blank">http://www.dcproof.com/ProofByInduction.html (Only 247 lines. Enjoy.)
> > > > >
> > > > > As did Zermelo and Fraenkel, I start by postulating the existence of an infinite set and derive Peano's Axioms from it. I think you find my development much more intuitive.
> > > > Fraenkel did nothing. The AOI is found in a paper by Zermelo.
> > > > Its an axiom of the form:
> > > >
> > > > EXIST(S): ....
> > > >
> > > > And then you can derive from it, where w is omega:
> > > >
> > > > EXIST(w): ...
> > > >
> > > > I don't see an axiom of this shape in your proof
> > > Perhaps you didn't know, but a Dedekind infinite set is one on which there exists an injective but not surjective function.
> > >
> > > On line 1 postulate the existence of an injective function f: S --> S.. On line 5, I postulate further that f is not surjective. So S is Dedekind infinite. On lines 12-106, I derive each of the Peano Axioms in turn.
> > >
> > > I hope this helps.
> > You dont postulate existence, you state nowhere
> >
> > EXIST(f): ....
> >
> > You only prove:
> >
> > ALL(f):[Dedekind(f) => Peano(c(f))]
> >
> It amounts to the same thing. More straightforward,
>
> BTW I found a more recent, shorter version. It proves:
>
> ALL(x):ALL(f):[Set(x)
> & ALL(a):[a in x => f(a) in x]
> & ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
> & EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
>
> => EXIST(n):EXIST(x0):[Set(n) & ALL(a):[a in n => a in x] & x0 in n
> & ALL(a):[a in n => f(a) in n]
> & ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
> & ALL(a):[a in n => ~f(a)=x0]
> & ALL(a):[Set(a)
> & ALL(b):[b in a => b in n]
> => [x0 in a & ALL(b):[b in a => f(b) in a]
> => ALL(b):[b in n => b in a]]]]]
>
> https://dcproof.com/ConstructN.htm (only 104 lines)
> > If you use a constant in FOL, it is universally quantified.
> Not a problem.
> > If you use a constant in premisse, this is only universally
> > quantified, not existentially quantified.
> >
> Doesn't matter.
> > Thats a trivial exercise to show that a proof:
> >
> > A(c) |- B(c)
> >
> > is only a proof:
> >
> > |- ALL(x):[A(x) => B(x)]
> As required. What's your problem, Jan Burse?
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Also you run sooner or later into the power set
axiom, if you stick to your new U Spec axiom.
If you prove uniqueness as well, then you have:

∀f(Df → ∃!nPfn)

So n is a function of f, the Dedekind function, i.e.
Df. And you have Peano for f and n, as follows,
by some construction, the function c:

∀f(Df → Pfc(f))

The fallacy is the same:

∀f(Df → Pfc(f)) → ∃f(Df ∧ Pfc(f)) is invalid.
Countermodel:
Domain: { 0 }
c: { (0,0) }
D: { }
P: { (0,0) }

The cure is the same:

(∃fDf ∧ ∀f(Df → Pfc(f))) → ∃f(Df ∧ Pfc(f)) is valid.

But can you prove this cure? You need c(f) e S
for your modified U Spec rule. But the constructed
set n, is subset of s. So basically S is the power set

Pow(s), and n e Pow(s). So you could apply your
modified U Spec axiom, if you had the axiom of power set.

Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 00:27:27 UTC+1:
> Whats wrong with you, one more fallacy by Dan-O-Matik:
>
> ∀f(Df → ∃nPfn) → ∃f∃n(Df ∧ Pfn) is invalid.
> Countermodel:
> Domain: { 0 }
> D: { }
> P: { (0,0) }
>
> Some quantifier dislexia on your side?
>
> P.S.: You need more assumption, for example this works:
>
> (∃fDf ∧ ∀f(Df → ∃nPfn)) → ∃f∃n(Df ∧ Pfn) is valid.
> https://www.umsu.de/trees/#~7fDf~1~6f%28Df~5~7nPfn%29~5~7f~7n%28Df~1Pfn%29
> Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 22:42:41 UTC+1:
> > On Thursday, January 13, 2022 at 3:57:16 PM UTC-5, Mostowski Collapse wrote:
> >
> >
> > > Dan Christensen schrieb am Donnerstag, 13. Januar 2022 um 21:50:29 UTC+1:
> > > > On Thursday, January 13, 2022 at 3:26:49 PM UTC-5, Mostowski Collapse wrote:
> > > >
> > > > > > Perhaps you missed it. Here it is again. http://www.dcproof.com/ProofByInduction.html" rel="nofollow" target="_blank">http://www.dcproof.com/ProofByInduction.html (Only 247 lines. Enjoy.)
> > > > > >
> > > > > > As did Zermelo and Fraenkel, I start by postulating the existence of an infinite set and derive Peano's Axioms from it. I think you find my development much more intuitive.
> > > > > Fraenkel did nothing. The AOI is found in a paper by Zermelo.
> > > > > Its an axiom of the form:
> > > > >
> > > > > EXIST(S): ....
> > > > >
> > > > > And then you can derive from it, where w is omega:
> > > > >
> > > > > EXIST(w): ...
> > > > >
> > > > > I don't see an axiom of this shape in your proof
> > > > Perhaps you didn't know, but a Dedekind infinite set is one on which there exists an injective but not surjective function.
> > > >
> > > > On line 1 postulate the existence of an injective function f: S --> S. On line 5, I postulate further that f is not surjective. So S is Dedekind infinite. On lines 12-106, I derive each of the Peano Axioms in turn.
> > > >
> > > > I hope this helps.
> > > You dont postulate existence, you state nowhere
> > >
> > > EXIST(f): ....
> > >
> > > You only prove:
> > >
> > > ALL(f):[Dedekind(f) => Peano(c(f))]
> > >
> > It amounts to the same thing. More straightforward,
> >
> > BTW I found a more recent, shorter version. It proves:
> >
> > ALL(x):ALL(f):[Set(x)
> > & ALL(a):[a in x => f(a) in x]
> > & ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
> > & EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
> >
> > => EXIST(n):EXIST(x0):[Set(n) & ALL(a):[a in n => a in x] & x0 in n
> > & ALL(a):[a in n => f(a) in n]
> > & ALL(a):ALL(b):[a in n & b in n => [f(a)=f(b) => a=b]]
> > & ALL(a):[a in n => ~f(a)=x0]
> > & ALL(a):[Set(a)
> > & ALL(b):[b in a => b in n]
> > => [x0 in a & ALL(b):[b in a => f(b) in a]
> > => ALL(b):[b in n => b in a]]]]]
> >
> > https://dcproof.com/ConstructN.htm (only 104 lines)
> > > If you use a constant in FOL, it is universally quantified.
> > Not a problem.
> > > If you use a constant in premisse, this is only universally
> > > quantified, not existentially quantified.
> > >
> > Doesn't matter.
> > > Thats a trivial exercise to show that a proof:
> > >
> > > A(c) |- B(c)
> > >
> > > is only a proof:
> > >
> > > |- ALL(x):[A(x) => B(x)]
> > As required. What's your problem, Jan Burse?
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

To prove what is required, and what Zermelo did
already in his 1908 paper, namely to go from some

EXIST(s)...

To some exist w, where w is omega:

EXIST(w)...

You possibly need the power set axiom in the case
of DC Proof and the modified U Spec rule. Because
you work with a Dedekind function f on some set s,

and the Peano structure has some set n, and guess
what the relationship between s and n is? Maybe
you dont prove it, but you have:

n ⊆ s

But this is the same statement as:

n ∈ Pow(s)

So the constuction of n from f, i.e. c(f), can be
bounded by a set S so that c(f) e S, when you
take S = Pow(s). But you don't have a power set

axiom in DC Proof. So you cannot show existence
of the Peano structure self standingly. You can only
prove this here:

ALL(f):[ => EXIST(n) ...]

But you cannot prove:

EXIST(f):EXIST(n):[ .... ]

Also not when you have EXIST(f):.. assumed. Since
your new U Spec inference rule makes things more
complicated and since you don't have power set axiom.

Maybe you can prove it?

Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 00:35:46 UTC+1:
> Also you run sooner or later into the power set
> axiom, if you stick to your new U Spec axiom.
> If you prove uniqueness as well, then you have:
>
> ∀f(Df → ∃!nPfn)
>
> So n is a function of f, the Dedekind function, i.e.
> Df. And you have Peano for f and n, as follows,
> by some construction, the function c:
>
> ∀f(Df → Pfc(f))
>
> The fallacy is the same:
>
> ∀f(Df → Pfc(f)) → ∃f(Df ∧ Pfc(f)) is invalid.
> Countermodel:
> Domain: { 0 }
> c: { (0,0) }
> D: { }
> P: { (0,0) }
>
> The cure is the same:
>
> (∃fDf ∧ ∀f(Df → Pfc(f))) → ∃f(Df ∧ Pfc(f)) is valid.
>
> But can you prove this cure? You need c(f) e S
> for your modified U Spec rule. But the constructed
> set n, is subset of s. So basically S is the power set
>
> Pow(s), and n e Pow(s). So you could apply your
> modified U Spec axiom, if you had the axiom of power set.
> Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 00:27:27 UTC+1:

The problem are these two quantifiers:

ALL(x):ALL(f):[Set(x)
& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
.... bla bla ...

ALL(x) and ALL(f) just dont give existence.
They can be vacously true in a model.

Instead of requiring a theorem with EXIST(f)
and EXIST(x), we could maybe permit an ALL(f)
and require an EXIST(x)).

This is a little more in the spirit of Zermelo, since
Zermelo does not have EXIST(∈) where ∈ is the
element of relation ship. But he uses ∈ to construct

the successor. Can you prove in DC Proof
that n exist when x exists? Something like:

ALL(f):[EXIST(x):Set(x)
& ALL(a):[a in x => f(a) in x]
& ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
& EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]]
.... bla bla ...

x is only used in the conclusion
ALL(a):[a in n => a in x] ,
you wouldn't need x in the conclusion

if you had f correctly modelled, you could replace
x by dom(f) or so. But if the conclusion with
ALL(a):[a in n => a in x] is valid, you can also prove
the conclusion without ALL(a):[a in n => a in x] .

Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 00:42:35 UTC+1:
> To prove what is required, and what Zermelo did
> already in his 1908 paper, namely to go from some
>
> EXIST(s)...
>
> To some exist w, where w is omega:
>
> EXIST(w)...
>
> You possibly need the power set axiom in the case
> of DC Proof and the modified U Spec rule. Because
> you work with a Dedekind function f on some set s,
>
> and the Peano structure has some set n, and guess
> what the relationship between s and n is? Maybe
> you dont prove it, but you have:
>
> n ⊆ s
>
> But this is the same statement as:
>
> n ∈ Pow(s)
>
> So the constuction of n from f, i.e. c(f), can be
> bounded by a set S so that c(f) e S, when you
> take S = Pow(s). But you don't have a power set
>
> axiom in DC Proof. So you cannot show existence
> of the Peano structure self standingly. You can only
> prove this here:
>
> ALL(f):[ => EXIST(n) ...]
>
> But you cannot prove:
>
> EXIST(f):EXIST(n):[ .... ]
>
> Also not when you have EXIST(f):.. assumed. Since
> your new U Spec inference rule makes things more
> complicated and since you don't have power set axiom.
>
> Maybe you can prove it?
> Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 00:35:46 UTC+1:
> > Also you run sooner or later into the power set
> > axiom, if you stick to your new U Spec axiom.
> > If you prove uniqueness as well, then you have:
> >
> > ∀f(Df → ∃!nPfn)
> >
> > So n is a function of f, the Dedekind function, i.e.
> > Df. And you have Peano for f and n, as follows,
> > by some construction, the function c:
> >
> > ∀f(Df → Pfc(f))
> >
> > The fallacy is the same:
> >
> > ∀f(Df → Pfc(f)) → ∃f(Df ∧ Pfc(f)) is invalid.
> > Countermodel:
> > Domain: { 0 }
> > c: { (0,0) }
> > D: { }
> > P: { (0,0) }
> >
> > The cure is the same:
> >
> > (∃fDf ∧ ∀f(Df → Pfc(f))) → ∃f(Df ∧ Pfc(f)) is valid.
> >
> > But can you prove this cure? You need c(f) e S
> > for your modified U Spec rule. But the constructed
> > set n, is subset of s. So basically S is the power set
> >
> > Pow(s), and n e Pow(s). So you could apply your
> > modified U Spec axiom, if you had the axiom of power set.
> > Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 00:27:27 UTC+1:

On Thursday, January 13, 2022 at 6:54:38 PM UTC-5, Mostowski Collapse wrote:
> The problem are these two quantifiers:
> ALL(x):ALL(f):[Set(x)
> & ALL(a):[a in x => f(a) in x]
> & ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
> & EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]

No problem with that. It just says, for all Dedekind infinite sets, et.c

> ... bla bla ...
>
> ALL(x) and ALL(f) just dont give existence.
> They can be vacously true in a model.
>

So, all sets are finite??? Now you are sounding WM!

Dan

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

On Thursday, January 13, 2022 at 6:54:38 PM UTC-5, Mostowski Collapse wrote:
> The problem are these two quantifiers:
> ALL(x):ALL(f):[Set(x)
> & ALL(a):[a in x => f(a) in x]
> & ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
> & EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]

No problem with that. It just says, for all Dedekind infinite sets, etc.

> ... bla bla ...
>
> ALL(x) and ALL(f) just dont give existence.
> They can be vacously true in a model.
>

So, all sets are finite??? Now you are sounding like WM!

Dan

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

Did you make you proof with the help of a pendulum
or what. Did you also find some water? LoL

Here is a simple proof, assume it ends with,
two alternatives 1) or 2) for demonstration:

1) ALL(x):[egg(x) => hatch(x,chicken(x))]
2) ALL(x):[egg(x) => EXIST(y):hatch(x,y)]

Can you now prove? No, none is provable:

1) => 3) EXIST(x):[egg(x) & hatch(x,chicken(x))]
2) => 4) EXIST(x):[egg(x) & EXIST(y):hatch(x,y)]

You didn't show that a Peano chicken exists.
We don't know whether there are some Dedekind eggs.

On the other hand Zermelo did it correctly.

Got it Bozo?

Dan Christensen schrieb am Freitag, 14. Januar 2022 um 01:08:10 UTC+1:
> On Thursday, January 13, 2022 at 6:54:38 PM UTC-5, Mostowski Collapse wrote:
> > The problem are these two quantifiers:
> > ALL(x):ALL(f):[Set(x)
> > & ALL(a):[a in x => f(a) in x]
> > & ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
> > & EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
> No problem with that. It just says, for all Dedekind infinite sets, etc.
> > ... bla bla ...
> >
> > ALL(x) and ALL(f) just dont give existence.
> > They can be vacously true in a model.
> >
> So, all sets are finite??? Now you are sounding like WM!
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, January 13, 2022 at 7:41:42 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Freitag, 14. Januar 2022 um 01:08:10 UTC+1:
> > On Thursday, January 13, 2022 at 6:54:38 PM UTC-5, Mostowski Collapse wrote:
> > > The problem are these two quantifiers:
> > > ALL(x):ALL(f):[Set(x)
> > > & ALL(a):[a in x => f(a) in x]
> > > & ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
> > > & EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
> > No problem with that. It just says, for all Dedekind infinite sets, etc.
> > > ... bla bla ...
> > >
> > > ALL(x) and ALL(f) just dont give existence.
> > > They can be vacously true in a model.
> > >
> > So, all sets are finite??? Now you are sounding like WM!

> Did you make you proof with the help of a pendulum
> or what. Did you also find some water? LoL
>
> Here is a simple proof, assume it ends with,
> two alternatives 1) or 2) for demonstration:
>
> 1) ALL(x):[egg(x) => hatch(x,chicken(x))]
> 2) ALL(x):[egg(x) => EXIST(y):hatch(x,y)]
>
> Can you now prove? No, none is provable:
>
> 1) => 3) EXIST(x):[egg(x) & hatch(x,chicken(x))]
> 2) => 4) EXIST(x):[egg(x) & EXIST(y):hatch(x,y)]
>

Nonsense!

> You didn't show that a Peano chicken exists.
> We don't know whether there are some Dedekind eggs.
>
> On the other hand Zermelo did it correctly.
>

He just assumed there existed an infinite set. As I did in my proof. Great minds...

Dan

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

Students beware of fake DC Proof. There is one more
problem with DC Proof, and its not my fault.
Dan-O-Matik himself started comparing his Peano

nonsense with set theory, and in particular with
Zermelos axiom of infinity, which states the existence
of an inductive set. So what is a further "bug" in

Dan-O-Matiks comparison? Zermelo proves more!
Zermelo proves global derived existence of omega, wheras
Dan-O-Matik only shows local derived existence of a Peano

structure. See yourself:

Dan-O-Matik, only derived local existence:
ALL(f):[Dedekind(f) => EXIST(n):Peano(f,n)]

Zermelo, derived global existence:
EXIST(w):ALL(s):[Inductive(s) => Omega(s,w)]

But Zermelo must also add EXIST(s):Inductive(s),
because without it, deriving existence
doesn't work out directly from his theorem:

∃w∀s(Is → Osw) → ∃s∃wOsw is invalid.
Countermodel:
Domain: { 0 }
I: { }
O: { }
https://www.umsu.de/trees/#~7w~6s%28Is~5Osw%29~5~7s~7wOsw

Would be similar fallacy. Similar cure though:

(∃sIs ∧ ∃w∀s(Is → Osw)) → ∃s∃wOsw is valid.
https://www.umsu.de/trees/#~7sIs~1~7w~6s%28Is~5Osw%29~5~7s~7wOsw

Dan Christensen schrieb am Freitag, 14. Januar 2022 um 03:22:37 UTC+1:
> On Thursday, January 13, 2022 at 7:41:42 PM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Freitag, 14. Januar 2022 um 01:08:10 UTC+1:
> > > On Thursday, January 13, 2022 at 6:54:38 PM UTC-5, Mostowski Collapse wrote:
> > > > The problem are these two quantifiers:
> > > > ALL(x):ALL(f):[Set(x)
> > > > & ALL(a):[a in x => f(a) in x]
> > > > & ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
> > > > & EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
> > > No problem with that. It just says, for all Dedekind infinite sets, etc.
> > > > ... bla bla ...
> > > >
> > > > ALL(x) and ALL(f) just dont give existence.
> > > > They can be vacously true in a model.
> > > >
> > > So, all sets are finite??? Now you are sounding like WM!
> > Did you make you proof with the help of a pendulum
> > or what. Did you also find some water? LoL
> >
> > Here is a simple proof, assume it ends with,
> > two alternatives 1) or 2) for demonstration:
> >
> > 1) ALL(x):[egg(x) => hatch(x,chicken(x))]
> > 2) ALL(x):[egg(x) => EXIST(y):hatch(x,y)]
> >
> > Can you now prove? No, none is provable:
> >
> > 1) => 3) EXIST(x):[egg(x) & hatch(x,chicken(x))]
> > 2) => 4) EXIST(x):[egg(x) & EXIST(y):hatch(x,y)]
> >
> Nonsense!
> > You didn't show that a Peano chicken exists.
> > We don't know whether there are some Dedekind eggs.
> >
> > On the other hand Zermelo did it correctly.
> >
> He just assumed there existed an infinite set. As I did in my proof. Great minds...
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

We can also show uniqueness, replacing ∃w by ∃!w.
And the parameter s can be eliminated in the definition
of omega, so we can prove in Zermelo:

∃!wOmega(w)

On the other hand in Dan-O-Matik, inside one domain
of discourse, there are many many Peano structures,
for each function f with Dedekind(f) there is a

Peano(f,n). Sometimes if we have f1 and f2, turns
out that the Peano structurs are the same, but there
are also f1 and f2 where the Peano structure is

not the same. Thats quite "unnatural" to have many
different "natural" numbers inside a domain of discourse.
Usually when we talk of natural numbers, such as

1, 2, 3, etc.. we don't assume that suddently there
are further natural numbers 1', 2', 3', etc.. generated
from an other Dedekind function. And so on.

What are Dan-O-Matiks numbers, potato numbers?

Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 09:50:43 UTC+1:
> Students beware of fake DC Proof. There is one more
> problem with DC Proof, and its not my fault.
> Dan-O-Matik himself started comparing his Peano
>
> nonsense with set theory, and in particular with
> Zermelos axiom of infinity, which states the existence
> of an inductive set. So what is a further "bug" in
>
> Dan-O-Matiks comparison? Zermelo proves more!
> Zermelo proves global derived existence of omega, wheras
> Dan-O-Matik only shows local derived existence of a Peano
>
> structure. See yourself:
>
> Dan-O-Matik, only derived local existence:
> ALL(f):[Dedekind(f) => EXIST(n):Peano(f,n)]
>
> Zermelo, derived global existence:
> EXIST(w):ALL(s):[Inductive(s) => Omega(s,w)]
>
> But Zermelo must also add EXIST(s):Inductive(s),
> because without it, deriving existence
> doesn't work out directly from his theorem:
>
> ∃w∀s(Is → Osw) → ∃s∃wOsw is invalid.
> Countermodel:
> Domain: { 0 }
> I: { }
> O: { }
> https://www.umsu.de/trees/#~7w~6s%28Is~5Osw%29~5~7s~7wOsw
>
> Would be similar fallacy. Similar cure though:
>
> (∃sIs ∧ ∃w∀s(Is → Osw)) → ∃s∃wOsw is valid.
> https://www.umsu.de/trees/#~7sIs~1~7w~6s%28Is~5Osw%29~5~7s~7wOsw
> Dan Christensen schrieb am Freitag, 14. Januar 2022 um 03:22:37 UTC+1:
> > On Thursday, January 13, 2022 at 7:41:42 PM UTC-5, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Freitag, 14. Januar 2022 um 01:08:10 UTC+1:
> > > > On Thursday, January 13, 2022 at 6:54:38 PM UTC-5, Mostowski Collapse wrote:
> > > > > The problem are these two quantifiers:
> > > > > ALL(x):ALL(f):[Set(x)
> > > > > & ALL(a):[a in x => f(a) in x]
> > > > > & ALL(a):ALL(b):[a in x & b in x => [f(a)=f(b) => a=b]]
> > > > > & EXIST(a):[a in x & ALL(b):[b in x => ~f(b)=a]]
> > > > No problem with that. It just says, for all Dedekind infinite sets, etc.
> > > > > ... bla bla ...
> > > > >
> > > > > ALL(x) and ALL(f) just dont give existence.
> > > > > They can be vacously true in a model.
> > > > >
> > > > So, all sets are finite??? Now you are sounding like WM!
> > > Did you make you proof with the help of a pendulum
> > > or what. Did you also find some water? LoL
> > >
> > > Here is a simple proof, assume it ends with,
> > > two alternatives 1) or 2) for demonstration:
> > >
> > > 1) ALL(x):[egg(x) => hatch(x,chicken(x))]
> > > 2) ALL(x):[egg(x) => EXIST(y):hatch(x,y)]
> > >
> > > Can you now prove? No, none is provable:
> > >
> > > 1) => 3) EXIST(x):[egg(x) & hatch(x,chicken(x))]
> > > 2) => 4) EXIST(x):[egg(x) & EXIST(y):hatch(x,y)]
> > >
> > Nonsense!
> > > You didn't show that a Peano chicken exists.
> > > We don't know whether there are some Dedekind eggs.
> > >
> > > On the other hand Zermelo did it correctly.
> > >
> > He just assumed there existed an infinite set. As I did in my proof. Great minds...
> > 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, January 14, 2022 at 4:02:32 AM UTC-5, Mostowski Collapse wrote:
> We can also show uniqueness, replacing ∃w by ∃!w.
> And the parameter s can be eliminated in the definition
> of omega, so we can prove in Zermelo:
>
> ∃!wOmega(w)
>
> On the other hand in Dan-O-Matik, inside one domain
> of discourse, there are many many Peano structures,
> for each function f with Dedekind(f) there is a
>
> Peano(f,n).

I have shown that in every Dedekind infinite set, there exists at least one Peano structure. So, there really is something "natural" about Peano's Axioms, the axiom of induction in particular. IMHO this should go a long way to justifying Peano's Axioms if one is at all skeptical of them. To further justify induction, I have shown elsewhere that induction can even hold on finite sets, e.g. on {0, 1} if S(0)=1 and S(1)=0. All quite "natural."

I have not included an axiom of infinity in DC Proof. Instead, I suggest users simply start proofs with a statement of Peano's Axioms as may be required in a proof. IMHO they are much more intuitive and self-evident than the ZFC Axiom of Infinity, a pedagogical nightmare.

Dan

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

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?

Dan Christensen schrieb am Freitag, 14. Januar 2022 um 17:43:02 UTC+1:
> On Friday, January 14, 2022 at 4:02:32 AM UTC-5, Mostowski Collapse wrote:
> > We can also show uniqueness, replacing ∃w by ∃!w.
> > And the parameter s can be eliminated in the definition
> > of omega, so we can prove in Zermelo:
> >
> > ∃!wOmega(w)
> >
> > On the other hand in Dan-O-Matik, inside one domain
> > of discourse, there are many many Peano structures,
> > for each function f with Dedekind(f) there is a
> >
> > Peano(f,n).
> I have shown that in every Dedekind infinite set, there exists at least one Peano structure. So, there really is something "natural" about Peano's Axioms, the axiom of induction in particular. IMHO this should go a long way to justifying Peano's Axioms if one is at all skeptical of them. To further justify induction, I have shown elsewhere that induction can even hold on finite sets, e.g. on {0, 1} if S(0)=1 and S(1)=0. All quite "natural."
>
> I have not included an axiom of infinity in DC Proof. Instead, I suggest users simply start proofs with a statement of Peano's Axioms as may be required in a proof. IMHO they are much more intuitive and self-evident than the ZFC Axiom of Infinity, a pedagogical nightmare.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

So you call your paranoid prime enemy a nightmare, whereas
in fact DC proof hasn't spent more time than taking a shit
in the morning over many problems of numerosity and ordering.

The next step in set theory is then to define cardinality
as the smallest ordinal in bijection, which then gives also
canonical representatives for cardinality.

Cardinality ordinals and ordinals are the same in the finite
case, and for the first infinite ordinal omega.

Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:04:25 UTC+1:
> 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?
> Dan Christensen schrieb am Freitag, 14. Januar 2022 um 17:43:02 UTC+1:
> > On Friday, January 14, 2022 at 4:02:32 AM UTC-5, Mostowski Collapse wrote:
> > > We can also show uniqueness, replacing ∃w by ∃!w.
> > > And the parameter s can be eliminated in the definition
> > > of omega, so we can prove in Zermelo:
> > >
> > > ∃!wOmega(w)
> > >
> > > On the other hand in Dan-O-Matik, inside one domain
> > > of discourse, there are many many Peano structures,
> > > for each function f with Dedekind(f) there is a
> > >
> > > Peano(f,n).
> > I have shown that in every Dedekind infinite set, there exists at least one Peano structure. So, there really is something "natural" about Peano's Axioms, the axiom of induction in particular. IMHO this should go a long way to justifying Peano's Axioms if one is at all skeptical of them. To further justify induction, I have shown elsewhere that induction can even hold on finite sets, e.g. on {0, 1} if S(0)=1 and S(1)=0. All quite "natural.."
> >
> > I have not included an axiom of infinity in DC Proof. Instead, I suggest users simply start proofs with a statement of Peano's Axioms as may be required in a proof. IMHO they are much more intuitive and self-evident than the ZFC Axiom of Infinity, a pedagogical nightmare.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Von Neumann ordinals arise naturally as an answer to the
classification problem asking to classify well-orders on sets.
In "naive set theory" we might typically say something along
the lines of: given two well-ordered sets (𝐴,<𝐴) and (𝐵,<𝐵),
we will say they are equivalent if there is an order-preserving
isomorphism between 𝐴 and 𝐵. Then, an "ordinal" will be
defined as an "equivalence class" of this equivalence relation.

In axiomatic set theory, however, we run into the problem
that the relation described above is "too big" to be an actual
object of ZFC, and so is any individual "equivalence class".
However, what we can find is that each "equivalence class"
has a canonical representative given by the

* 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 (𝐴,𝑅)≃(𝐵,∈|𝐵×𝐵).

By restricting to well-orders, we see that each "equivalence class" of
well-orders has a unique representative of this type, which is a
transitive set 𝑋 such that ∈|𝑋×𝑋 is a well-order on 𝑋. This is precisely
the definition of von Neumann ordinals.
https://math.stackexchange.com/a/2976857/1002973

Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:08:08 UTC+1:
> So you call your paranoid prime enemy a nightmare, whereas
> in fact DC proof hasn't spent more time than taking a shit
> in the morning over many problems of numerosity and ordering.
>
> The next step in set theory is then to define cardinality
> as the smallest ordinal in bijection, which then gives also
> canonical representatives for cardinality.
>
> Cardinality ordinals and ordinals are the same in the finite
> case, and for the first infinite ordinal omega.
> Mostowski Collapse schrieb am Freitag, 14. Januar 2022 um 18:04:25 UTC+1:
> > 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?
> > Dan Christensen schrieb am Freitag, 14. Januar 2022 um 17:43:02 UTC+1:
> > > On Friday, January 14, 2022 at 4:02:32 AM UTC-5, Mostowski Collapse wrote:
> > > > We can also show uniqueness, replacing ∃w by ∃!w.
> > > > And the parameter s can be eliminated in the definition
> > > > of omega, so we can prove in Zermelo:
> > > >
> > > > ∃!wOmega(w)
> > > >
> > > > On the other hand in Dan-O-Matik, inside one domain
> > > > of discourse, there are many many Peano structures,
> > > > for each function f with Dedekind(f) there is a
> > > >
> > > > Peano(f,n).
> > > I have shown that in every Dedekind infinite set, there exists at least one Peano structure. So, there really is something "natural" about Peano's Axioms, the axiom of induction in particular. IMHO this should go a long way to justifying Peano's Axioms if one is at all skeptical of them. To further justify induction, I have shown elsewhere that induction can even hold on finite sets, e.g. on {0, 1} if S(0)=1 and S(1)=0. All quite "natural."
> > >
> > > I have not included an axiom of infinity in DC Proof. Instead, I suggest users simply start proofs with a statement of Peano's Axioms as may be required in a proof. IMHO they are much more intuitive and self-evident than the ZFC Axiom of Infinity, a pedagogical nightmare.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com