Here is a much shorter proof, I playing around
with the maps to symbol |-> , just take it as a ternary
relation written as _,_ |-> _ , and alternative to your add.

Now dont define add as the smallest fixpoint, only
as a fixpoint should be enough. So do something
else than boring Dan Christensen:

x,y |-> z <=> (y=0 & z=x) | EXIST(u):EXIST(v):(y=s(u) & x,u |-> v & z=s(v))

Now prove:

Seriality: ALL(x):ALL(y):EXIST(z):x,y |-> z
Proof by induction on y.

Functionality: ALL(x):ALL(y):ALL(z):ALL(t):(x,y |-> z & x,y |-> t => z = t)
Proof by induction on y.

Mostowski Collapse schrieb am Samstag, 30. April 2022 um 23:38:40 UTC+2:
> Corr.: Typo
>
> > The problem is you have no Peano induction schema:
> >
> > P(0) & ALL(x):[P(x) => P(x+1)]
> > ------------------------------------------------
> > ALL(y):P(y)
>
> Sorry, its already late...
> Mostowski Collapse schrieb am Samstag, 30. April 2022 um 23:37:18 UTC+2:
> > Doesn't make any sense to prove existence of add/3 with 762 proof lines.
> > The problem is you have now Peano induction schema:
> >
> > P(0) & ALL(x):[P(x+1) => P(x)]
> > ------------------------------------------------
> > ALL(y):P(y)
> >
> > You can prove it much shorter if you have such a schema. Thats
> > usually what they teach in University.
> >
> > Dan Christensen schrieb am Samstag, 30. April 2022 um 22:39:44 UTC+2:
> > > This is how it is done: https://dcproof.com/ConstructAddFunction.htm

Now since we have proved:

ALL(x):ALL(y):EXISTUNIQUE(z):x,y |-> z

We are licensed to define, without harm:

add(x,y) = z <=> x,y |-> z

And some very easy proofs reveale:

add(x,0,x)
add(x,s(u))=s(add(x,u))

Universal quantifiers were omitted in some places,
to render the post more readable and shorter.

Mostowski Collapse schrieb am Sonntag, 1. Mai 2022 um 00:40:09 UTC+2:
> Here is a much shorter proof, I playing around
> with the maps to symbol |-> , just take it as a ternary
> relation written as _,_ |-> _ , and alternative to your add.
>
> Now dont define add as the smallest fixpoint, only
> as a fixpoint should be enough. So do something
> else than boring Dan Christensen:
>
> x,y |-> z <=> (y=0 & z=x) | EXIST(u):EXIST(v):(y=s(u) & x,u |-> v & z=s(v))
>
> Now prove:
>
> Seriality: ALL(x):ALL(y):EXIST(z):x,y |-> z
> Proof by induction on y.
>
> Functionality: ALL(x):ALL(y):ALL(z):ALL(t):(x,y |-> z & x,y |-> t => z = t)
> Proof by induction on y.
> Mostowski Collapse schrieb am Samstag, 30. April 2022 um 23:38:40 UTC+2:
> > Corr.: Typo
> >
> > > The problem is you have no Peano induction schema:
> > >
> > > P(0) & ALL(x):[P(x) => P(x+1)]
> > > ------------------------------------------------
> > > ALL(y):P(y)
> >
> > Sorry, its already late...
> > Mostowski Collapse schrieb am Samstag, 30. April 2022 um 23:37:18 UTC+2:
> > > Doesn't make any sense to prove existence of add/3 with 762 proof lines.
> > > The problem is you have now Peano induction schema:
> > >
> > > P(0) & ALL(x):[P(x+1) => P(x)]
> > > ------------------------------------------------
> > > ALL(y):P(y)
> > >
> > > You can prove it much shorter if you have such a schema. Thats
> > > usually what they teach in University.
> > >
> > > Dan Christensen schrieb am Samstag, 30. April 2022 um 22:39:44 UTC+2:
> > > > This is how it is done: https://dcproof.com/ConstructAddFunction.htm

Corr. Typo

add(x,0,x)
add(x,s(u))=s(add(x,u))

