We are still waiting for axioms that give classical even and odd,
not this nonsense here:

https://dcproof.com/EvenNextOdd.htm

So that we can prove:

ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Odd(b) => ~a+b=0]]

Dan Christensen schrieb am Sonntag, 22. Mai 2022 um 21:04:53 UTC+2:
> On Sunday, May 22, 2022 at 4:44:52 AM UTC-4, Mostowski Collapse wrote:
> > No mathematician is this careless as you are.
> >
> [snip]
>
> None are as desperate as you, Jan Burse. Learn some math and just admit you were wrong and save yourself all this embarrassment.
>
> Dan

A counter model, that satisfies the nonsense axioms,
and violates this formula:

ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Odd(b) => ~a+b=0]],

is easy. Take F4:

+ 0 1 2 3
0 0 1 2 3
1 1 2 3 0
2 2 3 0 1
3 3 0 1 2

Take a=1 and b=3, both are odd. But 1+3=0. Whats more
difficult, and I didn't find a counter model yet, is this here:

ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Even(b) => ~a+b=0]]

F3 doesn't work, since it does not satisfy the nonsense axioms,

+ 0 1 2
0 0 1 2
1 1 2 0
2 2 0 1

it violates this axiom from Dan-O-Matik:

10 ~EXIST(a):[a e n & 2*a=1]
Axiom
https://dcproof.com/EvenNextOdd.htm

Take a=2, then a+a=1.

Mostowski Collapse schrieb am Montag, 23. Mai 2022 um 09:37:22 UTC+2:
> We are still waiting for axioms that give classical even and odd,
> not this nonsense here:
>
> https://dcproof.com/EvenNextOdd.htm
>
> So that we can prove:
>
> ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Odd(b) => ~a+b=0]]
> Dan Christensen schrieb am Sonntag, 22. Mai 2022 um 21:04:53 UTC+2:
> > On Sunday, May 22, 2022 at 4:44:52 AM UTC-4, Mostowski Collapse wrote:
> > > No mathematician is this careless as you are.
> > >
> > [snip]
> >
> > None are as desperate as you, Jan Burse. Learn some math and just admit you were wrong and save yourself all this embarrassment.
> >
> > Dan

On Monday, May 23, 2022 at 3:37:22 AM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> We are still waiting ...
>
> https://dcproof.com/EvenNextOdd.htm
>
[snip]

Thank you for your interest. There, given a few basic results of basic arithmetic on lines 1-14, each derivable from Peano's Axioms, I formally prove (in 127 lines):

(1) ALL(a):[a e n => [Even(a) => Odd(a+1)]]

(2) ALL(a):[a e n => Even(2*a) & Odd(2*a+1)]

Where n = the set of natural numbers

Even and Odd are defined as usual (lines 15-16):

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

ALL(a):[Odd(a) <=> ~Even(a)]

Nothing very profound, it simply demonstrates how to correctly introduce definitions (Even and Odd here).
I hope this clears up your obvious confusion, 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

So its not possibly to define the classical even and odd in DC Proof?
What is it useful then? You cannot define even and odd so

that this is provable?

ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Even(b) => ~a+b=0]]

So DC Proof is a total failure, just like Archimedes
Plutonium and John Gabriel are?

LoL

Mostowski Collapse schrieb am Montag, 23. Mai 2022 um 09:37:22 UTC+2:
> We are still waiting for axioms that give classical even and odd,
> not this nonsense here:
>
> https://dcproof.com/EvenNextOdd.htm
>
> So that we can prove:
>
> ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Odd(b) => ~a+b=0]]
> Dan Christensen schrieb am Sonntag, 22. Mai 2022 um 21:04:53 UTC+2:
> > On Sunday, May 22, 2022 at 4:44:52 AM UTC-4, Mostowski Collapse wrote:
> > > No mathematician is this careless as you are.
> > >
> > [snip]
> >
> > None are as desperate as you, Jan Burse. Learn some math and just admit you were wrong and save yourself all this embarrassment.
> >
> > Dan

Of course its a difficult question, what are the classical numbers from
Euclid. Are we allowed to equate them with Peano Axioms? Are there
alternatives. This alternative here looks like utter nonsense:

https://dcproof.com/EvenNextOdd.htm

What happended to mathematical induction? Did you sweep it
under the rug? Are there alternatives to mathematical induction.
And how to fix that {0,1,2,3} isn't a model when you miss out

mathematical induction? I find for example here some alternatives:

¬(x < 0)
x < Sy ↔ (x < y ∨ x = y)
x < y ∨ x = y ∨ y < x
https://en.wikipedia.org/wiki/Robinson_arithmetic#Variant_axiomatizations

