Proving that addition in $mathbbN$ is associative and commutative The Next CEO of Stack OverflowProving mathematical induction with arbitrary base using (weak) inductionAre these two definitions of the natural numbers equivalent?Why this proof is incorrect?(Proof-verification) Proof that multiplication of natural numbers is commutativeIs the induction principle still viable if the induction skips over, or does not hold for some numbers?Mathematical induction from $n=1$Double inducton: Addition is commutativeProve addition is commutative using axioms, definitions, and inductionProving the commutative law for 1-based $BbbN$Proving the addition law for equality, eg. $+$ is compatible with $=$ on $mathbbN$
Return the Closest Prime Number
Is micro rebar a better way to reinforce concrete than rebar?
Would this house-rule that treats advantage as a +1 to the roll instead (and disadvantage as -1) and allows them to stack be balanced?
What happens if you roll doubles 3 times then land on "Go to jail?"
How to count occurrences of text in a file?
If Nick Fury and Coulson already knew about aliens (Kree and Skrull) why did they wait until Thor's appearance to start making weapons?
How do I avoid eval and parse?
Example of a Mathematician/Physicist whose Other Publications during their PhD eclipsed their PhD Thesis
Why am I allowed to create multiple unique pointers from a single object?
Sending manuscript to multiple publishers
How did the Bene Gesserit know how to make a Kwisatz Haderach?
Elegant way to replace substring in a regex with optional groups in Python?
How do we know the LHC results are robust?
Why has the US not been more assertive in confronting Russia in recent years?
Why does standard notation not preserve intervals (visually)
Would a galaxy be visible from outside, but nearby?
How did people program for Consoles with multiple CPUs?
What's the best way to handle refactoring a big file?
What benefits would be gained by using human laborers instead of drones in deep sea mining?
Why do remote companies require working in the US?
What flight has the highest ratio of time difference to flight time?
Written every which way
How does the mv command work with external drives?
Is "for causing autism in X" grammatical?
Proving that addition in $mathbbN$ is associative and commutative
The Next CEO of Stack OverflowProving mathematical induction with arbitrary base using (weak) inductionAre these two definitions of the natural numbers equivalent?Why this proof is incorrect?(Proof-verification) Proof that multiplication of natural numbers is commutativeIs the induction principle still viable if the induction skips over, or does not hold for some numbers?Mathematical induction from $n=1$Double inducton: Addition is commutativeProve addition is commutative using axioms, definitions, and inductionProving the commutative law for 1-based $BbbN$Proving the addition law for equality, eg. $+$ is compatible with $=$ on $mathbbN$
$begingroup$
I would like to prove the associative and commutative property of the natural numbers by using Peanos axioms only. Did I justify every step in my proofs correctly?
Definition. $forall n,m in mathbbN , n+m = underbraces(s(...s_textm (n)...)) = s^[m](n) $ where $s(n)$ is the successor function.
a) $forall n,m,k in mathbbN , n+(m+k)=(n+m)+k$
Proof: Let $SsubsetmathbbN$ be the set for which a) holds.
- Case $k=1 , forall n,m in mathbbN$
$n +(m+1) =$ (definition of $+$) $ = s^[m+1](n) = (*) = s(s^[m](n)) = s(m + n) = (m+n) + 1$
I am not sure how to justify $(*)$. I have:
$s^[m+1](n) = underbraces(s(....s_textm(underbraces_text1(n))...))=underbraces_text1(underbraces(s(...s_textm(n)...)))=s(s^[m](n))$
The composition of functions is associative but am I implicitly assuming the commutative property of the natural numbers i.e. $m+1 = 1+m$ ?
- Let $kin S$ be arbitrary $implies n+(m+k)=(n+m)+k$
$n+(m+(k+1))= $ (From 1. for $m+(k+1)$) = $n +((m+k)+1) = $ (From 1. for $n+(t+1)$ and $t=m+kinmathbbN$) $=(n+t)+1 = (n + (m+k))+1 = (kin S) = ((n+m)+k)+1=s^[k](n+m)+1=s^[k+1](n+m) = (n+m)+(k+1)$
From 1. we have $1in S$ and from 2. we have $kin S implies s(k)=k+1in S$ and by the axiom of mathematical induction it follows that $S = mathbbN$.
b) $forall n,m in mathbbN , n+m=m+n$
Proof:
First we will show that $s(n) = s^[n](1)$
$n=1 implies s(1) = 1+1 = s^[1](1)$
Let $ninmathbbN$ be an arbitrary number for which the claim holds:
$s(n+1) = (n+1) + 1 = s(n) + 1 = s^[n](1) + 1 = s^[n+1](1)$
By the axiom of mathematical induction, the claim holds for all natural numbers.
Now let $SsubsetmathbbN$ be the set of all numbers for which the original claim holds.
- Case $m=1$
$n+1 = s(n) = s^[n](1) = 1 + n$
- Let $min S$ be arbitrary $implies n + m = m + n$
$n + (m+1) = s^[m+1](n) = s(s^[m](n)) =s(n+m) =$ ( $min S$ ) $= s(m+n) = s(s^[n](m)) = s^[n+1](m) = m + (n+1) =$ (Case 1.) $=m+(1+n)=$ (associative) $=(m+1)+n$.
From 1. we have $1in S$ and from 2. we have $min S implies s(m)=m+1in S$ and by the axiom of mathematical induction it follows that $S = mathbbN$.
proof-verification induction natural-numbers
$endgroup$
|
show 2 more comments
$begingroup$
I would like to prove the associative and commutative property of the natural numbers by using Peanos axioms only. Did I justify every step in my proofs correctly?
Definition. $forall n,m in mathbbN , n+m = underbraces(s(...s_textm (n)...)) = s^[m](n) $ where $s(n)$ is the successor function.
a) $forall n,m,k in mathbbN , n+(m+k)=(n+m)+k$
Proof: Let $SsubsetmathbbN$ be the set for which a) holds.
- Case $k=1 , forall n,m in mathbbN$
$n +(m+1) =$ (definition of $+$) $ = s^[m+1](n) = (*) = s(s^[m](n)) = s(m + n) = (m+n) + 1$
I am not sure how to justify $(*)$. I have:
$s^[m+1](n) = underbraces(s(....s_textm(underbraces_text1(n))...))=underbraces_text1(underbraces(s(...s_textm(n)...)))=s(s^[m](n))$
The composition of functions is associative but am I implicitly assuming the commutative property of the natural numbers i.e. $m+1 = 1+m$ ?
- Let $kin S$ be arbitrary $implies n+(m+k)=(n+m)+k$
$n+(m+(k+1))= $ (From 1. for $m+(k+1)$) = $n +((m+k)+1) = $ (From 1. for $n+(t+1)$ and $t=m+kinmathbbN$) $=(n+t)+1 = (n + (m+k))+1 = (kin S) = ((n+m)+k)+1=s^[k](n+m)+1=s^[k+1](n+m) = (n+m)+(k+1)$
From 1. we have $1in S$ and from 2. we have $kin S implies s(k)=k+1in S$ and by the axiom of mathematical induction it follows that $S = mathbbN$.
b) $forall n,m in mathbbN , n+m=m+n$
Proof:
First we will show that $s(n) = s^[n](1)$
$n=1 implies s(1) = 1+1 = s^[1](1)$
Let $ninmathbbN$ be an arbitrary number for which the claim holds:
$s(n+1) = (n+1) + 1 = s(n) + 1 = s^[n](1) + 1 = s^[n+1](1)$
By the axiom of mathematical induction, the claim holds for all natural numbers.
Now let $SsubsetmathbbN$ be the set of all numbers for which the original claim holds.
- Case $m=1$
$n+1 = s(n) = s^[n](1) = 1 + n$
- Let $min S$ be arbitrary $implies n + m = m + n$
$n + (m+1) = s^[m+1](n) = s(s^[m](n)) =s(n+m) =$ ( $min S$ ) $= s(m+n) = s(s^[n](m)) = s^[n+1](m) = m + (n+1) =$ (Case 1.) $=m+(1+n)=$ (associative) $=(m+1)+n$.
From 1. we have $1in S$ and from 2. we have $min S implies s(m)=m+1in S$ and by the axiom of mathematical induction it follows that $S = mathbbN$.
proof-verification induction natural-numbers
$endgroup$
1
$begingroup$
You'll have to clarify lines like "Let $SsubsetmathbbN$ be the set for which a) holds." I suspect you mean that you are looking at the $k$ which make it true foe all $m,n$ but since (a) has no free variables what you say is meaningless.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
You'll find it much easier to root the inductions at $0$.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
OK, but as I said, that's not what you have written, is it?
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
I'd also recommend not using $dots$ in such proofs/definitions. I think that's where you're getting confused. If you insist in excluding $0$ from $mathbbN$ then the definition of $+$ in terms of $s$ is: $m+1=s(m)$, $m+s(n)=s(m+n)$. It's then pretty straightforward to prove associativity.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
I'm sorry, it just seems to me not to be a good enough definition as it leads to exactly this doubt. I think you are right when you say you've used $m+1=1+m$ at $(*)$; the problem is that the Peano arithmetic is escaping into the mathematical language describing it. In most standard formulations one proves associativity, then $1+m=m+1$ then full commutativity.
$endgroup$
– ancientmathematician
yesterday
|
show 2 more comments
$begingroup$
I would like to prove the associative and commutative property of the natural numbers by using Peanos axioms only. Did I justify every step in my proofs correctly?
Definition. $forall n,m in mathbbN , n+m = underbraces(s(...s_textm (n)...)) = s^[m](n) $ where $s(n)$ is the successor function.
a) $forall n,m,k in mathbbN , n+(m+k)=(n+m)+k$
Proof: Let $SsubsetmathbbN$ be the set for which a) holds.
- Case $k=1 , forall n,m in mathbbN$
$n +(m+1) =$ (definition of $+$) $ = s^[m+1](n) = (*) = s(s^[m](n)) = s(m + n) = (m+n) + 1$
I am not sure how to justify $(*)$. I have:
$s^[m+1](n) = underbraces(s(....s_textm(underbraces_text1(n))...))=underbraces_text1(underbraces(s(...s_textm(n)...)))=s(s^[m](n))$
The composition of functions is associative but am I implicitly assuming the commutative property of the natural numbers i.e. $m+1 = 1+m$ ?
- Let $kin S$ be arbitrary $implies n+(m+k)=(n+m)+k$
$n+(m+(k+1))= $ (From 1. for $m+(k+1)$) = $n +((m+k)+1) = $ (From 1. for $n+(t+1)$ and $t=m+kinmathbbN$) $=(n+t)+1 = (n + (m+k))+1 = (kin S) = ((n+m)+k)+1=s^[k](n+m)+1=s^[k+1](n+m) = (n+m)+(k+1)$
From 1. we have $1in S$ and from 2. we have $kin S implies s(k)=k+1in S$ and by the axiom of mathematical induction it follows that $S = mathbbN$.
b) $forall n,m in mathbbN , n+m=m+n$
Proof:
First we will show that $s(n) = s^[n](1)$
$n=1 implies s(1) = 1+1 = s^[1](1)$
Let $ninmathbbN$ be an arbitrary number for which the claim holds:
$s(n+1) = (n+1) + 1 = s(n) + 1 = s^[n](1) + 1 = s^[n+1](1)$
By the axiom of mathematical induction, the claim holds for all natural numbers.
Now let $SsubsetmathbbN$ be the set of all numbers for which the original claim holds.
- Case $m=1$
$n+1 = s(n) = s^[n](1) = 1 + n$
- Let $min S$ be arbitrary $implies n + m = m + n$
$n + (m+1) = s^[m+1](n) = s(s^[m](n)) =s(n+m) =$ ( $min S$ ) $= s(m+n) = s(s^[n](m)) = s^[n+1](m) = m + (n+1) =$ (Case 1.) $=m+(1+n)=$ (associative) $=(m+1)+n$.
From 1. we have $1in S$ and from 2. we have $min S implies s(m)=m+1in S$ and by the axiom of mathematical induction it follows that $S = mathbbN$.
proof-verification induction natural-numbers
$endgroup$
I would like to prove the associative and commutative property of the natural numbers by using Peanos axioms only. Did I justify every step in my proofs correctly?
Definition. $forall n,m in mathbbN , n+m = underbraces(s(...s_textm (n)...)) = s^[m](n) $ where $s(n)$ is the successor function.
a) $forall n,m,k in mathbbN , n+(m+k)=(n+m)+k$
Proof: Let $SsubsetmathbbN$ be the set for which a) holds.
- Case $k=1 , forall n,m in mathbbN$
$n +(m+1) =$ (definition of $+$) $ = s^[m+1](n) = (*) = s(s^[m](n)) = s(m + n) = (m+n) + 1$
I am not sure how to justify $(*)$. I have:
$s^[m+1](n) = underbraces(s(....s_textm(underbraces_text1(n))...))=underbraces_text1(underbraces(s(...s_textm(n)...)))=s(s^[m](n))$
The composition of functions is associative but am I implicitly assuming the commutative property of the natural numbers i.e. $m+1 = 1+m$ ?
- Let $kin S$ be arbitrary $implies n+(m+k)=(n+m)+k$
$n+(m+(k+1))= $ (From 1. for $m+(k+1)$) = $n +((m+k)+1) = $ (From 1. for $n+(t+1)$ and $t=m+kinmathbbN$) $=(n+t)+1 = (n + (m+k))+1 = (kin S) = ((n+m)+k)+1=s^[k](n+m)+1=s^[k+1](n+m) = (n+m)+(k+1)$
From 1. we have $1in S$ and from 2. we have $kin S implies s(k)=k+1in S$ and by the axiom of mathematical induction it follows that $S = mathbbN$.
b) $forall n,m in mathbbN , n+m=m+n$
Proof:
First we will show that $s(n) = s^[n](1)$
$n=1 implies s(1) = 1+1 = s^[1](1)$
Let $ninmathbbN$ be an arbitrary number for which the claim holds:
$s(n+1) = (n+1) + 1 = s(n) + 1 = s^[n](1) + 1 = s^[n+1](1)$
By the axiom of mathematical induction, the claim holds for all natural numbers.
Now let $SsubsetmathbbN$ be the set of all numbers for which the original claim holds.
- Case $m=1$
$n+1 = s(n) = s^[n](1) = 1 + n$
- Let $min S$ be arbitrary $implies n + m = m + n$
$n + (m+1) = s^[m+1](n) = s(s^[m](n)) =s(n+m) =$ ( $min S$ ) $= s(m+n) = s(s^[n](m)) = s^[n+1](m) = m + (n+1) =$ (Case 1.) $=m+(1+n)=$ (associative) $=(m+1)+n$.
From 1. we have $1in S$ and from 2. we have $min S implies s(m)=m+1in S$ and by the axiom of mathematical induction it follows that $S = mathbbN$.
proof-verification induction natural-numbers
proof-verification induction natural-numbers
edited 2 days ago
AltairAC
asked Mar 25 at 20:08
AltairACAltairAC
5591519
5591519
1
$begingroup$
You'll have to clarify lines like "Let $SsubsetmathbbN$ be the set for which a) holds." I suspect you mean that you are looking at the $k$ which make it true foe all $m,n$ but since (a) has no free variables what you say is meaningless.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
You'll find it much easier to root the inductions at $0$.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
OK, but as I said, that's not what you have written, is it?
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
I'd also recommend not using $dots$ in such proofs/definitions. I think that's where you're getting confused. If you insist in excluding $0$ from $mathbbN$ then the definition of $+$ in terms of $s$ is: $m+1=s(m)$, $m+s(n)=s(m+n)$. It's then pretty straightforward to prove associativity.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
I'm sorry, it just seems to me not to be a good enough definition as it leads to exactly this doubt. I think you are right when you say you've used $m+1=1+m$ at $(*)$; the problem is that the Peano arithmetic is escaping into the mathematical language describing it. In most standard formulations one proves associativity, then $1+m=m+1$ then full commutativity.
$endgroup$
– ancientmathematician
yesterday
|
show 2 more comments
1
$begingroup$
You'll have to clarify lines like "Let $SsubsetmathbbN$ be the set for which a) holds." I suspect you mean that you are looking at the $k$ which make it true foe all $m,n$ but since (a) has no free variables what you say is meaningless.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
You'll find it much easier to root the inductions at $0$.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
OK, but as I said, that's not what you have written, is it?
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
I'd also recommend not using $dots$ in such proofs/definitions. I think that's where you're getting confused. If you insist in excluding $0$ from $mathbbN$ then the definition of $+$ in terms of $s$ is: $m+1=s(m)$, $m+s(n)=s(m+n)$. It's then pretty straightforward to prove associativity.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
I'm sorry, it just seems to me not to be a good enough definition as it leads to exactly this doubt. I think you are right when you say you've used $m+1=1+m$ at $(*)$; the problem is that the Peano arithmetic is escaping into the mathematical language describing it. In most standard formulations one proves associativity, then $1+m=m+1$ then full commutativity.
$endgroup$
– ancientmathematician
yesterday
1
1
$begingroup$
You'll have to clarify lines like "Let $SsubsetmathbbN$ be the set for which a) holds." I suspect you mean that you are looking at the $k$ which make it true foe all $m,n$ but since (a) has no free variables what you say is meaningless.
$endgroup$
– ancientmathematician
2 days ago
$begingroup$
You'll have to clarify lines like "Let $SsubsetmathbbN$ be the set for which a) holds." I suspect you mean that you are looking at the $k$ which make it true foe all $m,n$ but since (a) has no free variables what you say is meaningless.
$endgroup$
– ancientmathematician
2 days ago
1
1
$begingroup$
You'll find it much easier to root the inductions at $0$.
$endgroup$
– ancientmathematician
2 days ago
$begingroup$
You'll find it much easier to root the inductions at $0$.
$endgroup$
– ancientmathematician
2 days ago
1
1
$begingroup$
OK, but as I said, that's not what you have written, is it?
$endgroup$
– ancientmathematician
2 days ago
$begingroup$
OK, but as I said, that's not what you have written, is it?
$endgroup$
– ancientmathematician
2 days ago
1
1
$begingroup$
I'd also recommend not using $dots$ in such proofs/definitions. I think that's where you're getting confused. If you insist in excluding $0$ from $mathbbN$ then the definition of $+$ in terms of $s$ is: $m+1=s(m)$, $m+s(n)=s(m+n)$. It's then pretty straightforward to prove associativity.
$endgroup$
– ancientmathematician
2 days ago
$begingroup$
I'd also recommend not using $dots$ in such proofs/definitions. I think that's where you're getting confused. If you insist in excluding $0$ from $mathbbN$ then the definition of $+$ in terms of $s$ is: $m+1=s(m)$, $m+s(n)=s(m+n)$. It's then pretty straightforward to prove associativity.
$endgroup$
– ancientmathematician
2 days ago
1
1
$begingroup$
I'm sorry, it just seems to me not to be a good enough definition as it leads to exactly this doubt. I think you are right when you say you've used $m+1=1+m$ at $(*)$; the problem is that the Peano arithmetic is escaping into the mathematical language describing it. In most standard formulations one proves associativity, then $1+m=m+1$ then full commutativity.
$endgroup$
– ancientmathematician
yesterday
$begingroup$
I'm sorry, it just seems to me not to be a good enough definition as it leads to exactly this doubt. I think you are right when you say you've used $m+1=1+m$ at $(*)$; the problem is that the Peano arithmetic is escaping into the mathematical language describing it. In most standard formulations one proves associativity, then $1+m=m+1$ then full commutativity.
$endgroup$
– ancientmathematician
yesterday
|
show 2 more comments
0
active
oldest
votes
Your Answer
StackExchange.ifUsing("editor", function ()
return StackExchange.using("mathjaxEditing", function ()
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix)
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
);
);
, "mathjax-editing");
StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "69"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);
else
createEditor();
);
function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader:
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
,
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);
);
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3162260%2fproving-that-addition-in-mathbbn-is-associative-and-commutative%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
0
active
oldest
votes
0
active
oldest
votes
active
oldest
votes
active
oldest
votes
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3162260%2fproving-that-addition-in-mathbbn-is-associative-and-commutative%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
1
$begingroup$
You'll have to clarify lines like "Let $SsubsetmathbbN$ be the set for which a) holds." I suspect you mean that you are looking at the $k$ which make it true foe all $m,n$ but since (a) has no free variables what you say is meaningless.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
You'll find it much easier to root the inductions at $0$.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
OK, but as I said, that's not what you have written, is it?
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
I'd also recommend not using $dots$ in such proofs/definitions. I think that's where you're getting confused. If you insist in excluding $0$ from $mathbbN$ then the definition of $+$ in terms of $s$ is: $m+1=s(m)$, $m+s(n)=s(m+n)$. It's then pretty straightforward to prove associativity.
$endgroup$
– ancientmathematician
2 days ago
1
$begingroup$
I'm sorry, it just seems to me not to be a good enough definition as it leads to exactly this doubt. I think you are right when you say you've used $m+1=1+m$ at $(*)$; the problem is that the Peano arithmetic is escaping into the mathematical language describing it. In most standard formulations one proves associativity, then $1+m=m+1$ then full commutativity.
$endgroup$
– ancientmathematician
yesterday