Mostowski Collapse schrieb am Sonntag, 1. Mai 2022 um 00:51:12 UTC+2:
> Now since we have proved:
>
> ALL(x):ALL(y):EXISTUNIQUE(z):x,y |-> z
>
> We are licensed to define, without harm:
>
> add(x,y) = z <=> x,y |-> z
>
> And some very easy proofs reveale:
>
> add(x,0,x)
> add(x,s(u))=s(add(x,u))
>
> Universal quantifiers were omitted in some places,
> to render the post more readable and shorter.
> Mostowski Collapse schrieb am Sonntag, 1. Mai 2022 um 00:40:09 UTC+2:
> > Here is a much shorter proof, I playing around
> > with the maps to symbol |-> , just take it as a ternary
> > relation written as _,_ |-> _ , and alternative to your add.
> >
> > Now dont define add as the smallest fixpoint, only
> > as a fixpoint should be enough. So do something
> > else than boring Dan Christensen:
> >
> > x,y |-> z <=> (y=0 & z=x) | EXIST(u):EXIST(v):(y=s(u) & x,u |-> v & z=s(v))
> >
> > Now prove:
> >
> > Seriality: ALL(x):ALL(y):EXIST(z):x,y |-> z
> > Proof by induction on y.
> >
> > Functionality: ALL(x):ALL(y):ALL(z):ALL(t):(x,y |-> z & x,y |-> t => z = t)
> > Proof by induction on y.
> > Mostowski Collapse schrieb am Samstag, 30. April 2022 um 23:38:40 UTC+2:
> > > Corr.: Typo
> > >
> > > > The problem is you have no Peano induction schema:
> > > >
> > > > P(0) & ALL(x):[P(x) => P(x+1)]
> > > > ------------------------------------------------
> > > > ALL(y):P(y)
> > >
> > > Sorry, its already late...
> > > Mostowski Collapse schrieb am Samstag, 30. April 2022 um 23:37:18 UTC+2:
> > > > Doesn't make any sense to prove existence of add/3 with 762 proof lines.
> > > > The problem is you have now Peano induction schema:
> > > >
> > > > P(0) & ALL(x):[P(x+1) => P(x)]
> > > > ------------------------------------------------
> > > > ALL(y):P(y)
> > > >
> > > > You can prove it much shorter if you have such a schema. Thats
> > > > usually what they teach in University.
> > > >
> > > > Dan Christensen schrieb am Samstag, 30. April 2022 um 22:39:44 UTC+2:
> > > > > This is how it is done: https://dcproof.com/ConstructAddFunction.htm

But we must point out that there are more problems.
Doesn't make any sense to prove existence of add/3 with 762 proof lines.

Dan Christensen schrieb am Samstag, 30. April 2022 um 22:39:44 UTC+2:
> This is how it is done: https://dcproof.com/ConstructAddFunction.htm

And where is a proof of EXIST(n):Peano(n) ? You don't have a powerful
set theory, like ZFC would be, that could prove that. In ZFC you
could do such a construction, by means of the Axiom of Infinity (AOI).

You are just a crank. You don't understand that mathematics works:

- definition
- lemma
- theorem

This building block is hardly used:

- axiom

Now you have axioms for Peano, and don't prove EXIST(n):Peano(n).

A variation of the definition discipline, found in many modern
theorem provers, reads as follows:

- meta /* provided by the tool */
- def_dom /* example use <n,0,s> */
- def_ind /* example use x,y |-> z */
- def_rec /* example use add(x,y) = z */
- lemma
- theorem

This building block is then hardly used:

- axiom

The meta theory assures that the domains from def_dom, inductive
predicate definitions from def_ind and recursive functions definitions
from def_rec are all well . The meta theory and logic framework assures

things like EXIST(n):Peano(n), similar like in ZFC via Axiom of
Infinity (AOI). You can check out Coq, Isabelle/HOL, etc.. how its
done. def_rec, def_ind and def_dom are then setup so that

they are more reasoning friendly, to better support lemma and
theorem construction. Ultimately we want to prove some theorems
and not only construct some domains, predicates and functions.

Although the construction of the basic things in itself could be also an end.

Mostowski Collapse schrieb am Sonntag, 1. Mai 2022 um 08:24:00 UTC+2:
> But we must point out that there are more problems.
> Doesn't make any sense to prove existence of add/3 with 762 proof lines.
> Dan Christensen schrieb am Samstag, 30. April 2022 um 22:39:44 UTC+2:
> > This is how it is done: https://dcproof.com/ConstructAddFunction.htm
> And where is a proof of EXIST(n):Peano(n) ? You don't have a powerful
> set theory, like ZFC would be, that could prove that. In ZFC you
> could do such a construction, by means of the Axiom of Infinity (AOI).
>
> You are just a crank. You don't understand that mathematics works:
>
> - definition
> - lemma
> - theorem
>
> This building block is hardly used:
>
> - axiom
>
> Now you have axioms for Peano, and don't prove EXIST(n):Peano(n).