You could then use an alternative to mathematical induction,
for example course of value induction, but I guess you cannot
omit any form of induction:

ALL(b):[ALL(a):[a < b => P(a)]=>P(b)] => ALL(c):P(c)

(Not sure where Euclid had induction, did he somewhere?)

Mostowski Collapse schrieb am Montag, 23. Mai 2022 um 17:45:17 UTC+2:
> So its not possibly to define the classical even and odd in DC Proof?
> What is it useful then? You cannot define even and odd so
>
> that this is provable?
>
> ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Even(b) => ~a+b=0]]
>
> So DC Proof is a total failure, just like Archimedes
> Plutonium and John Gabriel are?
>
> LoL
> Mostowski Collapse schrieb am Montag, 23. Mai 2022 um 09:37:22 UTC+2:
> > We are still waiting for axioms that give classical even and odd,
> > not this nonsense here:
> >
> > https://dcproof.com/EvenNextOdd.htm
> >
> > So that we can prove:
> >
> > ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Odd(b) => ~a+b=0]]
> > Dan Christensen schrieb am Sonntag, 22. Mai 2022 um 21:04:53 UTC+2:
> > > On Sunday, May 22, 2022 at 4:44:52 AM UTC-4, Mostowski Collapse wrote:
> > > > No mathematician is this careless as you are.
> > > >
> > > [snip]
> > >
> > > None are as desperate as you, Jan Burse. Learn some math and just admit you were wrong and save yourself all this embarrassment.
> > >
> > > Dan

Here is a lead:

The logical and scientific process called induction dates back
as far as Cicero's translation of Aristotle. Cicero used the latin
term "inductio", for the Greek "epagoge", which translates as "leading to."
https://pballew.blogspot.com/2009/09/mathematical-induction-brief-history-of.html

Mostowski Collapse schrieb am Montag, 23. Mai 2022 um 17:56:54 UTC+2:
> Of course its a difficult question, what are the classical numbers from
> Euclid. Are we allowed to equate them with Peano Axioms? Are there
> alternatives. This alternative here looks like utter nonsense:
>
> https://dcproof.com/EvenNextOdd.htm
>
> What happended to mathematical induction? Did you sweep it
> under the rug? Are there alternatives to mathematical induction.
> And how to fix that {0,1,2,3} isn't a model when you miss out
>
> mathematical induction? I find for example here some alternatives:
>
> ¬(x < 0)
> x < Sy ↔ (x < y ∨ x = y)
> x < y ∨ x = y ∨ y < x
> https://en.wikipedia.org/wiki/Robinson_arithmetic#Variant_axiomatizations
>
> You could then use an alternative to mathematical induction,
> for example course of value induction, but I guess you cannot
> omit any form of induction:
>
> ALL(b):[ALL(a):[a < b => P(a)]=>P(b)] => ALL(c):P(c)
>
> (Not sure where Euclid had induction, did he somewhere?)
> Mostowski Collapse schrieb am Montag, 23. Mai 2022 um 17:45:17 UTC+2:
> > So its not possibly to define the classical even and odd in DC Proof?
> > What is it useful then? You cannot define even and odd so
> >
> > that this is provable?
> >
> > ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Even(b) => ~a+b=0]]
> >
> > So DC Proof is a total failure, just like Archimedes
> > Plutonium and John Gabriel are?
> >
> > LoL
> > Mostowski Collapse schrieb am Montag, 23. Mai 2022 um 09:37:22 UTC+2:
> > > We are still waiting for axioms that give classical even and odd,
> > > not this nonsense here:
> > >
> > > https://dcproof.com/EvenNextOdd.htm
> > >
> > > So that we can prove:
> > >
> > > ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Odd(b) => ~a+b=0]]
> > > Dan Christensen schrieb am Sonntag, 22. Mai 2022 um 21:04:53 UTC+2:
> > > > On Sunday, May 22, 2022 at 4:44:52 AM UTC-4, Mostowski Collapse wrote:
> > > > > No mathematician is this careless as you are.
> > > > >
> > > > [snip]
> > > >
> > > > None are as desperate as you, Jan Burse. Learn some math and just admit you were wrong and save yourself all this embarrassment.
> > > >
> > > > Dan

On Monday, May 23, 2022 at 11:45:17 AM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> So its not possibly to define the classical even and odd in DC Proof?

You can define them as wonky as you wish, Jan Burse. I was simply demonstrating the best way to formally define them WITHOUT any of your typical wonkiness. None of your "dark elements," sorry.

Dan

And why is this not provable from your nonsense:

/* Not Provable in Dan-O-Matik Nonsense */
ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Even(b) => ~a+b=0]]
https://dcproof.com/EvenNextOdd.htm

I think you defined some Odd and Even that could be also from Mars.

