I did not claim (Q, succQ, 0) satisfies the Peano axioms,
in the sense that N would be replaced by Q.

Thats your idee fix. Sorry I cannot help you.

Dan Christensen schrieb am Samstag, 7. Mai 2022 um 17:15:38 UTC+2:
> On Saturday, May 7, 2022 at 5:23:13 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> > I have of course succQ(-1)=0. But I have also ~(-1 e N).
> Of course (N, S, 0) satisfies PA, where S is the usual successor function on N. Sadly for you, and contrary to your outrageous claim, (Q, succQ, 0) where succQ(x)=x+1 on Q, does NOT satisfy PA since succQ(-1)=0. When will you learn, 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

Maybe see a doctor, it seems you have some reading
disability or some other mental health problem.

Mostowski Collapse schrieb am Samstag, 7. Mai 2022 um 17:36:29 UTC+2:
> I did not claim (Q, succQ, 0) satisfies the Peano axioms,
> in the sense that N would be replaced by Q.
>
> Thats your idee fix. Sorry I cannot help you.
> Dan Christensen schrieb am Samstag, 7. Mai 2022 um 17:15:38 UTC+2:
> > On Saturday, May 7, 2022 at 5:23:13 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> > > I have of course succQ(-1)=0. But I have also ~(-1 e N).
> > Of course (N, S, 0) satisfies PA, where S is the usual successor function on N. Sadly for you, and contrary to your outrageous claim, (Q, succQ, 0) where succQ(x)=x+1 on Q, does NOT satisfy PA since succQ(-1)=0. When will you learn, 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

Mostowski Collapse wrote:

> I did not claim (Q, succQ, 0) satisfies the Peano axioms,
> in the sense that N would be replaced by Q.
>
> Thats your idee fix. Sorry I cannot help you.
>
> Dan Christensen schrieb am Samstag, 7. Mai 2022 um 17:15:38 UTC+2:

You two lovers should go to kievj and kiss the ring of the nazi home
zelenskej, like everybody else. Big governments kissed the ring of
zelenske, why not you??

https://cdni.russiatoday.com/files/2022.05/l/62753b4085f54049e92af89d.jpg

On Saturday, May 7, 2022 at 2:20:47 PM UTC-4, Mitch Yamaguchi wrote:
> Mostowski Collapse wrote:
>
> > I did not claim (Q, succQ, 0) satisfies the Peano axioms,
> > in the sense that N would be replaced by Q.
> >
> > Thats your idee fix. Sorry I cannot help you.
> >
> > Dan Christensen schrieb am Samstag, 7. Mai 2022 um 17:15:38 UTC+2:
> You two lovers should go to kievj and kiss the ring of the nazi home
> zelenskej, like everybody else. Big governments kissed the ring of
> zelenske, why not you??
>

You have it backwards, Nazi boy. Remember:

WAR OF AGRESSION = NAZI

If you have free access the internet (somehow I doubt it), check the English-language news from your closest ally, China. It is obvious that, while they do not outright call them "war crimes," there is coverage of Russia atrocities. Today, they report:

"Two months of war in Ukraine have left 7.7 million people internally displaced and driven over 5.5 million people across international borders, including nearly two-thirds of all children in Ukraine. Hundreds of children have been killed and many more have been injured," he pointed out.

"Nearly 200 attacks have been reported against health care facilities, and schools continue to be impacted by strikes."

Makes you real proud, don't it, Nazi boy? Doesn't look like even your best friends are much influenced by your lies.
So, are you ready to be a hero at the front? Something tells me there will be a shortage of bullet-proof vests. Don't expect your spiffy new SS uniform to offer much protection. Save at least one bullet in your pocket, for, well... you know.

This substitution, which is only a way of speaking,
for having a model with s = succZ, works also in
your DC Proof tool. Using dcpsetup9.exe I get:

1 succZ=s
Axiom

2 ALL(a):[a ε n => ~s(a)=0]
Axiom

3 ALL(a):[a ε n => ~succZ(a)=0]
Substitute, 1, 2

Thats just equality in a proof tool, in the case of
DC Proof equality is also available for function symbols.
At least what the usual equality laws concerns, you do not really

need to define axioms for f=g in DC Proof. You only need to
define more axioms when you want more function symbols
to be equal, than the quality that is already available in

DC Proof. But the available equality is sufficient to explain
what the replacement is, there is no automatic replacment of
n=z, if you do not say so. Same for any s=succX, which shows