Dan Christensen is currently in some UNDEFINED
delirium. He says this is Wonky:

Dan Christensen schrieb am Dienstag, 10. Mai 2022 um 01:44:05 UTC+2:
> Wonky result:
> 11. ALL(a):[~a in n => ~Even(a)]
> Conclusion, 2
https://groups.google.com/g/sci.logic/c/gV50jEU6fvQ/m/jRRRllUEAgAJ

But every sane mathematician will agree:

~(a e {0,1,2,3,...}) => ~(a e {0,2,4,...})

LoL

On Tuesday, May 10, 2022 at 3:17:38 AM UTC-4, Mostowski Collapse wrote:
> Dan Christensen is currently in some UNDEFINED
> delirium. He says this is Wonky:
>
> Dan Christensen schrieb am Dienstag, 10. Mai 2022 um 01:44:05 UTC+2:
> > Wonky result:
> > 11. ALL(a):[~a in n => ~Even(a)]
> > Conclusion, 2

This is the wonky result of Jan Burse's wonky definition of Even( ). A cautionary tale that you really do need to restrict quantifiers -- to the set of natural numbers in this case.

>
> But every sane mathematician will agree:
>
> ~(a e {0,1,2,3,...}) => ~(a e {0,2,4,...})

A problem potentially arises when you try to define a predicate Even(x) (means: x is even) and ~Even(x) means x is odd. As you would expect, if you are are talking only about the natural numbers should probably restrict quantifiers to the natural numbers. But not Jan Burse. He wants to be able to make inferences about the evenness of every object in the universe -- his "dark elements."

Here is the standard way to define Even on the natural numbers:

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

Poor Jan Burse gets in backwards, doesn't explicitly restrict the first quantifier and gets into trouble. He writes:

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

It may look OK to his untrained eye, but it does lead to some major wonkiness with ALL(a):[~a in N => ~Even(a)]. Does ~Even(x) mean x is odd? Not necessarily, according to Jan Burse.

This confusion can be easily avoided by starting with a proper definition, one in which each quantifier is explicitly restricted to the set of natural numbers. Jan Burse would rather die.

Dan

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

You are crazy, this definition:
ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]

You can even write it as:
ALL(a):[Even(a) <=> EXIST(b):[b in N & a=2*b]]

Gives nothing else than Even = {0, 2, 4, …}. What should it
give else, so that ALL(a):[~a in n => ~Even(a)] would not be valid?

Dan Christensen schrieb am Dienstag, 10. Mai 2022 um 18:36:09 UTC+2:
> On Tuesday, May 10, 2022 at 3:17:38 AM UTC-4, Mostowski Collapse wrote:
> > Dan Christensen is currently in some UNDEFINED
> > delirium. He says this is Wonky:
> >
> > Dan Christensen schrieb am Dienstag, 10. Mai 2022 um 01:44:05 UTC+2:
> > > Wonky result:
> > > 11. ALL(a):[~a in n => ~Even(a)]
> > > Conclusion, 2
> This is the wonky result of Jan Burse's wonky definition of Even( ). A cautionary tale that you really do need to restrict quantifiers -- to the set of natural numbers in this case.
> >
> > But every sane mathematician will agree:
> >
> > ~(a e {0,1,2,3,...}) => ~(a e {0,2,4,...})
> A problem potentially arises when you try to define a predicate Even(x) (means: x is even) and ~Even(x) means x is odd. As you would expect, if you are are talking only about the natural numbers should probably restrict quantifiers to the natural numbers. But not Jan Burse. He wants to be able to make inferences about the evenness of every object in the universe -- his "dark elements."
>
> Here is the standard way to define Even on the natural numbers:
>
> ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
>
> Poor Jan Burse gets in backwards, doesn't explicitly restrict the first quantifier and gets into trouble. He writes:
>
> ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
>
> It may look OK to his untrained eye, but it does lead to some major wonkiness with ALL(a):[~a in N => ~Even(a)]. Does ~Even(x) mean x is odd? Not necessarily, according to Jan Burse.
>
> This confusion can be easily avoided by starting with a proper definition, one in which each quantifier is explicitly restricted to the set of natural numbers. Jan Burse would rather die.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Or do you see some b e N, so that this expression:

