Notation: Within $RCA_0,$ define pairing map $$(i,j) = (i+j)^2+i$$
In Simpson's Subsystem of Second Order Arithmetic, chapter $2,$ he stated the following theorem.
Theorem II $2.2$ The following are provable in $RCA_0.$
$1.$ $i\leq (i,j)$ and $j\leq (i,j).$
$2.$ $(i,j) = (i',j') \rightarrow (i=i' \wedge j=j').$
The author provided the following proof.
Proof: Part $1$ is obvious. For part $2,$ given $k= (i,j) = (i+j)^2+i,$ we claim that there exists a unique $m$ such that $$m^2\leq k <(m+1)^2.$$ Existence of $m$ is obvious by taking $m=i+j,$ and uniqueness follows from the fact that $m<n\rightarrow m^2<n^2.$ It now follows that $i=k-m^2$ and $j=m-i.$ This proves part $2.$
I very confused about the proof for part $2.$ I do not see how the proof above uses assumption and shows that $i=i' \wedge j=j'.$ It seems to me it is not relevant here.
Can anyone enlighten me? Thanks.
In the given context, the easiest and most useful way of demonstrating that the pairing function is injective is to explicitly recover the components, i.e. define the projections.
The given proof shows you how to explicitly calculate $i$ and $j$ and gives formulas that determine $i$ and $j$ given $(i,j)$. Since the $m$ in the formulas is unique, these formulas uniquely determine $i$ and $j$. If $(i,j)=k=(i',j')$, then the $i$ and $i'$ calculated from $k$ must be equal, and similarly for $j$ and $j'$.
The implicit algorithm is simply to pick the largest number whose square is less than or equal to $(i,j)$ (by counting up to it if necessary). This will be $i+j$. We can then calculate $i$ and $j$ as given by the formulas.