that your Peano Axioms are an open formulation, since one
can easily verify that all of your Peano Axioms are still satisfied
when succ | N = succN.

In an open formulation this here is not provable:

/* not provable because of use of open formalism */
ALL(a):ALL(b):[s(a)=b => a e n & a e n]

In a closed formulation, it can be made provable.

/* with some grafting of function application */
ALL(a):ALL(b):[s(a)=b => a e n & a e n]

Dan Christensens Peano Axioms lacks the so called
"closed world assumption", CWA:

https://en.wikipedia.org/wiki/Closed-world_assumption

Mostowski Collapse schrieb am Samstag, 7. Mai 2022 um 21:54:04 UTC+2:
> This substitution, which is only a way of speaking,
> for having a model with s = succZ, works also in
> your DC Proof tool. Using dcpsetup9.exe I get:
>
> 1 succZ=s
> Axiom
>
> 2 ALL(a):[a ε n => ~s(a)=0]
> Axiom
>
> 3 ALL(a):[a ε n => ~succZ(a)=0]
> Substitute, 1, 2
>
> Thats just equality in a proof tool, in the case of
> DC Proof equality is also available for function symbols.
> At least what the usual equality laws concerns, you do not really
>
> need to define axioms for f=g in DC Proof. You only need to
> define more axioms when you want more function symbols
> to be equal, than the quality that is already available in
>
> DC Proof. But the available equality is sufficient to explain
> what the replacement is, there is no automatic replacment of
> n=z, if you do not say so. Same for any s=succX, which shows
>
> that your Peano Axioms are an open formulation, since one
> can easily verify that all of your Peano Axioms are still satisfied
> when succ | N = succN.

Why is the closed world assumption missing?
Well because he uses:

ALL(a):[a e n => s(a) e n]

And not the more common:

s : n -> n

If he would use the more common s : n -> n, and if
he had a system with some grafting of function

application he could also exclude all dom(succX) =\= n.

Mostowski Collapse schrieb am Samstag, 7. Mai 2022 um 22:11:31 UTC+2:
> In an open formulation this here is not provable:
>
> /* not provable because of use of open formalism */
> ALL(a):ALL(b):[s(a)=b => a e n & a e n]
>
> In a closed formulation, it can be made provable.
>
> /* with some grafting of function application */
> ALL(a):ALL(b):[s(a)=b => a e n & a e n]
>
> Dan Christensens Peano Axioms lacks the so called
> "closed world assumption", CWA:
>
> https://en.wikipedia.org/wiki/Closed-world_assumption
> Mostowski Collapse schrieb am Samstag, 7. Mai 2022 um 21:54:04 UTC+2:
> > This substitution, which is only a way of speaking,
> > for having a model with s = succZ, works also in
> > your DC Proof tool. Using dcpsetup9.exe I get:
> >
> > 1 succZ=s
> > Axiom
> >
> > 2 ALL(a):[a ε n => ~s(a)=0]
> > Axiom
> >
> > 3 ALL(a):[a ε n => ~succZ(a)=0]
> > Substitute, 1, 2
> >
> > Thats just equality in a proof tool, in the case of
> > DC Proof equality is also available for function symbols.
> > At least what the usual equality laws concerns, you do not really
> >
> > need to define axioms for f=g in DC Proof. You only need to
> > define more axioms when you want more function symbols
> > to be equal, than the quality that is already available in
> >
> > DC Proof. But the available equality is sufficient to explain
> > what the replacement is, there is no automatic replacment of
> > n=z, if you do not say so. Same for any s=succX, which shows
> >
> > that your Peano Axioms are an open formulation, since one
> > can easily verify that all of your Peano Axioms are still satisfied
> > when succ | N = succN.

Dan Christensen wrote:

idiot, it just reveals your incompetency. Engilsh written by a chinese, in
science papers, is absurd.

> "Two months of war in Ukraine have left 7.7 million people internally
> displaced and driven over 5.5 million people across international
> borders, including nearly two-thirds of all children in Ukraine.
> Hundreds of children have been killed and many more have been injured,"
> he pointed out. "Nearly 200 attacks have been reported against health
> care facilities, and schools continue to be impacted by strikes."

all, admittedly, done by the nazi ukraine, you lying nazi pig. You know
what I say is true. It stays everywhere. Your country is a capitalist
shithole. You forgot the link, nazi.

A captured militant of the Armed Forces of Ukraine about the crimes of the
Ukrainian command https://www.bitchute.com/video/69xwcmk3acmf/

