Often when reading various texts involving total/partial orders, I come across statements like:
"...thus $\leq$ is a total order on $\mathbb{Z}$ when $a \leq b$ is given its usual meaning."
Is there a precise definition for said "meaning"? I've never actually seen one. Of course one could say $a \leq b$ $\iff$ $-a \geq -b$, but I feel this doesn't really address the issue.
I'm beginning to think that we aren't really giving $\geq$ meaning, we're in fact giving arbitrary integers meaning. For instance, perhaps we define $3$ as: $3 \in \mathbb{Z}$ such that $3 \neq 2,4$ and $2 \leq 3 \leq 4$. But this requires a definition of $2$, which, if we were to formulate in a similar way, would require a definition of $3$. Perhaps this is acceptable, but it seems somewhat circular to me.
Algebraic definition
Here is the typical algebraic way to define usual meaning: $\def\nn{\mathbb{N}}$ $\def\zz{\mathbb{Z}}$
Note that this definition relies on having defined $\nn$ first, and then later $\zz$ with $\nn$ embedded into it. And when it gets down to $\nn$, you use the Peano Arithmetic axioms for it, which needs non-logical symbols $(\nn,0,1,+,\times)$.
Computational definition
You can define $\zz$ to be the collection of finite strings made up of decimal digits and an optional negative sign at the start. Then you can define $\le$ directly as an algorithm:
Note that the table used by the above definition would be much simpler if we use binary instead of decimal representation, but either way the idea is the same.
Comparison
It is certainly harder to prove that the computational definition is a total order! That is one main reason to use the algebraic definition. However, it is now obvious that the algebraic definition does not really answer the question, because it is nothing more than just pushing the question under the carpet by assuming the consistency of PA, that is, the existence of a model of PA. In contrast, the computational method is more concrete, since it is actually physically implemented on every computer/calculator in an equivalent form.