a = 2*b

gives something else than what is listed Even = {0, 2, 4, …}.

BTW: We can now establish a third form of defining Even and Odd,
also mentioned in Euclid, and the most useful for math:

Case 3:
ALL(a):[Even(a) <=> EXIST(b):[b in N & a=2*b]]
ALL(a):[Odd(a) <=> EXIST(b):[b in N & a=2*b+1]]

Mostowski Collapse schrieb am Dienstag, 10. Mai 2022 um 18:40:43 UTC+2:
> You are crazy, this definition:
> ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
> You can even write it as:
> ALL(a):[Even(a) <=> EXIST(b):[b in N & a=2*b]]
>
> Gives nothing else than Even = {0, 2, 4, …}. What should it
> give else, so that ALL(a):[~a in n => ~Even(a)] would not be valid?
> Dan Christensen schrieb am Dienstag, 10. Mai 2022 um 18:36:09 UTC+2:
> > On Tuesday, May 10, 2022 at 3:17:38 AM UTC-4, Mostowski Collapse wrote:
> > > Dan Christensen is currently in some UNDEFINED
> > > delirium. He says this is Wonky:
> > >
> > > Dan Christensen schrieb am Dienstag, 10. Mai 2022 um 01:44:05 UTC+2:
> > > > Wonky result:
> > > > 11. ALL(a):[~a in n => ~Even(a)]
> > > > Conclusion, 2
> > This is the wonky result of Jan Burse's wonky definition of Even( ). A cautionary tale that you really do need to restrict quantifiers -- to the set of natural numbers in this case.
> > >
> > > But every sane mathematician will agree:
> > >
> > > ~(a e {0,1,2,3,...}) => ~(a e {0,2,4,...})
> > A problem potentially arises when you try to define a predicate Even(x) (means: x is even) and ~Even(x) means x is odd. As you would expect, if you are are talking only about the natural numbers should probably restrict quantifiers to the natural numbers. But not Jan Burse. He wants to be able to make inferences about the evenness of every object in the universe -- his "dark elements."
> >
> > Here is the standard way to define Even on the natural numbers:
> >
> > ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> >
> > Poor Jan Burse gets in backwards, doesn't explicitly restrict the first quantifier and gets into trouble. He writes:
> >
> > ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
> >
> > It may look OK to his untrained eye, but it does lead to some major wonkiness with ALL(a):[~a in N => ~Even(a)]. Does ~Even(x) mean x is odd? Not necessarily, according to Jan Burse.
> >
> > This confusion can be easily avoided by starting with a proper definition, one in which each quantifier is explicitly restricted to the set of natural numbers. Jan Burse would rather die.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Case 3 is equivalent to Case 2.
Case 3 is not equivalent to Case 1.

Since Euclid mentioned Case 2 and Case 3, I guess Case 1 is a no go.
But the main argument against Case 1 is that it is a non-well defined
definition, whereas Case 2 and Case 3 are both well defined.

https://en.m.wikipedia.org/wiki/Well-defined_expression

