2
$\begingroup$

In other words, for any two natural numbers, there exist no more than one natural number that equals the sum of the two numbers. Or rather, for any two natural numbers, their sum is unique.

In first order logic, I am trying to prove the following:

$\forall a,b,c,c'\in \mathbb{N}(a+b=c \land a+b=c' \implies c=c')$

I tried induction on $b$, and proved the base case for $b=0$, but am having trouble with the inductive step.

Edit: I was confused while asking the question. I am indeed looking for a proof that addition is injective, rather than one that equality is transitive.

$\endgroup$
2
  • 2
    $\begingroup$ Are you trying to prove addition is injective, if you fix a? Since, as others have noted, what you're trying to prove is somewhat trivial. That's what I thought you meant at first. $\endgroup$ Jul 5 at 22:52
  • 2
    $\begingroup$ As soon as you adopt the (functional) notation $a+b$ to denote a number, you are already assuming addition is a well defined (single-valued) operation. I think that indeed addition is defined in the Peano system as a (recursively defined) map $\Bbb N\times\Bbb N\to\Bbb N$; while that leaves something to prove namely that the recursion is well founded, it does not leave any doubt about the uniqueness of the sum obtained (supposing one is). Things would be different if "$R(a,b,c)\equiv(a+b=c)$ were defined as a relation on $\Bbb N^3$, but I don't think that is the case. $\endgroup$ Jul 6 at 10:52

3 Answers 3

2
$\begingroup$

Suppose $a + b = c$ and $a + b = c’$. By the symmetric property of equality, $c = a + b$. By the transitive property of equality, $c = c’$.

As you can see, the proof here is trivial. So there is probably some source of confusion if you think the proof shouldn’t be trivial.

$\endgroup$
2
$\begingroup$

Equality is an equivalence relation. Equivalence relations are all defined by being reflexive, symmetric, and transitive. So by the transitive property of equality $c=a+b=c' \implies c=c'$. And this is also the $4^{\text{th}}$ Peano axiome.

$\endgroup$
0
$\begingroup$

I'd introduce addition as follows:

$a + 0 = a$ and $a + v(b) = v(a+b)$ where $v$ denotes the successor.

This leads to an answer of your problem.

$\endgroup$
1
  • 1
    $\begingroup$ But as the other answers stated, this uniqueness can be confirmed without using any properties of addition, except that it's a (total) function $\mathbb{N}\times\mathbb{N}\to\mathbb{N}$. It would work just as well with the operator $a\star b := 37a^3 + \lfloor\sin(a\cdot b^2) + \pi\rfloor$. $\endgroup$ Jul 6 at 9:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.