logicpeano-axioms
In Peano arithmetic (first order), we first define natural numbers using a successor function and Peano axioms, then we define addition (and multiplication), and then, we define inequality, as:
$a\leq b\leftrightarrow\exists c\left(a+c=b\right)$
Is there any way to define inequality first, directly from the successor function and Peano axioms? (I mean, if I don't need addition for my purpose, why define it?).
The bare bones answer is something like what Hagen has said. The idea is this: Exponentiation is understood to be a function defined recursively: $y=2^x$ iff there is a sequence $t_0,t_1,\dots,t_x$ such that
In this respect, exponentiation is hardly unique: $y=x!$ is defined similarly, for example. Now you'd say that there is a sequence $z_0,z_1,\dots,z_x$, such that
(That $t_0=z_0=1$ is coincidence. In one case it is because $2^0=1$; in the other, because $0!=1$.)
So, to define a formula saying that $y=2^x$, you'd like to say that there is a sequence $t_0,\dots,t_x$ as above.
The problem, of course, is that in Peano Arithmetic one talks about numbers rather than sequences. Gödel solved this problem when working on his proof of the incompleteness theorem: He explained how to code finite sequences by numbers, by using the Chinese remainder theorem. Recall that this result states that, given any numbers $n_1,\dots,n_k$, pairwise relatively prime, and any numbers $m_1,\dots,m_k$, there is a number $x$ that simultaneously satisfies all congruences $$ x\equiv m_i\pmod {n_i} $$ for $1\le i\le k$.
In particular, given $m_1,\dots,m_k$, let $n=t!$ where $t=\max(m_1,\dots,m_k,k)$. Letting $n_1=n+1$, $n_2=2n+1,\dots$, $n_k=kn+1$, we see that the $n_i$ are relatively prime, and we can find an $x$ that satisfies $x\equiv m_i\pmod{n_i}$ for all $i$. We can then say that the pair $\langle x,n\rangle$ codes the sequence $(m_1,\dots,m_k)$. In fact, given $x,n$, it is rather easy to "decode" the $m_i$: Just note that $m_i$ is the remainder of dividing $x$ by $in+1$.
Accordingly, we can define $y=2^x$ by saying that there is a pair $\langle a,b\rangle$ that, in the sense just described, codes a sequence $(t_0,t_1,\dots,t_x)$ such that $t_0=1$, $t_x=y$, and $t_{n+1}=2t_n$ for all $n<x$. (Again, "in the sense just described" ends up meaning simply that "the remainder of dividing $a$ by $ib+1$ is $t_i$ for all $i\le x$". Note that we are not requiring $b$ to be the particular number we exhibited above using factorials.)
Of course, one needs to prove that any two pairs coding such a sequence agree on the value of $t_x$, but this is easy to establish. And we can code a pair by a number using, for example, Cantor's enumeration of $\mathbb N\times\mathbb N$, so that $\langle a,b\rangle$ is coded as the number $$ c=\frac{(a+b)(a+b+1)}2+b. $$ This is a bijection, and has the additional advantages that it is definable and satisfies $a,b\le c$ (so it is given by a bounded formula).
An issue that appears now is that we need to formalize the discussion of the Chinese remainder theorem and the subsequent coding within Peano arithmetic. This presents new difficulties, as again, we cannot (in the language of arithmetic) talk about sequences, and cannot talk about factorials, until we do all the above, so it is not clear how to prove or even how to formulate these results.
This problem can be solved by noting that we can use induction within Peano arithmetic. One then proceeds to show, essentially, that given any finite sequence, there is a pair that codes it, and that if a pair codes a sequence $\vec s$, and a number $t$ is given, then there is a pair that codes the sequence $\vec s{}^\frown(t)$. That is, one can write down a formula $\phi(x,y,z)$, "$y$ codes a sequence, the $z$-th member of which is $x$", such that PA proves:
In fact, we can let $\phi$ be a bounded formula: Take $\phi(x,y,z)$ to be
There are $a,b\le y$ such that $y=\langle a,b\rangle$ (Cantor's pairing) and $x<zb+1$ and there is a $d\le a$ such that $a=d(zb+1)+x$.
Once we have in PA the existence of coded sequences like this, implementing recursive definitions such as exponential functions is straightforward.
There are two excellent references for these coding issues and the subtleties surrounding them:
There is a point of confusion in the question:
For instance, I've read that we can define addition in second-order arithmetic by writing
- $x+0 = x$
- $x+S(y) = S(x+y).$
Why does this work in second order arithmetic, but not in first-order?
That does not work in second-order arithmetic. It is an implicit characterization of the addition function, but it is not an explicit definition of the addition function in terms of the successor function.
A genuine definition is a formula $\phi(n,m,p)$ in a language without the addition symbol $+$ such that, for all natural numbers $n,m,p$, we have $n + m = p$ if and only if $\phi(n,m,p)$ holds. A "pseudo-definition" that is able to refer to the object being defined is called an implicit definition, but implicit definability is much weaker than actual definability.
One actual definition of addition of natural numbers in second-order arithmetic is: $$ n + m = p \Leftrightarrow (\forall f)\left[ \left( f(0) = n \land (\forall k)[f(S(k)) = S(f(k)]\right ) \to f(m) = p\right]. $$ Here $n,m,p$ are natural numbers, $(\forall k)$ quantifies over the natural numbers, and $(\forall f)$ quantifies over all unary functions from the natural numbers to themselves. Notice that, crucially, the right side does not mention $+$. In the particular definition, we could also rewrite it with an existential function quantifier: $$ n + m = p \Leftrightarrow (\exists f)\left( f(0) = n \land (\forall k)[f(S(k)) = S(f(k))] \land f(m) = p\right.) $$
Why does this definition not work in first-order logic? Because, in a single-sorted first-order theory of arithmetic, it is not possible to quantify over functions in the way that the definition does.
Now, that does not prove that it is impossible to define addition of natural numbers in terms of successor. It only shows that the definition in second-order arithmetic does not go through unchanged.
One way to see that addition is not definable from successor is sketched in this answer by Alex Kruckman. The key point is that if we look at the first-order theory of the natural numbers with successor and a constant for 0, every formula in this language (with some free variables) is equivalent to a quantifier-free formula in the language (with the same free variables). A proof of that is given by Richard Kaye here. So if addition was definable in that structure, it would be definable by a quantifier-free formula. But by analyzing the form of such a formula we can show that it cannot define addition.
Actually, more is known. Neither addition nor multiplication is definable from successor alone; multiplication is not definable from successor and addition; and addition is not definable from successor and multiplication. The theory of the natural numbers with multiplication and addition is undecidable, but the restriction to just addition is decidable, and the restriction with just multiplication is decidable.
Best Answer
In a precise sense, the answer is no. Namely, let $PA_{succ}$ be the set of PA-theorems in the language containing only the symbol for the successor function; then we can show:
In particular, this means that there is no first-order formula using only successor which PA proves defines a linear ordering.
Specifically, consider the structure (in the language of successor only) $\mathbb{N}+\mathbb{Z}+\mathbb{Z}$. This is a model of $PA_{succ}$ (this takes a bit of work, but isn't hard), but has no definable linear ordering: consider any automorphism swapping the two $\mathbb{Z}$-parts.
(A bit more thought also shows that there is no formula in the language of successor alone which defines a linear ordering in the standard model $\mathbb{N}$; the key ingredient is the proof that $PA_{succ}$ is complete. And in fact thinking along these lines ultimately shows that no model of $PA_{succ}$ has a definable linear ordering.)