Dan Christensen schrieb am Montag, 23. Mai 2022 um 21:01:47 UTC+2:
> On Monday, May 23, 2022 at 11:45:17 AM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> > So its not possibly to define the classical even and odd in DC Proof?
> You can define them as wonky as you wish, Jan Burse. I was simply demonstrating the best way to formally define them WITHOUT any of your typical wonkiness. None of your "dark elements," sorry.
>
> Dan

On Tuesday, May 24, 2022 at 8:09:23 AM UTC-4, Mostowski Collapse wrote:
> And why is this not provable from your nonsense:
>
> /* Not Provable in Dan-O-Matik Nonsense */
> ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Even(b) => ~a+b=0]]
> https://dcproof.com/EvenNextOdd.htm
>

[snip]

Do pay attention Jan Burse! I listed ONLY those results of from basic arithmetic on N (lines 1-14) that were necessary to prove the theorem and corollary in question.

Dan

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

Prove more theorems from your nonsense.

Dan Christensen schrieb am Dienstag, 24. Mai 2022 um 16:47:55 UTC+2:
> On Tuesday, May 24, 2022 at 8:09:23 AM UTC-4, Mostowski Collapse wrote:
> > And why is this not provable from your nonsense:
> >
> > /* Not Provable in Dan-O-Matik Nonsense */
> > ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Even(b) => ~a+b=0]]
> > https://dcproof.com/EvenNextOdd.htm
> >
> [snip]
>
> Do pay attention Jan Burse! I listed ONLY those results of from basic arithmetic on N (lines 1-14) that were necessary to prove the theorem and corollary in question.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Thats also a lie. Not all are necessary:
- Multiplication is not necessary, you can use a+a for 2*a.
- If you had addition correctly you could then prove:

10 ~EXIST(a):[a e n & 2*a=1]

Respectively:

10 ~EXIST(a):[a e n & a+a=1]

Why do you need this as an axiom? Doesnt your addition
on the natural numbers already deliever this result?

BTW: Your axioms have an interesting model: make
multiplication behave like this a*b=0. This explains why

you can even not prove this here from your nonsense:

/* Not Provable from Dan Christensen Nonsense */
EXIST(a):[a e n & ~a=0 & Even(a)]

Mostowski Collapse schrieb am Dienstag, 24. Mai 2022 um 18:02:16 UTC+2:
> Prove more theorems from your nonsense.
> Dan Christensen schrieb am Dienstag, 24. Mai 2022 um 16:47:55 UTC+2:
> > On Tuesday, May 24, 2022 at 8:09:23 AM UTC-4, Mostowski Collapse wrote:
> > > And why is this not provable from your nonsense:
> > >
> > > /* Not Provable in Dan-O-Matik Nonsense */
> > > ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Even(b) => ~a+b=0]]
> > > https://dcproof.com/EvenNextOdd.htm
> > >
> > [snip]
> >
> > Do pay attention Jan Burse! I listed ONLY those results of from basic arithmetic on N (lines 1-14) that were necessary to prove the theorem and corollary in question.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Because your multiplication is so fluffy, a*b=0 is also
a model of your axioms, in this multiplication we would have:

Even = {0}
Odd = {1,2,3,4,…}

And this praised corollary of yours,

2) ALL(a):[a e n => Even(2*a) & Odd(2*a+1)]

since a*b=0 is a model, doesnt say more than:

Even(0) & Odd(0+1)

Mostowski Collapse schrieb am Dienstag, 24. Mai 2022 um 18:17:07 UTC+2:
> Thats also a lie. Not all are necessary:
> - Multiplication is not necessary, you can use a+a for 2*a.
> - If you had addition correctly you could then prove:
> 10 ~EXIST(a):[a e n & 2*a=1]
> Respectively:
>
> 10 ~EXIST(a):[a e n & a+a=1]
>
> Why do you need this as an axiom? Doesnt your addition
> on the natural numbers already deliever this result?
>
> BTW: Your axioms have an interesting model: make
> multiplication behave like this a*b=0. This explains why
>
> you can even not prove this here from your nonsense:
>
> /* Not Provable from Dan Christensen Nonsense */
> EXIST(a):[a e n & ~a=0 & Even(a)]
> Mostowski Collapse schrieb am Dienstag, 24. Mai 2022 um 18:02:16 UTC+2:
> > Prove more theorems from your nonsense.
> > Dan Christensen schrieb am Dienstag, 24. Mai 2022 um 16:47:55 UTC+2:
> > > On Tuesday, May 24, 2022 at 8:09:23 AM UTC-4, Mostowski Collapse wrote:
> > > > And why is this not provable from your nonsense:
> > > >
> > > > /* Not Provable in Dan-O-Matik Nonsense */
> > > > ALL(a):ALL(b):[a e n & b e n => [Odd(a) & Even(b) => ~a+b=0]]
> > > > https://dcproof.com/EvenNextOdd.htm
> > > >
> > > [snip]
> > >
> > > Do pay attention Jan Burse! I listed ONLY those results of from basic arithmetic on N (lines 1-14) that were necessary to prove the theorem and corollary in question.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Tuesday, May 24, 2022 at 12:17:07 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> Thats also a lie. Not all are necessary:
> - Multiplication is not necessary, you can use a+a for 2*a.
> - If you had addition correctly you could then prove:
> 10 ~EXIST(a):[a e n & 2*a=1]
> Respectively:
>
> 10 ~EXIST(a):[a e n & a+a=1]
>
[snip]