On Saturday, May 7, 2022 at 4:23:21 PM UTC-4, Mitch Yamaguchi wrote:
> Dan Christensen wrote:
>
> idiot, it just reveals your incompetency. Engilsh written by a chinese, in
> science papers, is absurd.
> > "Two months of war in Ukraine have left 7.7 million people internally
> > displaced and driven over 5.5 million people across international
> > borders, including nearly two-thirds of all children in Ukraine.
> > Hundreds of children have been killed and many more have been injured,"
> > he pointed out. "Nearly 200 attacks have been reported against health
> > care facilities, and schools continue to be impacted by strikes."

> all, admittedly, done by the nazi ukraine, you lying nazi pig.

Wow, you really are a useful idiot! Not even the Chinese are buying into that shit. Maybe they are hoping to buy up Russia after the war. Should go fairly cheaply.

You are now truly alone in the world and will be for several generations, comrade. Not even the Chinese will trust you.

Well the point is that you can classify axiom systems into CWA
and OWA. Depending on how they see for example:

ALL(a):ALL(b):[s(a)=b => a e n & b e n]

Your Peano Axioms tend towards OWA. Since your Peano Axioms
are satisfiable by any function s where s agrees on N with the

successor on the natural numbers.

For CWA / OWA see here:
https://en.wikipedia.org/wiki/Closed-world_assumption

Dan Christensen schrieb am Samstag, 7. Mai 2022 um 22:44:38 UTC+2:
> Not sure what point you are tying to make. The only
requirement of an axiom is that it be syntactically correct.
There is no check for logical consistency. You could even
have an axiom P & ~P just to see what would happen.

Dan Christensen wrote:

>> > he pointed out. "Nearly 200 attacks have been reported against health
>> > care facilities, and schools continue to be impacted by strikes."
>
>> all, admittedly, done by the nazi ukraine, you lying nazi pig.
>
> Wow, you really are a useful idiot! Not even the Chinese are buying into
> that shit. Maybe they are hoping to buy up Russia after the war. Should
> go fairly cheaply.
>
> You are now truly alone in the world and will be for several
> generations, comrade. Not even the Chinese will trust you.

you are lying your ass out. Put the link, I bet you push mainstream
propaganda, confusing a capitalist site with china. China capitalist too,
but you are lying.

Here, if you know "ukrainian" as I do, from the people, you hear "nazis"
and zelenske, the nazi puppet.

a mariopol "ukrainian" horror guilt
https://www.bitchute.com/video/7eh7ZODlMyRW/

you won't call that for a country, would you.

Other names for OWA axioms systems are:
- dark elements tsunami
- extrensic intrinsic confusion
- Russell swirling in his grave
- You are using my ALL(_) wrong
- black matter hell

- blame it on the empty set
- Half-Functions
- extension function spaces

- ad hoc axioms boom boom
- Poop-Mathematics
- Etc...

LMAO!

Mostowski Collapse schrieb:
> Well the point is that you can classify axiom systems into CWA
> and OWA. Depending on how they see for example:
>
> ALL(a):ALL(b):[s(a)=b => a e n & b e n]
>
> Your Peano Axioms tend towards OWA. Since your Peano Axioms
> are satisfiable by any function s where s agrees on N with the
>
> successor on the natural numbers.
>
> For CWA / OWA see here:
> https://en.wikipedia.org/wiki/Closed-world_assumption
>
> Dan Christensen schrieb am Samstag, 7. Mai 2022 um 22:44:38 UTC+2:
> > Not sure what point you are tying to make. The only
> requirement of an axiom is that it be syntactically correct.
> There is no check for logical consistency. You could even
> have an axiom P & ~P just to see what would happen.

Mostowski Collapse wrote:

> Other names for OWA axioms systems are:
> - dark elements tsunami - extrensic intrinsic confusion - Russell
> swirling in his grave - You are using my ALL(_) wrong - black matter
> hell

that's exactly a blackhole bellow the event horizon. Try again.

OWA axioms systems have their justification
when you study classes of different
mathematical structure.

But I wouldn't know that Peano Structures
form a larger class of different
mathematical structures.

Since there is this theorem, isn't it?
- All Peano Structures are isomorphic?

You can only prove the theorem if you
use s : n -> n, it doesn't work if you
use ALL(a):[a e n => s(a) e n].

