2

I am struggling with

$$\mathbb{N} \models \langle x,y \rangle =\langle u,v \rangle \rightarrow x=u, y=v $$

where $\langle x,y \rangle:=(x+y)^2 +x$ is $L_{PA}-term$, where $L_{PA}$ is languague of Peano arithmetic and $\mathbb{N}$ the standard model of it ($\mathbb{N} = \langle \mathbb{N}, 0, s, +, *, \leq \rangle$ where $s$ is a succesor function). According to my lecture notes I should get something like $$\langle x,y \rangle = \langle u,v \rangle \rightarrow x+y=u+v$$ from which it easily follows. I only got $(x+y)^2 \leq \langle u,v \rangle < (x+y+1)^2$. I guess I am missing something obvious but I do not know what. When I draw this as a pairing function, I see, that the statement holds.

It is an example from the begining of Sequence encoding.

Tusau
  • 81

1 Answers1

1

We have $x + y = \max \{z | z^2 \leq \langle x, y\rangle\}$: $(x + y)^2 \leq \langle x, y\rangle$, but $(x + y + 1)^2 = (x + y)^2 + 2x + 2y + 1 > \langle x, y\rangle$.

Or, in PA, $x + y = z$ can be written as $z^2 \leq \langle x, y\rangle \wedge (z + 1)^2 > \langle x, y\rangle$.

Thus, if $\langle x, y\rangle = \langle u, v\rangle$ then $$x + y = \max \{z | z^2 \leq \langle x, y\rangle\} = \max \{z | z^2 \leq \langle u, v\rangle\} = u + v$$

mihaild
  • 15,368