Mostowski Collapse schrieb am Dienstag, 10. Mai 2022 um 18:48:30 UTC+2:
> Or do you see some b e N, so that this expression:
>
> a = 2*b
>
> gives something else than what is listed Even = {0, 2, 4, …}.
>
> BTW: We can now establish a third form of defining Even and Odd,
> also mentioned in Euclid, and the most useful for math:
>
> Case 3:
> ALL(a):[Even(a) <=> EXIST(b):[b in N & a=2*b]]
> ALL(a):[Odd(a) <=> EXIST(b):[b in N & a=2*b+1]]
> Mostowski Collapse schrieb am Dienstag, 10. Mai 2022 um 18:40:43 UTC+2:
> > You are crazy, this definition:
> > ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
> > You can even write it as:
> > ALL(a):[Even(a) <=> EXIST(b):[b in N & a=2*b]]
> >
> > Gives nothing else than Even = {0, 2, 4, …}. What should it
> > give else, so that ALL(a):[~a in n => ~Even(a)] would not be valid?
> > Dan Christensen schrieb am Dienstag, 10. Mai 2022 um 18:36:09 UTC+2:
> > > On Tuesday, May 10, 2022 at 3:17:38 AM UTC-4, Mostowski Collapse wrote:
> > > > Dan Christensen is currently in some UNDEFINED
> > > > delirium. He says this is Wonky:
> > > >
> > > > Dan Christensen schrieb am Dienstag, 10. Mai 2022 um 01:44:05 UTC+2:
> > > > > Wonky result:
> > > > > 11. ALL(a):[~a in n => ~Even(a)]
> > > > > Conclusion, 2
> > > This is the wonky result of Jan Burse's wonky definition of Even( ). A cautionary tale that you really do need to restrict quantifiers -- to the set of natural numbers in this case.
> > > >
> > > > But every sane mathematician will agree:
> > > >
> > > > ~(a e {0,1,2,3,...}) => ~(a e {0,2,4,...})
> > > A problem potentially arises when you try to define a predicate Even(x) (means: x is even) and ~Even(x) means x is odd. As you would expect, if you are are talking only about the natural numbers should probably restrict quantifiers to the natural numbers. But not Jan Burse. He wants to be able to make inferences about the evenness of every object in the universe -- his "dark elements."
> > >
> > > Here is the standard way to define Even on the natural numbers:
> > >
> > > ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> > >
> > > Poor Jan Burse gets in backwards, doesn't explicitly restrict the first quantifier and gets into trouble. He writes:
> > >
> > > ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
> > >
> > > It may look OK to his untrained eye, but it does lead to some major wonkiness with ALL(a):[~a in N => ~Even(a)]. Does ~Even(x) mean x is odd? Not necessarily, according to Jan Burse.
> > >
> > > This confusion can be easily avoided by starting with a proper definition, one in which each quantifier is explicitly restricted to the set of natural numbers. Jan Burse would rather die.
> > > 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:

>> > 11. ALL(a):[~a in n => ~Even(a)]
>> > Conclusion, 2
>
> This is the wonky result of Jan Burse's wonky definition of Even( ). A
> cautionary tale that you really do need to restrict quantifiers -- to the
> set of natural numbers in this case.

you two nazis sure??

Ukraine’s ‘senseless PR action’ at Snake Island led to heavy losses – Russia
Kiev lost 30 drones, 14 aircraft and 3 ships in a ‘senseless PR action’ to retake island, the Russian military says
https://www.rt.com/russia/555268-snake-island-pr-military/

Ukraine turns off Europe-bound gas
Kiev cites ‘force majeure’ to halt a third of Russian transited gas flow to Europe, while Gazprom says there have been no issues that would justify the move
https://www.rt.com/russia/555265-gazprom-gas-ukraine-europe/

Millions of UK homes face no heat this winter, power chief warns
https://www.rt.com/news/555258-uk-energy-heating-cost/

British TV censored Zelensky Nazi pic – Russian diplomat
Sky News slot ended after Dmitry Polyansky showed an image of a Nazi symbol posted by Ukraine’s leader
https://www.rt.com/russia/555225-russian-diplomat-sky-news/

UN Has 'Credible Information' on Ukrainian Troops' Torture of Russian PoWs
https://sputniknews.com/20220510/un-has-credible-information-on-ukrainian-troops-torture-of-russian-pows-1095406731.html
"We have received credible information of torture, ill-treatment and incommunicado detention by [the] Ukrainian Armed Forces of prisoners of war belonging to the Russian Armed Forces and affiliated armed groups", Bogner said in a press briefing on Tuesday.

WATCH Ukrainian Neo-Nazis March to Celebrate Anniversary of UPA
https://sputniknews.com/20220510/watch-ukrainian-neo-nazis-march-to-celebrate-anniversary-of-upa-1095393516.html
https://videon.img.ria.ru/Out/Flv/20220509/2022_05_09_DONBASSGENOCIDE9051_kf5tkl44.fba.mp4

On Tuesday, May 10, 2022 at 4:38:58 PM UTC-4, Colt Hiyama wrote:
> Dan Christensen wrote:
>
> >> > 11. ALL(a):[~a in n => ~Even(a)]
> >> > Conclusion, 2
> >
> > This is the wonky result of Jan Burse's wonky definition of Even( ). A
> > cautionary tale that you really do need to restrict quantifiers -- to the
> > set of natural numbers in this case.
> you two nazis sure??
>

Remember:

WAR OF AGREESION = NAZI

That's you, Nazi boy! Their denials didn't help the original Nazis. Yours won't help you. Also remember to keep that length of rope handy for when the Nazi hunters track you down.