Mostowski Collapse schrieb:
>
> Other names for OWA axioms systems are:
> - dark elements tsunami
> - extrensic intrinsic confusion
> - Russell swirling in his grave
> - You are using my ALL(_) wrong
> - black matter hell
>
> - blame it on the empty set
> - Half-Functions
> - extension function spaces
>
> - ad hoc axioms boom boom
> - Poop-Mathematics
> - Etc...
>
> LMAO!
>
> Mostowski Collapse schrieb:
>> Well the point is that you can classify axiom systems into CWA
>> and OWA. Depending on how they see for example:
>>
>> ALL(a):ALL(b):[s(a)=b => a e n & b e n]
>>
>> Your Peano Axioms tend towards OWA. Since your Peano Axioms
>> are satisfiable by any function s where s agrees on N with the
>>
>> successor on the natural numbers.
>>
>> For CWA / OWA see here:
>> https://en.wikipedia.org/wiki/Closed-world_assumption
>>
>> Dan Christensen schrieb am Samstag, 7. Mai 2022 um 22:44:38 UTC+2:
>>  > Not sure what point you are tying to make. The only
>> requirement of an axiom is that it be syntactically correct.
>> There is no check for logical consistency. You could even
>> have an axiom P & ~P just to see what would happen.
>

On Saturday, May 7, 2022 at 5:28:14 PM UTC-4, Mostowski Collapse wrote:
> OWA axioms systems have their justification
> when you study classes of different
> mathematical structure.
>
> But I wouldn't know that Peano Structures
> form a larger class of different
> mathematical structures.
>
> Since there is this theorem, isn't it?
> - All Peano Structures are isomorphic?
>

Yes.

http://dcproof.com/PeanoThm1.htm (723 lines)
http://dcproof.com/PeanoThm2.htm (188 lines)
http://dcproof.com/PeanoThm3.htm (167 lines)

Dan

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

On Saturday, May 7, 2022 at 5:28:14 PM UTC-4, Mostowski Collapse wrote:
> OWA axioms systems have their justification
> when you study classes of different
> mathematical structure.
>
> But I wouldn't know that Peano Structures
> form a larger class of different
> mathematical structures.
>
> Since there is this theorem, isn't it?
> - All Peano Structures are isomorphic?
>

Yes.