Poor, desperate Jan Burse, he is grasping at straws as always! (HA, HA, HA!!!)

Just admit you were wrong and avoid embarrassing yourself like this.

Dan

On Tuesday, May 24, 2022 at 12:29:05 PM UTC-4, Mostowski Collapse wrote:
> Because your multiplication is so fluffy, a*b=0 is also
> a model of your axioms, in this multiplication we would have:
>
> Even = {0}
> Odd = {1,2,3,4,…}
>

[snip]

Could you be more desperate, Jan Burse? (HA, HA, HA!!!)

Dan

Can you please prove this here with your Wonky Even and Odd:
Use your EvenNextOdd to prove:

f(1)=2
f(n)=f(n-1)+1 for n>1 & Even(n)
f(n)=f(n-2)+2 for n>1 & Odd(n)
=>
f(2017)=2018

Source:

MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics,
Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas - 2021
https://github.com/openai/miniF2F

I don't think you can prove it. You cannot prove:

EXIST(a):[a e n & ~a=0 & Even(n)]

So how would you derive f(2017)=2018?

Dan Christensen schrieb am Mittwoch, 25. Mai 2022 um 01:54:25 UTC+2:
> On Tuesday, May 24, 2022 at 12:29:05 PM UTC-4, Mostowski Collapse wrote:
> > Because your multiplication is so fluffy, a*b=0 is also
> > a model of your axioms, in this multiplication we would have:
> >
> > Even = {0}
> > Odd = {1,2,3,4,…}
> >
> [snip]
>
> Could you be more desperate, Jan Burse? (HA, HA, HA!!!)
>
> Dan

Hint, you only need to prove these two things:

ALL(a):[a e n => [Odd(a) => f(a) = a+1]]

Odd(2*10*10*10+1*10+7) where 10=2*2*2+2 and 7=2*2+2+1

Shouldn't be so difficult, except if one is using Wonky nonsense as here:

https://dcproof.com/EvenNextOdd.htm

Mostowski Collapse schrieb am Mittwoch, 25. Mai 2022 um 02:11:24 UTC+2:
> Can you please prove this here with your Wonky Even and Odd:
> Use your EvenNextOdd to prove:
>
> f(1)=2
> f(n)=f(n-1)+1 for n>1 & Even(n)
> f(n)=f(n-2)+2 for n>1 & Odd(n)
> =>
> f(2017)=2018
>
> Source:
>
> MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics,
> Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas - 2021
> https://github.com/openai/miniF2F
>
> I don't think you can prove it. You cannot prove:
>
> EXIST(a):[a e n & ~a=0 & Even(n)]
>
> So how would you derive f(2017)=2018?
> Dan Christensen schrieb am Mittwoch, 25. Mai 2022 um 01:54:25 UTC+2:
> > On Tuesday, May 24, 2022 at 12:29:05 PM UTC-4, Mostowski Collapse wrote:
> > > Because your multiplication is so fluffy, a*b=0 is also
> > > a model of your axioms, in this multiplication we would have:
> > >
> > > Even = {0}
> > > Odd = {1,2,3,4,…}
> > >
> > [snip]
> >
> > Could you be more desperate, Jan Burse? (HA, HA, HA!!!)
> >
> > Dan

Nope, an easier approach would be to prove this here:

ALL(a):[a e n => [a > 0 => f(a)=a+1]]

Here is a small test, that is what the function obviously does:

f(1, 2) :- !.
f(N, X) :- N mod 2 =:= 0, !, M is N-1, f(M, Y), X is Y+1.
f(N, X) :- M is N-2, f(M, Y), X is Y+2.

?- between(1,10,N), f(N,X), write(N-X), nl, fail; true.
1-2
2-3
3-4
4-5
5-6
6-7
7-8
8-9
9-10
10-11
true.