Dan Christensen wrote:

>> > the set of natural numbers in this case.
>> you two nazis sure??
>
> Remember: WAR OF AGREESION = NAZI

this inbreed nazi still committing double negation. _Aggression_ already
is included the term _war_, you know nothing idiot.

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

Mostowski Collapse schrieb am Dienstag, 24. Mai 2022 um 23:23:57 UTC+2:
> 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

On Wednesday, May 11, 2022 at 4:03:39 PM UTC-4, Cecil Nitta wrote:
> Dan Christensen wrote:
>
> >> > the set of natural numbers in this case.
> >> you two nazis sure??
> >
> > Remember: WAR OF AGREESION = NAZI
> this inbreed nazi still committing double negation.

Tell it to the judges, Nazi boy.

See the Nuremberg judgement. Or has your boss has censored that, too? Must make him nervous.

The problem is from here:
https://artofproblemsolving.com/wiki/index.php/2017_AMC_12A_Problems#Problem_7

I guess its even not provable so easy from your Peano
Axioms. Course of value induction would be more handy.
But maybe you can map it to ordinary mathematical induction.

By proving Q(a) <=> ALL(b):[b < a => P(b)], via ordinary mathematical
induction. One gets from the ordinary mathematical induction
schema which reads:

Q(0) ALL(c):[Q(c) => Q(c+1)]
----------------------------------------------------
ALL(d):Q(d)

The following new schema. For observe that Q(0) is
vacusly true, since there is no b < 0. So we have to
only look what Q(c) => Q(c+1) says. But Q(c) says

ALL(b):[b < c => P(b)] and Q(c+1) says this here
ALL(b):[b < c+1 => P(b)]. The later is equivalent
to ALL(b)[b < c => P(b)] and P(c). But the ALL(b):[b < c=> P(b)]

in the conclusion Q(c+1) is redundant. Also a further
consideration tells that ALL(d):Q(d) implies ALL(e):P(e).
So basically we have a new schema:

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

Course of value induction. This could help
in proving that we have:

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

Mostowski Collapse schrieb am Dienstag, 24. Mai 2022 um 23:28:10 UTC+2:
> 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
> Mostowski Collapse schrieb am Dienstag, 24. Mai 2022 um 23:23:57 UTC+2:
> > 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

Dan Christensen wrote:

> On Wednesday, May 11, 2022 at 4:03:39 PM UTC-4, Cecil Nitta wrote:
>> Dan Christensen wrote:
>>
>> >> > the set of natural numbers in this case.
>> >> you two nazis sure??
>> >
>> > Remember: WAR OF AGREESION = NAZI
>> this inbreed nazi still committing double negation.

British mercenaries in Ukraine face death penalty
https://www.rt.com/news/556221-mercenaries-ukraine-death-penalty/
Viktor Gavrilov, the judiciary spokesman, revealed that an investigation
into the activities of “a group of foreign mercenaries” who allegedly
“took part in the preparation and implementation of hostilities against
the DPR,” had been completed and a criminal case had been “fully formed.”

Three suspected mercenaries from Britain and Morocco, who joined the
Ukrainian military and were later captured by the forces of the Donetsk
People’s Republic (DPR), could be facing the death penalty there, the
republic’s General Prosecutor’s Office said on Friday.

Mostowski Collapse wrote:

> The problem is from here:

amazing, you guys. An armed police of 5000 in the fucking *fake_money*
shithole country of switzarland. To "protect" the oligarchs "partners" to
the retard dementia hit claus schwab (anal), all "climate warming"
oriented, traveling in private jets.

here's another nazi oligarch, trying to escape justice.

Ex-president attempts to leave Ukraine
https://www.rt.com/russia/556224-ukraine-poroshenko-poland-border/

Former president of Ukraine Petro Poroshenko tried to cross the border
into Poland on Friday, Ukrainian media reported citing the state customs
service sources. Volodymyr Zelensky’s predecessor is currently facing
treason charges in Kiev.

On Tuesday, May 10, 2022 at 12:40:43 PM UTC-4, Mostowski Collapse wrote:
> You are crazy, this definition:
> ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
> You can even write it as:
> ALL(a):[Even(a) <=> EXIST(b):[b in N & a=2*b]]
>

You can play around with this wonky definition and get all the wonky results you want. Not interested, Jan Burse.

Dan