If we have Peano systems (n,0,next) and (n',0',next') then there existence a unique function f mapping n to n' such that
1. f(0)=0'
2. f(next(x)) = next'(f(x))
http://dcproof.com/PeanoThm1.htm (723 lines)

The unique mapping between a pair of Peano systems (n,0,next) and (n',0,next') is a bijection.
http://dcproof.com/PeanoThm2.htm (188 lines)

The bijective mapping from n to n' preserves the successor relations on n and n'
http://dcproof.com/PeanoThm3.htm (167 lines)

Dan

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

Still utter nonsense, you use extrensic parameters.
You only proved:

next | n1 ~ next‘ | n2

Where f | A denotes f restricted to A. You didnt show
next ~ next‘, or do you for example claim

succQ ~ succN

which are both satisfied by your Peano Axioms and
where ~ denotes isomorphism?

LoL

P.S.: For isomorphism you need to have f : dom(next) ->
dom(next‘) and not your nonsense ALL(a):[a e n1 => f(a) e n2].

Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 06:17:03 UTC+2:
> On Saturday, May 7, 2022 at 5:28:14 PM UTC-4, Mostowski Collapse wrote:
> > OWA axioms systems have their justification
> > when you study classes of different
> > mathematical structure.
> >
> > But I wouldn't know that Peano Structures
> > form a larger class of different
> > mathematical structures.
> >
> > Since there is this theorem, isn't it?
> > - All Peano Structures are isomorphic?
> >
> Yes.
>
> If we have Peano systems (n,0,next) and (n',0',next') then there existence a unique function f mapping n to n' such that
> 1. f(0)=0'
> 2. f(next(x)) = next'(f(x))
> http://dcproof.com/PeanoThm1.htm (723 lines)
>
> The unique mapping between a pair of Peano systems (n,0,next) and (n',0,next') is a bijection.
> http://dcproof.com/PeanoThm2.htm (188 lines)
>
> The bijective mapping from n to n' preserves the successor relations on n and n'
> http://dcproof.com/PeanoThm3.htm (167 lines)
> 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, May 8, 2022 at 5:08:55 AM UTC-4, Mostowski Collapse wrote:

> P.S.: For isomorphism you need to have f : dom(next) ->
> dom(next‘) and not your nonsense ALL(a):[a e n1 => f(a) e n2].
> Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 06:17:03 UTC+2:
> > On Saturday, May 7, 2022 at 5:28:14 PM UTC-4, Mostowski Collapse wrote:
> > > OWA axioms systems have their justification
> > > when you study classes of different
> > > mathematical structure.
> > >
> > > But I wouldn't know that Peano Structures
> > > form a larger class of different
> > > mathematical structures.
> > >
> > > Since there is this theorem, isn't it?
> > > - All Peano Structures are isomorphic?
> > >
> > Yes.
> >
> > If we have Peano systems (n,0,next) and (n',0',next') then there existence a unique function f mapping n to n' such that
> > 1. f(0)=0'
> > 2. f(next(x)) = next'(f(x))
> > http://dcproof.com/PeanoThm1.htm (723 lines)
> >
> > The unique mapping between a pair of Peano systems (n,0,next) and (n',0,next') is a bijection.
> > http://dcproof.com/PeanoThm2.htm (188 lines)
> >
> > The bijective mapping from n to n' preserves the successor relations on n and n'
> > http://dcproof.com/PeanoThm3.htm (167 lines)

> Still utter nonsense, you use extrensic parameters.

This from a crank who believes he can make logical inferences about a function outside of it domain of definition, i.e. where it is undefined -- your DARK ELEMENTS!

> You only proved:
>
> next | n1 ~ next‘ | n2
>

I proved than all Peano systems are essentially the same structure. The names of things may differ, but it is the SAME structure. In this sense, there is only one Peano system. Deal with it, 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

Not the same next and next', only restricted to n1 and n2.
This has some consequences, for example you cannot prove:

~EXIST(a):[next(a)=0]

Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 17:21:24 UTC+2:
> On Sunday, May 8, 2022 at 5:08:55 AM UTC-4, Mostowski Collapse wrote:
> I proved than all Peano systems are essentially the same structure. The names of things may differ, but it is the SAME structure. In this sense, there is only one Peano system. Deal with it, Jan Burse.

On Sunday, May 8, 2022 at 11:27:05 AM UTC-4, Mostowski Collapse (akawrote:

> Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 17:21:24 UTC+2:
> > On Sunday, May 8, 2022 at 5:08:55 AM UTC-4, Mostowski Collapse wrote:
> > I proved than all Peano systems are essentially the same structure. The names of things may differ, but it is the SAME structure. In this sense, there is only one Peano system. Deal with it, Jan Burse.

> Not the same next and next', only restricted to n1 and n2.

Pay attention, Jan Burse! I am comparing different structures, each including a set, an element of that set and a function with certain properties on that set.

> This has some consequences, for example you cannot prove:
>
> ~EXIST(a):[next(a)=0]

Why would I want to prove such nonsense? Perhaps you are confusing it with one of Peano's Axioms: ALL(a):[a in n => ~s(a)=0] or equivalently ~EXIST(a):[a in n & s(a)=0]. In mathematics, you almost always want to restrict every quantifier. You usually don't want to be talking about every object in the universe.

Dan

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

Try proving:

ALL(a):[~Even(a) => Even(next(a))]

LoL

Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 20:36:14 UTC+2:
> On Sunday, May 8, 2022 at 11:27:05 AM UTC-4, Mostowski Collapse (akawrote:
> > Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 17:21:24 UTC+2:
> > > On Sunday, May 8, 2022 at 5:08:55 AM UTC-4, Mostowski Collapse wrote:
> > > I proved than all Peano systems are essentially the same structure. The names of things may differ, but it is the SAME structure. In this sense, there is only one Peano system. Deal with it, Jan Burse.
> > Not the same next and next', only restricted to n1 and n2.
> Pay attention, Jan Burse! I am comparing different structures, each including a set, an element of that set and a function with certain properties on that set.
> > This has some consequences, for example you cannot prove:
> >
> > ~EXIST(a):[next(a)=0]
> Why would I want to prove such nonsense? Perhaps you are confusing it with one of Peano's Axioms: ALL(a):[a in n => ~s(a)=0] or equivalently ~EXIST(a):[a in n & s(a)=0]. In mathematics, you almost always want to restrict every quantifier. You usually don't want to be talking about every object in the universe.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Wait, I am trying to make a better example with Even.
Ok, this is the better example, which corresponds
to the usual expectation we have about Even(_):

ALL(a):[Even(a) => ~Even(next(a))]

Can you prove it from Your Peano Axioms and
from Your Even Axiom? I guess no. What if
a = -1, one of the Dark Elements,

that could be found in your Even(_) sometimes?

Mostowski Collapse schrieb am Sonntag, 8. Mai 2022 um 20:39:11 UTC+2:
> Try proving:
>
> ALL(a):[~Even(a) => Even(next(a))]
>
> LoL
> Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 20:36:14 UTC+2:
> > On Sunday, May 8, 2022 at 11:27:05 AM UTC-4, Mostowski Collapse (akawrote:
> > > Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 17:21:24 UTC+2:
> > > > On Sunday, May 8, 2022 at 5:08:55 AM UTC-4, Mostowski Collapse wrote:
> > > > I proved than all Peano systems are essentially the same structure. The names of things may differ, but it is the SAME structure. In this sense, there is only one Peano system. Deal with it, Jan Burse.
> > > Not the same next and next', only restricted to n1 and n2.
> > Pay attention, Jan Burse! I am comparing different structures, each including a set, an element of that set and a function with certain properties on that set.
> > > This has some consequences, for example you cannot prove:
> > >
> > > ~EXIST(a):[next(a)=0]
> > Why would I want to prove such nonsense? Perhaps you are confusing it with one of Peano's Axioms: ALL(a):[a in n => ~s(a)=0] or equivalently ~EXIST(a):[a in n & s(a)=0]. In mathematics, you almost always want to restrict every quantifier. You usually don't want to be talking about every object in the universe.
> > 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, May 8, 2022 at 2:45:06 PM UTC-4, Mostowski Collapse wrote:
> Wait, I am trying to make a better example with Even.
> Ok, this is the better example, which corresponds
> to the usual expectation we have about Even(_):
>
> ALL(a):[Even(a) => ~Even(next(a))]
>

You would need to restrict the quantifier to N. Then, given the basic rules of arithmetic, you could then use a proof by contradiction.

Dan

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

Thats not how Euclid formulates it:

7. An odd number is that which is not divisible into two equal parts, or that which differs by a unit from an even number.

He also uses the definition format with Even(_) in front:

6. An even number is that which is divisible into two equal parts.

Which translates to:

ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]

Even(a): An even number
<=>: is
Number(a): that which [number]
EXIST(b):[Number(b) & a=2*b]: is divisible into two equal parts

Very easy....

Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 21:59:28 UTC+2:
> On Sunday, May 8, 2022 at 2:45:06 PM UTC-4, Mostowski Collapse wrote:
> > Wait, I am trying to make a better example with Even.
> > Ok, this is the better example, which corresponds
> > to the usual expectation we have about Even(_):
> >
> > ALL(a):[Even(a) => ~Even(next(a))]
> >
> You would need to restrict the quantifier to N. Then, given the basic rules of arithmetic, you could then use a proof by contradiction.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

What about:

/* Dan-O-Matik Style */
ALL(a):[Number(a) => [Even(a) <=> EXIST(b):[Number(b) & a=2*b]]]
ALL(a):[Number(a) => [Odd(a) <=> ~EXIST(b):[Number(b) & a=2*b]]]

Can you prove in DC Proof, both Even and Odd will have Dark Elements:

ALL(a):[Even(a) => Odd(s(a))]

Possibly no. But I guess it works with ordinary style:

/* Ordinary Style = Euclid Style */
ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]
ALL(a):[Odd(a) <=> [Number(a) & ~EXIST(b):[Number(b) & a=2*b]]]

Mostowski Collapse schrieb am Sonntag, 8. Mai 2022 um 22:11:24 UTC+2:
> Thats not how Euclid formulates it:
>
> 7. An odd number is that which is not divisible into two equal parts, or that which differs by a unit from an even number.
>
> He also uses the definition format with Even(_) in front:
>
> 6. An even number is that which is divisible into two equal parts.
>
> Which translates to:
>
> ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]
>
> Even(a): An even number
> <=>: is
> Number(a): that which [number]
> EXIST(b):[Number(b) & a=2*b]: is divisible into two equal parts
>
> Very easy....
> Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 21:59:28 UTC+2:
> > On Sunday, May 8, 2022 at 2:45:06 PM UTC-4, Mostowski Collapse wrote:
> > > Wait, I am trying to make a better example with Even.
> > > Ok, this is the better example, which corresponds
> > > to the usual expectation we have about Even(_):
> > >
> > > ALL(a):[Even(a) => ~Even(next(a))]
> > >
> > You would need to restrict the quantifier to N. Then, given the basic rules of arithmetic, you could then use a proof by contradiction.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com