Mostowski Collapse schrieb am Mittwoch, 25. Mai 2022 um 02:15:33 UTC+2:
> Hint, you only need to prove these two things:
>
> ALL(a):[a e n => [Odd(a) => f(a) = a+1]]
>
> Odd(2*10*10*10+1*10+7) where 10=2*2*2+2 and 7=2*2+2+1
>
> Shouldn't be so difficult, except if one is using Wonky nonsense as here:
>
> https://dcproof.com/EvenNextOdd.htm
> Mostowski Collapse schrieb am Mittwoch, 25. Mai 2022 um 02:11:24 UTC+2:
> > Can you please prove this here with your Wonky Even and Odd:
> > Use your EvenNextOdd to prove:
> >
> > f(1)=2
> > f(n)=f(n-1)+1 for n>1 & Even(n)
> > f(n)=f(n-2)+2 for n>1 & Odd(n)
> > =>
> > f(2017)=2018
> >
> > Source:
> >
> > MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics,
> > Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas - 2021
> > https://github.com/openai/miniF2F
> >
> > I don't think you can prove it. You cannot prove:
> >
> > EXIST(a):[a e n & ~a=0 & Even(n)]
> >
> > So how would you derive f(2017)=2018?
> > Dan Christensen schrieb am Mittwoch, 25. Mai 2022 um 01:54:25 UTC+2:
> > > On Tuesday, May 24, 2022 at 12:29:05 PM UTC-4, Mostowski Collapse wrote:
> > > > Because your multiplication is so fluffy, a*b=0 is also
> > > > a model of your axioms, in this multiplication we would have:
> > > >
> > > > Even = {0}
> > > > Odd = {1,2,3,4,…}
> > > >
> > > [snip]
> > >
> > > Could you be more desperate, Jan Burse? (HA, HA, HA!!!)
> > >
> > > Dan

Why not simply prove (the set n of natural numbers not
shown, you should get the idea without showing it):

ALL(a):ALL(b):EXIST(c):[a+c=b | a=b+c]

Proof: We use this definition of +,
0+x=x
y'+x=(x+y)'
Smallest such +

Now try proof by induction for the above theorem:
Base Case: a=0
We need to show: ALL(b):EXIST(c):[0+c=b | 0=b+c]
We can use c=b to satisfy the EXIST

Inductive Step: a=n'
We need to show: ALL(b):EXIST(c):[n'+c=b | n'=b+c]

We make sub proof by induction:
Base Case: b=0
We need to show: EXIST(c):[n'+c=0 | n'=0+c]
We can use c=n' to satisfy the EXIST

Inductive Step: b=m'
We need to show: EXIST(c):[n'+c=m' | n'=m'+c]
Since n'+c = (n+c)', and since (n+c)'=m' is logical
equivalent to n+c=m. And since m'+c=(m+c)', and
since n'=(m+c)' is logical equivalent to n=m+c,
we need to show: EXIST(c):[n+c=m | n=m+c]
but this is just the outer induction hypothesis.

So the inner proof by induction can be closed.
And therefore the outer proof by induction as well.

Q.E.D.

We did only make use of Pressburger Arithmetic in the
previous lemma. Now lets do everything Even/Odd
in Pressburger Arithmetic as well!

We can use the previous lemma to show
the key lemma of EvenNextOdd:

