As William pointed out in his answer, Peano Arithmetic is a certain first-order theory which describes properties of $\mathbb{N}$, the natural numbers (that is, $\mathbb{N}\models\text{PA}$). However, it is incomplete (as shown by Gödel), and hence it is not equal to the complete theory of the natural numbers, denoted $\text{Th}(\mathbb{N})$, which consists of all first-order statements true of $\mathbb{N}$. The situation is different with the theory of real closed fields - this is a complete theory, and $\mathbb{R}\models \text{RCF}$, so $\text{RCF} = \text{Th}(\mathbb{R})$.
Your main confusion, however, seems to be about how $\text{Th}(\mathbb{N})$ can be so much more complicated than $\text{Th}(\mathbb{R})$, despite the fact that $\mathbb{N}\subset \mathbb{R}$. If $\text{Th}(\mathbb{R})$ is decidable, why can't we use the decision procedure to decide all questions about $\mathbb{N}$?
This phenomenon is possible because there is no single first-order formula (in our language $\{0,1,+,\cdot\}$) which picks out the natural numbers as a subset of the reals. To decide whether a sentence is true about $\mathbb{N}$ by asking a question about $\mathbb{R}$, we would have to somehow ensure that all quantifiers talk only about the integers.
To illustrate the difficulty, consider the sentence $\phi:\forall x\,\exists y\, (y+y = x)$. $\phi$ is certainly false in $\mathbb{N}$. But to use the decidability of $\text{Th}(\mathbb{R})$ to see this, we would need to be able to express that for all natural numbers $x$ there is a natural number $y$ such that $y+y = x$, which we cannot do. Allowing the variables to range over $\mathbb{R}$, $\phi$ is true.
Intuitively, it is questions about divisibility like this one which make $\text{Th}(\mathbb{N})$ so much more complicated than $\text{Th}(\mathbb{R})$. The formula $\psi(x,y):\exists z (x = y\cdot z)$, expressing that $y|x$, gives access to all the complexity of the prime numbers. By contrast, the reals are extremely homogeneous: $\psi(x,y)$ is true of a pair of reals $(a,b)$ whenever $b\neq 0$.
I'm not totally sure what you're asking, but let me take a stab at it:
Your sentence
One must see 'semi-decidable' as a property of the specific decision problem, i.e. keep apart "x is satisfiable" and "x is not satisfiable"
is absolutely correct. There are many senses in which two decision problems can be "equivalent," and the point is that semidecidability (or more commonly, computable or recursive enumerability) does not always respect these notions. For instance, every c.e. set is Turing equivalent to a co-c.e. set, but obviously no c.e. set is also co-c.e. unless it is computable. This is essentially the example you give of unsatisfiability for first-order formulas.
Best Answer
First: The difference between axioms and theorems is this: Axioms are given statements that reflect elementary truths that we suppose to be true of some domain. For example, $\forall x \ x+0=x$ is one of the axioms of Robinson Arithmetic ($Q$), and indeed it expresses some very elementary truth about arithmetic.
A theorem, on the other hand, is some statement we can infer from the axioms. So this is typically something more complicated. For example, we can combine the axioms $\forall x \ x+0=x$ and $\forall x \forall y \ x + s(y) = s(x+y)$ to infer the theorem that $\forall x \ x + s(0) = s(x)$.
There are a few different sets of axioms for Robinson arithmetic, but the idea is that there are only a limited number of axioms. The Robinson Arithmetic Wikipedia page shows $7$ axioms for $Q$.
Now, the theory of $Q$ is the set of all theorems, i.e. all the statements that you can infer from the axioms. I think you can easily see that there are infinitely many theorems.
A set of statements being decidable means that there is some systematic algorithm that can decide, given any statement, whether it is a member of that set or not.
Note that any finite set of statements is intuitively decidable: for any given statement, we can simply compare it, one by one, with the finite set of statements and see if they match: we will either get a match or, after some finite amount of time, find that the statement does not match any of them. So, either way, we get our answer, meaning that the set of statements is decidable.
OK, but what exactly do we mean by decidable? As you will find in your studies on computability, it was Turing who operationalized the notion of systematic algorithms (computations) using his Turing-machines. Thus, be 'decidable' we typically mean 'Turing-machine-decidable'.
Another notion you are likely to run into in your studies on computability is recursiveness. There is a separate definition of what it means for a set to be a recursive set, and as it turns out, a a set is 'decidable' if and only if it is recursive.
A theory being axiomatizable means that there is a limited set of axioms from which all statements in that theory can be derived. By 'limited' we mean 'recursive', i.e. the set of axioms should be a decidable set.
The set of axioms from Q is decidable: given any statement, we can decide whether that statement is one of its axioms. This is because there are only finitely many axioms, and as we already saw, any finite set of statements is decidable.
Still, there can also be infinite sets that are decidable. The Peano Axioms, for example, is an infinite set of statements: besides a small number of axioms that are pretty much the same as $Q$, it also contains an infinite number of instances of an axiom schema called the axiom of induction. The Peano Axioms still are a decidable set though, since it is easy to verify whether some given statement is one of the basic axioms, or an instance of the axiom of induction.
Note that the claim that $Q$ is axiomatizable is a straightforward consequence of the fact that we defined $Q$ to be the set of statements that logically follow from its axioms, and the fact that that set of axioms is finite, and therefore a decidable set of statements.
For the theory of $Q$, things are quite different. Again, note that there are infinitely many theorems of $Q$. Now, as we saw, that does in and of itself not mean that that set is not decidable. But, in this case, infinity does rear its ugly head, and the theory of $Q$ turns out to be undecidable.
Since you're doing computability theory, let's make a connection with the halting problem: you probably already know that the halting problem is undecidable: there is no general algorithm that can always tell, for any given algorithm and input, whether that algorithm is going to eventually halt on that input or not. So: any algorithm on any input is either going to halt or not, but we don't always know whether it does or not.
OK, so now consider the question as whether or not some statement is a statement of the theory of Q. Since Q is axiomatizable, we know that there is an algorithm that, if the given statement is a theorem of Q, the algorithm will eventually say that it is: one such algorithm is to simply go through all possible first-order logic proofs (the set of which is enumerable, so we can indeed go theough those one by one), and see if it is a derivation of that statement starting with the axioms of Q.
Indeed, as such, we can say that theoremhood-of-Q is 'semi-decidable': if some given statement is a theorem of Q, then this algorithm will eventually tell us that that is so. And that is like the halting problem: if some algorithm with a given input will eventually halt, then we will eventually know that as well, simply by running that algorithm on that input.
However, what if this algorithm gets as input a statement that is not a theorem of Q? Then there exists of course no such proof, and that algorithm will never stop. And if it never stops, then it also does not tell us that it isn't a theorem, i.e. it is not a theorem, but we don't know that it is not a theorem. Of course, if we would know that the algorithm would never stop, then we would have our answer (answer: it is not a theorem), but we already know that we can't always know whether some algorithm will halt or not.
Ok, so that's the intuitive connection. Pleas note that this is not a proof that Q is not decidable: maybe there is some other algorithm that can tell for any theorem that it is a theorem and for any non-theorem that it is not a theorem... but as it turns out, there isn't: deciding whether or not something is a theorem turns out to be just as difficult as deciding whether some algorithm halts or not.