You should be able to prove it from Presburger arithmetic
only, thats quite easy, I sketched it already here:
https://groups.google.com/g/sci.logic/c/UABVyIeAlxc/m/O_kQbK6PAQAJ

Presburger arithmetic is Peano induction
plus addition. See here:

x + 0 = x
x + (y + 1) = (x + y) + 1
https://en.wikipedia.org/wiki/Presburger_arithmetic

No need to introduce multiplication which is not necessarely
multiplication on the natural numbers. Just use a+a in place of 2*a.

On the German Wikipedia of Presburger arithmetic,
they make Even as an example for Presburger arithmetic:

„ x ist gerade“ durch G ( x ) :⇔ ∃ z : z + z = x
https://de.wikipedia.org/wiki/Presburger-Arithmetik

Dan Christensen schrieb am Samstag, 28. Mai 2022 um 04:44:26 UTC+2:
> On Tuesday, May 10, 2022 at 12:40:43 PM UTC-4, Mostowski Collapse wrote:
> > You are crazy, this definition:
> > ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
> > You can even write it as:
> > ALL(a):[Even(a) <=> EXIST(b):[b in N & a=2*b]]
> >
> You can play around with this wonky definition and get all the wonky results you want. Not interested, Jan Burse.
>
> Dan

See my reply yesterday to your identical posting elsewhere.

Dan

On Saturday, May 28, 2022 at 5:52:32 AM UTC-4, Mostowski Collapse wrote:
> You should be able to prove it from Presburger arithmetic
> only, thats quite easy, I sketched it already here:
> https://groups.google.com/g/sci.logic/c/UABVyIeAlxc/m/O_kQbK6PAQAJ
>
> Presburger arithmetic is Peano induction
> plus addition. See here: ...

[snip]

How would you prove:

ALL(a):[a e n => Even(a) v Even(3*a+1)]
https://www.tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=ARI&File=ARI598=1.p

Is your EvenNextOdd.html strong enough?

Dan Christensen schrieb am Samstag, 28. Mai 2022 um 17:16:54 UTC+2:
> See my reply yesterday to your identical posting elsewhere.
>
> Dan
> On Saturday, May 28, 2022 at 5:52:32 AM UTC-4, Mostowski Collapse wrote:
> > You should be able to prove it from Presburger arithmetic
> > only, thats quite easy, I sketched it already here:
> > https://groups.google.com/g/sci.logic/c/UABVyIeAlxc/m/O_kQbK6PAQAJ
> >
> > Presburger arithmetic is Peano induction
> > plus addition. See here: ...
>
> [snip]

You only want to glorify your dislexia. But I see an AND
here and not an IF, from the website cuemath.com:

„The even natural numbers are the numbers that are
even, exactly divisible by 2, and belong to the set N. So
the set of even natural numbers is {2,4,6,8,...}.“
https://www.cuemath.com/numbers/natural-numbers/

So this is wrong: Dan O Matiks EvenNextOdd
ALL(a):[a e n => [Even(a) <=> EXISTS(b):[b e n & 2*b = a]]]

And this is correct: Common Sense, gives {2,4,6,8,...}.
ALL(a):[Even(a) <=> a e n & EXISTS(b):[b e n & 2*b = a]]

Dan Christensen schrieb am Samstag, 28. Mai 2022 um 18:16:54 UTC+3:
> See my reply yesterday to your identical posting elsewhere.
>
> Dan
> On Saturday, May 28, 2022 at 5:52:32 AM UTC-4, Mostowski Collapse wrote:
> > You should be able to prove it from Presburger arithmetic
> > only, thats quite easy, I sketched it already here:
> > https://groups.google.com/g/sci.logic/c/UABVyIeAlxc/m/O_kQbK6PAQAJ
> >
> > Presburger arithmetic is Peano induction
> > plus addition. See here: ...
>
> [snip]

Mostowski Collapse wrote:

> You only want to glorify your dislexia. But I see an AND here and not an
> IF, from the website cuemath.com:

absolutely, this nazi oriented individual, named Dan Christensen, is
deleting the evidences and the proofs proving him wrong.
> And this is correct: Common Sense, gives {2,4,6,8,...}. ALL(a):[Even(a)
> <=> a e n & EXISTS(b):[b e n & 2*b = a]]
>
> Dan Christensen schrieb am Samstag, 28. Mai 2022 um 18:16:54 UTC+3: