Show for i' that ∀x x' + i' = x + i'' I am given the following...
When $i = 0$ $\forall x\colon x' + 0 = x + 0'$
Assume it holds that $\forall x\colon x' + i = x + i'$
Show that $\forall x\colon x' + i' = x + i''$
My tools are the axioms of Q
The only ones that seem relevant are
Q1 : $\forall x\forall y(x'= y' \to x = y)$
Q4 : $\forall x x + 0  = x$
Q5 : $\forall x\forall y x + y' = (x + y)'$
I've been trying this for a while and these were my attempted solutions
1
$x' + i' = x + i''$
$x + 0' + i' = x + i''$ by Q4
from here I tried to to let $i' = y$ to get
$x + (y + 0')  = x + y'$
$x + (y + 0)' = x + y'$ by Q4
$x + (y)'= x + y'$
$x + y' = x + y'$
setting $y = i'$
$x + i'' = x + i''$
Not sure if this was the right way.
 A: Try starting with the logical truth:
$$x'+i'=x'+i'$$
then
$$x'+i'=x'+(i+0)'\;\;\text{by Q4}$$
can you continue? let me know and I'll go further.
edit after your comment:
in order to format formulae in Tex you can place them between two dollar signs. "$"
edit 2, the full answer:
The next obvious step in the proof is applying Q5 to get the equation: 
$$x'+i'=x'+i+0'\;\;\text{by Q5}$$
$$x'+i'=x+i'+0'\;\;\text{by the induction hypothesis}$$
$$x'+i'=x+(i'+0)'\;\;\text{by Q5}$$
$$x'+i'=x+(i')'\;\;\text{by Q4}$$
Which is the desired result.
A: Yeah no, that does not prove anything; indeed I could have stated ahead of time that $x + S(S(i)) = x + S(S(i))$ without knowing anything about the successor function $S$: it is tautologically true. But what you are being asked to prove is a very deep fact, which is that the addition functions defined by
data N = Zero | S N

add1 a Zero = a
add1 a (S n) = S (add1 a n)

add2 a Zero = a
add2 a (S n) = add2 (S a) n

are both the same function. (In fact this matters a lot for computer programmers because it turns out that in many computer programming languages add1 wastes a precious resource called the “call stack” whereas add2 is “tail-recursive” and so it can be optimized to a loop to not waste this particular resource.)
You want to use two facts here:


*

*If $A = B$ then $S(A) = S(B).$ This does not appear as an axiom  because it does not need to, it is part of what it means for two things to be equal: they must in all ways be indistinguishable including by applying any function to them.

*If $A = S(b + c)$ then $A = b + S(c).$ This is part of the definition of addition but you normally use it the forwards way, going from $b + S(c)$ to $S(b + c).$ I am telling you that because these two entities are equal, you can also use it in this reverse way. Equals signs are nondirectional.


Starting from the given assumption about $S(x) + i = x + S(i),$ apply $S(\bullet)$ to both sides per the first fact and then use the reasoning of the second fact to get to your desired happy place.