LEMMA 76
ALL(a):ALL(b):[~(a+a = (b+b)')]
https://dcproof.com/EvenNextOdd.htm

By the previous post lemma we have:
EXIST(c):[a+c=b | a=b+c]

Now proof by cases:
Case 1: a+c=b, then the problem a+a = (b+b)'
reduces to a+a=(a+c+a+c)', and hence a+a=a+a+(c+c)'
using associativity and commutativity, which we
need also to prove first via induction, and we need a
cancellation lemma which we need also to prove
first via induction, and we do get 0=(c+c)'
which violates a peano axiom, so it is ~(a+a = (b+b)'.

Case 2: a=b+c, then the problem a+a = (b+b)' reduces
to (b+c+b+c)=(b+b)', and hence b+b+c+c=(b+b)',
and hence c+c=1, using 1=0', this needs a new proof
by induction, which will trivially show again that
this is not possible, so it is ~(a+a = (b+b)' again.

Q.E.D.

Mostowski Collapse schrieb am Freitag, 27. Mai 2022 um 13:58:52 UTC+2:
> Why not simply prove (the set n of natural numbers not
> shown, you should get the idea without showing it):
>
> ALL(a):ALL(b):EXIST(c):[a+c=b | a=b+c]
>
> Proof: We use this definition of +,
> 0+x=x
> y'+x=(x+y)'
> Smallest such +
>
> Now try proof by induction for the above theorem:
> Base Case: a=0
> We need to show: ALL(b):EXIST(c):[0+c=b | 0=b+c]
> We can use c=b to satisfy the EXIST
>
> Inductive Step: a=n'
> We need to show: ALL(b):EXIST(c):[n'+c=b | n'=b+c]
>
> We make sub proof by induction:
> Base Case: b=0
> We need to show: EXIST(c):[n'+c=0 | n'=0+c]
> We can use c=n' to satisfy the EXIST
>
> Inductive Step: b=m'
> We need to show: EXIST(c):[n'+c=m' | n'=m'+c]
> Since n'+c = (n+c)', and since (n+c)'=m' is logical
> equivalent to n+c=m. And since m'+c=(m+c)', and
> since n'=(m+c)' is logical equivalent to n=m+c,
> we need to show: EXIST(c):[n+c=m | n=m+c]
> but this is just the outer induction hypothesis.
>
> So the inner proof by induction can be closed.
> And therefore the outer proof by induction as well.
>
> Q.E.D.

Now there is a trick, instead of using circumscription:

0+x=x
y'+x=(x+y)'
Smallest such +

We can also use completion:

x+y=z <=> (x=0 & y=z) | EXIST(p):EXIST(q):(p'=x & p+y=q & q'=z)

This makes using + in the proofs much simpler.
One can prove that the circumscription + is
the same as the completion +, right? Yes or No?

Mostowski Collapse schrieb am Freitag, 27. Mai 2022 um 14:11:14 UTC+2:
> We did only make use of Pressburger Arithmetic in the
> previous lemma. Now lets do everything Even/Odd
> in Pressburger Arithmetic as well!
>
> We can use the previous lemma to show
> the key lemma of EvenNextOdd:
>
> LEMMA 76
> ALL(a):ALL(b):[~(a+a = (b+b)')]
> https://dcproof.com/EvenNextOdd.htm
>
> By the previous post lemma we have:
> EXIST(c):[a+c=b | a=b+c]
>
> Now proof by cases:
> Case 1: a+c=b, then the problem a+a = (b+b)'
> reduces to a+a=(a+c+a+c)', and hence a+a=a+a+(c+c)'
> using associativity and commutativity, which we
> need also to prove first via induction, and we need a
> cancellation lemma which we need also to prove
> first via induction, and we do get 0=(c+c)'
> which violates a peano axiom, so it is ~(a+a = (b+b)'.
>
> Case 2: a=b+c, then the problem a+a = (b+b)' reduces
> to (b+c+b+c)=(b+b)', and hence b+b+c+c=(b+b)',
> and hence c+c=1, using 1=0', this needs a new proof
> by induction, which will trivially show again that
> this is not possible, so it is ~(a+a = (b+b)' again.
>
> Q.E.D.
> Mostowski Collapse schrieb am Freitag, 27. Mai 2022 um 13:58:52 UTC+2:
> > Why not simply prove (the set n of natural numbers not
> > shown, you should get the idea without showing it):
> >
> > ALL(a):ALL(b):EXIST(c):[a+c=b | a=b+c]
> >
> > Proof: We use this definition of +,
> > 0+x=x
> > y'+x=(x+y)'
> > Smallest such +
> >
> > Now try proof by induction for the above theorem:
> > Base Case: a=0
> > We need to show: ALL(b):EXIST(c):[0+c=b | 0=b+c]
> > We can use c=b to satisfy the EXIST
> >
> > Inductive Step: a=n'
> > We need to show: ALL(b):EXIST(c):[n'+c=b | n'=b+c]
> >
> > We make sub proof by induction:
> > Base Case: b=0
> > We need to show: EXIST(c):[n'+c=0 | n'=0+c]
> > We can use c=n' to satisfy the EXIST
> >
> > Inductive Step: b=m'
> > We need to show: EXIST(c):[n'+c=m' | n'=m'+c]
> > Since n'+c = (n+c)', and since (n+c)'=m' is logical
> > equivalent to n+c=m. And since m'+c=(m+c)', and
> > since n'=(m+c)' is logical equivalent to n=m+c,
> > we need to show: EXIST(c):[n+c=m | n=m+c]
> > but this is just the outer induction hypothesis.
> >
> > So the inner proof by induction can be closed.
> > And therefore the outer proof by induction as well.
> >
> > Q.E.D.

On Friday, May 27, 2022 at 8:22:09 AM UTC-4, Mostowski Collapse wrote:
> Now there is a trick, instead of using circumscription:
> 0+x=x
> y'+x=(x+y)'
> Smallest such +

That's not a formal proof. Too much hand waving.

THIS is a formal proof: https://www.dcproof.com/ConstructAddFunction.htm (762 lines)

There, starting from Peano's Axioms (lines 1-6), I prove:

EXIST(add):[ALL(a):ALL(b):[a in n & b e n => add(a,b) in n]
& ALL(a):[a in n => add(a,0)=a]
& ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]]

where
n = the set of natural numbers
s = the usual successor function on n
add = the add function in prefix notation

Dan

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

I was conjecturing:

Definition 1: "circumscription"
0+x=x
y'+x=(x+y)'
Smallest such +

Definition 2: "completion"
x+y=z <=> (x=0 & y=z) | EXIST(p):EXIST(q):(p'=x & p+y=q & q'=z)

Definition 1 <=> Definition 2 in Peano
"One can prove that the circumscription + is
the same as the completion +, right?"

Yes or No?

Dan Christensen schrieb am Freitag, 27. Mai 2022 um 16:52:09 UTC+2:
> On Friday, May 27, 2022 at 8:22:09 AM UTC-4, Mostowski Collapse wrote:
> > Now there is a trick, instead of using circumscription:
> > 0+x=x
> > y'+x=(x+y)'
> > Smallest such +
> That's not a formal proof. Too much hand waving.
>
> THIS is a formal proof: https://www.dcproof.com/ConstructAddFunction.htm (762 lines)
>
> There, starting from Peano's Axioms (lines 1-6), I prove:
>
> EXIST(add):[ALL(a):ALL(b):[a in n & b e n => add(a,b) in n]
> & ALL(a):[a in n => add(a,0)=a]
> & ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]]
> where
> n = the set of natural numbers
> s = the usual successor function on n
> add = the add function in prefix notation
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Or more formally, the add from here:
https://www.dcproof.com/ConstructAddFunction.htm

And this add2 from here:
ALL(x):ALL(y):ALL(z):[x e n & y e n & z e n & =>
[add2(x,y)=z <=> (x=0 & y=z) |
EXIST(p):EXIST(q):(p e n & q e n & s(p)=x & add2(p,y)=q & s(q)=z)

One can prove:
ALL(x):ALL(y):ALL(z):[x e n & y e n & z e n & =>
[add(y,x)=z <=> add2(x,y)=z]]

Here is a proof sketch. Use induction on x first:
Base Case x=0:
we get add(y,0)=y and we get add2(0,y)=y so that
we have to show ALL(y):ALL(z):[y e n & z e n =>
[y=z <=> y=z]], which trivially holds.
Induction Step x=n':
we get add(y,n')=add(y,n)' and add2(n',y)=add2(n,y)' so
that we have to show ALL(y):ALL(z):[y e n & z e n =>
[add(y,n)'=z <=> add2(n,y)'=z]]

Now we can open sub induction on z.
Base Case z=0:
add(y,n)'=0 is false and add2(n,y)'=0 is false,
so what we would show is ALL(y):[y e n =>
[false <=> false ]], which trivially holds
Induction Step z=m':
add(y,n)'=m' is logically equivalent to add(y,n)=m
and add2(n,y)'=m' is logically equivalent to add2(n,y)=m
so what we would show is ALL(y):[y e n =>
[add(y,n)=m <=> add2(n,y)=m]],
which is true by the outer induction hypothesis.

So the inner proof by induction can be closed.
And therefore the outer proof by induction as well.

Q.E.D.

Mostowski Collapse schrieb am Freitag, 27. Mai 2022 um 18:21:45 UTC+2:
> I was conjecturing:
>
> Definition 1: "circumscription"
> 0+x=x
> y'+x=(x+y)'
> Smallest such +
> Definition 2: "completion"
> x+y=z <=> (x=0 & y=z) | EXIST(p):EXIST(q):(p'=x & p+y=q & q'=z)
> Definition 1 <=> Definition 2 in Peano
> "One can prove that the circumscription + is
> the same as the completion +, right?"
>
> Yes or No?
> Dan Christensen schrieb am Freitag, 27. Mai 2022 um 16:52:09 UTC+2:
> > On Friday, May 27, 2022 at 8:22:09 AM UTC-4, Mostowski Collapse wrote:
> > > Now there is a trick, instead of using circumscription:
> > > 0+x=x
> > > y'+x=(x+y)'
> > > Smallest such +
> > That's not a formal proof. Too much hand waving.
> >
> > THIS is a formal proof: https://www.dcproof.com/ConstructAddFunction.htm (762 lines)
> >
> > There, starting from Peano's Axioms (lines 1-6), I prove:
> >
> > EXIST(add):[ALL(a):ALL(b):[a in n & b e n => add(a,b) in n]
> > & ALL(a):[a in n => add(a,0)=a]
> > & ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]]
> > where
> > n = the set of natural numbers
> > s = the usual successor function on n
> > add = the add function in prefix notation
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

The bottom line is, we get Pressburger Arithmetic
by these simple axioms:
https://en.wikipedia.org/wiki/Presburger_arithmetic

1 Set(n)
Axiom
2 0 e n
Axiom
3 ALL(a):[a e n => s(a) e n]
Axiom
4 ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
Axiom
5 ALL(a):[a e n => ~s(a)=0]
Axiom
6 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Axiom
7 ALL(x):ALL(y):ALL(z):[x e n & y e n & z e n & =>
[x+y=z <=> (x=0 & y=z) |
EXIST(p):EXIST(q):(p e n & q e n & s(p)=x
& p+y=q & s(q)=z)
Axiom

And we could prove Even/Odd stuff from it, as
already sketched here:
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/tj2gnv1UBAAJ

Mostowski Collapse schrieb:
> Or more formally, the add from here:
> https://www.dcproof.com/ConstructAddFunction.htm
>
> And this add2 from here:
> ALL(x):ALL(y):ALL(z):[x e n & y e n & z e n & =>
> [add2(x,y)=z <=> (x=0 & y=z) |
> EXIST(p):EXIST(q):(p e n & q e n & s(p)=x & add2(p,y)=q & s(q)=z)
>
> One can prove:
> ALL(x):ALL(y):ALL(z):[x e n & y e n & z e n & =>
> [add(y,x)=z <=> add2(x,y)=z]]
>
> Here is a proof sketch. Use induction on x first:
> Base Case x=0:
> we get add(y,0)=y and we get add2(0,y)=y so that
> we have to show ALL(y):ALL(z):[y e n & z e n =>
> [y=z <=> y=z]], which trivially holds.
> Induction Step x=n':
> we get add(y,n')=add(y,n)' and add2(n',y)=add2(n,y)' so
> that we have to show ALL(y):ALL(z):[y e n & z e n =>
> [add(y,n)'=z <=> add2(n,y)'=z]]
>
> Now we can open sub induction on z.
> Base Case z=0:
> add(y,n)'=0 is false and add2(n,y)'=0 is false,
> so what we would show is ALL(y):[y e n =>
> [false <=> false ]], which trivially holds
> Induction Step z=m':
> add(y,n)'=m' is logically equivalent to add(y,n)=m
> and add2(n,y)'=m' is logically equivalent to add2(n,y)=m
> so what we would show is ALL(y):[y e n =>
> [add(y,n)=m <=> add2(n,y)=m]],
> which is true by the outer induction hypothesis.
>
> So the inner proof by induction can be closed.
> And therefore the outer proof by induction as well.
>
> Q.E.D.
>
>
> Mostowski Collapse schrieb am Freitag, 27. Mai 2022 um 18:21:45 UTC+2:
>> I was conjecturing:
>>
>> Definition 1: "circumscription"
>> 0+x=x
>> y'+x=(x+y)'
>> Smallest such +
>> Definition 2: "completion"
>> x+y=z <=> (x=0 & y=z) | EXIST(p):EXIST(q):(p'=x & p+y=q & q'=z)
>> Definition 1 <=> Definition 2 in Peano
>> "One can prove that the circumscription + is
>> the same as the completion +, right?"
>>
>> Yes or No?
>> Dan Christensen schrieb am Freitag, 27. Mai 2022 um 16:52:09 UTC+2:
>>> On Friday, May 27, 2022 at 8:22:09 AM UTC-4, Mostowski Collapse wrote:
>>>> Now there is a trick, instead of using circumscription:
>>>> 0+x=x
>>>> y'+x=(x+y)'
>>>> Smallest such +
>>> That's not a formal proof. Too much hand waving.
>>>
>>> THIS is a formal proof: https://www.dcproof.com/ConstructAddFunction.htm (762 lines)
>>>
>>> There, starting from Peano's Axioms (lines 1-6), I prove:
>>>
>>> EXIST(add):[ALL(a):ALL(b):[a in n & b e n => add(a,b) in n]
>>> & ALL(a):[a in n => add(a,0)=a]
>>> & ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]]
>>> where
>>> n = the set of natural numbers
>>> s = the usual successor function on n
>>> add = the add function in prefix notation
>>> Dan
>>>
>>> Download my DC Proof 2.0 freeware at http://www.dcproof.com
>>> Visit my Math Blog at http://www.dcproof.wordpress.com

Dan Christensen wrote:

> On Friday, May 27, 2022 at 8:22:09 AM UTC-4, Mostowski Collapse wrote:
>> Now there is a trick, instead of using circumscription:
>> 0+x=x y'+x=(x+y)'
>> Smallest such +
>
> That's not a formal proof. Too much hand waving.

Ukrainian POW says his commander left them 'for a meeting' and never came
back https://www.bitchute.com/video/ru6ZCM08YuGN/