I am trying to formally construct the usual partial ordering LTE from Peano's 5 Axioms. Would the following construction work?
$$\forall a,b: [(a,b)\in LTE \iff(a,b)\in N^2$$
$$\land ~ \forall c\subset N^2:[\forall d\in N: [(d,d) \in c]$$
$$ \land ~ \forall d,e:[(d,e)\in c \implies(d, S(e))\in c]$$
$$\implies (a,b) \in c]]$$
where $N$ is the set of natural numbers and $S$ is the usual successor function on $N$.
EDIT:
Informally, for all $x,y\in N$, we can recursively define $\le$ on $N$ as the "smallest" set of ordered pairs of natural numbers that satisfies:
$$x \le x$$
$$x\le y \implies x\le S(y)$$
(Answering my own question)
Thanks all for your help, but I didn't find my construction here to be very workable. I was trying to avoid using an addition function to "simplify things." That was probably a mistake.
Using Peano's Axioms, some basic set theory and a form of natural deduction, I formally constructed (in order) the function $+$ and the relations $\leq$ and $\lt$ as sets of ordered n-tuples such that, for all $x, y \in N$ we have:
$x+0 = x$
$x+S(y) = S(x+y)$
$x\leq y \iff \exists z\in N: x+z=y$
$x \lt y \iff x\leq y ~\land ~ x\neq y$
Everything then fell into place. I was just now able to derive the usual fundamental properties of $+$, $\leq$ and $\lt$ for a larger project that I am working on.