On Wednesday, May 25, 2022 at 11:00:28 AM UTC-4, Mostowski Collapse wrote:
> This axiom is dubious:
>
> 9 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*(b-c)=a*b-a*c]
> Axiom
>

Easy fix. See line 14 of revised proof at https://dcproof.com/EvenNextOdd.htm

Thanks for bringing this to my attention.

Dan

Its still running outside of n. Here:

10 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a-b=c <=> a=c+b]]
Axiom

Thats cause why it goes out of n, i.e. ~(a-b e n) for certain situations.

Your stuff would be less ad-hoc, if you would derive it from Peano in the first place.

Dan Christensen schrieb am Mittwoch, 25. Mai 2022 um 19:30:10 UTC+2:
> On Wednesday, May 25, 2022 at 11:00:28 AM UTC-4, Mostowski Collapse wrote:
> > This axiom is dubious:
> >
> > 9 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*(b-c)=a*b-a*c]
> > Axiom
> >
> Easy fix. See line 14 of revised proof at https://dcproof.com/EvenNextOdd.htm
>
> Thanks for bringing this to my attention.
>
> Dan

Take a = 1, b = 3. a = c + b will be always false for any c e N.

But how do you want to make 1-3 = c for all c e N false.

This works only if ~(1 - 3 e N).

Mostowski Collapse schrieb am Mittwoch, 25. Mai 2022 um 20:51:42 UTC+2:
> Its still running outside of n. Here:
>
> 10 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a-b=c <=> a=c+b]]
> Axiom
>
> Thats cause why it goes out of n, i.e. ~(a-b e n) for certain situations.
>
> Your stuff would be less ad-hoc, if you would derive it from Peano in the first place.
> Dan Christensen schrieb am Mittwoch, 25. Mai 2022 um 19:30:10 UTC+2:
> > On Wednesday, May 25, 2022 at 11:00:28 AM UTC-4, Mostowski Collapse wrote:
> > > This axiom is dubious:
> > >
> > > 9 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*(b-c)=a*b-a*c]
> > > Axiom
> > >
> > Easy fix. See line 14 of revised proof at https://dcproof.com/EvenNextOdd.htm
> >
> > Thanks for bringing this to my attention.
> >
> > Dan

On Wednesday, May 25, 2022 at 2:51:42 PM UTC-4, Mostowski Collapse wrote:
> Its still running outside of n. Here:
>
> 10 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a-b=c <=> a=c+b]]
> Axiom
>

Also an easy fix. The biconditional turns out to be unnecessary. Use instead:

10. ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a=c+b => a-b=c ]]
Axiom

Will update proof in the next day or so.

Dan

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