With regard to the deeper motivation behind this question: I think there's some confusions around exactly how to interpret nonstandard models. I'm going to focus on the very narrow question, "Can models disagree about the computability of certain definable sets?"
The first step is realizing that this is a bit vague. There's at least three ways I can see to interpret it:
Interpretation 1 (Internal). You give me a formula in the language of arithmetic - viewed as a definition of a set - $\varphi(x)$. Each model $M$ of $PA$ yields a set $\varphi^M$. Now, $\varphi^M$ is a subset of $M$, not $\mathbb{N}$, but $M$ can't tell the difference. The sentence $\psi\equiv$"$\{x: \varphi(x)\}$ is decidable(=computable)" is expressible in the language of arithmetic, as $$\psi\equiv\exists e_0, e_1\forall x[(\varphi(x)\iff \exists sT(e_0, x, s))\wedge (\neg\varphi(x)\iff\exists sT(e_1, x, s))],$$ where $T$ is Kleene's $T$ predicate: $T(e, x, s)$ means "the $e$th Turing machine halts on input $x$ in $s$ steps."
Okay, fix $\varphi$. We can now ask:
Is there a model $M$ which satisfies $\psi$? $\neg \psi$?
Interpretation 2 (External). You give me a formula in the language of arithmetic - viewed as a definition of a set - $\varphi(x)$. Each model $M$ of $PA$ yields a set $\varphi^M$. Now, $\varphi^M$ is a subset of $M$, but the standard model $\mathbb{N}$ injects into $M$ in a canonical way; call this map "$i_M$." So we can talk about the standard natural numbers which ($M$ thinks) the statement $\varphi$ is true of; that is, the set $$X_M=i_M^{-1}(\varphi^M).$$ This set $X_M$ is a genuine set of natural numbers, and we can ask whether $X_M$ is: computable, infinite, coinfinite, of asymptotic density 1, etc. For instance, in the Goodstein example, $X_M$ is the set of standard natural numbers which $M$ thinks have halting Goodstein sequences.
This "cutting off" process might seem unnatural, but it's actually really mathematically interesting: it's what standard systems, for instance, are all about.
Okay, fix $\varphi$. We can now ask:
Is there a model $M$ such that $X_M$ is computable? Non-computable?
Interpretation 3 (Mix-and-match). As in interpretation 1, we look at the whole set $\varphi^M$. However, we now look at standard indices for computable functions, interpreted in $M$. Specifically, say $\varphi^M$ is mix-and-match-computable in $M$ if there is there some standard natural number $n$ such that $M$ thinks $\Phi_n$ is a total computable function such that $\Phi_n$ is the characteristic function of $\varphi^M$.
Okay fix $\varphi$. We can now ask:
Is there a model $M$ such that $\varphi^M$ is mix-and-match computable in $M$? Non-mix-and-match computable in $M$?
Despite the heterogeneous nature of this question, I suspect it too has its place in your intuition: basically, this question is asking, "Is there a genuine algorithm which, consistently, solves this problem?"
Now, what about your actual question? Well, we can exhibit formulas $\varphi$ such that there are models exhibiting divergent behavior in each of the three interpretations. This is actually pretty easy to do: we just shoehorn in some known undecidability. For instance, consider the formula $$\varphi(x)\equiv [\neg Con(PA) \wedge x\not=x]\vee[Con(PA) \wedge \exists s(T(x, x, s)].$$ In a model of $PA$ which thinks $PA$ is inconsistent, $\varphi$ just denotes the empty set, but in any model of $PA$ which thinks $PA$ is consistent - such as the standard one - $\varphi$ denotes that model's halting problem, which that model will think is incomputable. This might seem a bit trivial - it certainly does to me - but there's not an obvious way I can see to "carve out" such trivial solutions. (Maybe someone here can think of one!)
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
The idea is the same: let $f$ be total computable s.t. $f(\mathbb N)$ is not decidable, let $A$ be set of numbers $g(n) = 2^{2f(n)} + 2^{2f(n) + 2n + 3}$ and let $B$ be set of numbers $2^{2k + 1}$.
We can easily recover $n$ from $g(n)$ and compute $f$ on it, to check if some number is in $A$ or not.
We can prove that $2^{2k}$ is in $A - B$ iff $k = f(n)$ for some $n$.
Indeed, assume $2^{2p} = 2^{2q} + 2^{2q + 2r + 3} - 2^{2s + 1}$ for some $p,q,r,s$. We need to prove that $p = q$. Lets rewrite it as $2^{2p} + 2^{2s + 1} = 2^{2q} + 2^{2q + 2r + 3}$. Both left and right part written in binary have two non-zero digits, with only one on even position $2p$ and $2q$ correspondingly. As numbers are equal, this positions are equal.
So, we have that $(A - B) \cap \{2^{2k} | k \in \mathbb N|\}$ is undecidable, and thus $A - B$ is also undecidable.