Absoluteness of Satisfaction Relation for Models of the type $J_\alpha$ Is the satisfaction relation absolute between $J_\alpha \subseteq J_\beta$? That is, given a language $L$, a $L$-structures $M$, a formula $\varphi$, and $x$ which are all in $J_\alpha$, is it true that 
$J_\alpha \models (M \models \varphi(x)) \Leftrightarrow J_\beta \models (M \models \varphi(x))$
Does it make any difference if $M = (X, \in)$ where $X$ is a transitive set? 

In Kunen $\textit{Set Theory}$, he proves that the satisfaction relation is absolute for transitive models of $ZF - P$. He notes that it can also be proved in what he calls BST which includes extensionally, comprehension, union, pair, foundation, and the disjunction of the power set axiom and replacement. It is not clear to me that models of the form $J_\alpha$ or even $L_\alpha$ necessarily satisfy all these axioms. 
Thanks for any information on this question. 
 A: As with other theorems about the semantics of semantics (e.g. proving the upwards persistence of $\Sigma_1$ formulae) using two layers of satisfaction is helpful since it lets us look at the inner $\vDash$'s variable assignment itself. For simplicity we suppress the parameter and write $J_\alpha\vDash(M\vDash\phi)\leftrightarrow J_\beta\vDash(M\vDash\phi)$.
Proving the forwards direction: unravelling the definition of $\vDash$, we get the claim that if there exists a variable assignment $s$ such that $J_\alpha,s\vDash(M\vDash\phi)$, then $J_\beta\vDash(M\vDash\phi)$. Since $J_\alpha\subseteq J_\beta$, when working in the forward direction (i.e. $J_\alpha\vDash(M\vDash\phi)\rightarrow J_\beta\vDash(M\vDash\phi)$) we can take some assignment $s$ such that $J_\alpha,s\vDash(M\vDash\phi)$, by definition of $\vDash$ each witness $u(\mathsf v)$ for each variable symbol $\mathsf v$ should be in $M\subseteq L_\alpha$, so $J_\beta,s\vDash(M\vDash\phi)$. Then by definition of $\vDash$ we have $J_\beta\vDash(M\vDash\phi)$.
The backwards direction, $J_\beta\vDash(M\vDash\phi)\rightarrow J_\alpha\vDash(M\vDash\phi)$: unravelling one of the inside satisfaction relations, we get $J_\beta\vDash(\exists u(u\textrm{ is a var assignment}\land M,u\vDash\phi))\rightarrow J_\alpha\vDash(M\vDash\phi)$. We can reuse the variable assignment again here, but showing why we can is more difficult: being a variable assignment - i.e. being a function with finite range that's a subset of $M$ - is absolute between transitive models, so we don't need to worry about $J_\alpha$ not satisfying "$u$ is a variable assignment". Since $u$ is a variable assignment such that $M,u\vDash\phi$, we have $\textrm{ran}(u)\subseteq M$, and $M\subseteq J_\alpha$. Therefore for any variable symbol $\mathsf v$, we have $u(\mathsf v)\in J_\alpha$. Assuming all variable symbols in this language are also members of $J_\alpha$ (e.g. natural numbers), since $J_\alpha$ is closed under the Godel-operations we have $u\in J_\alpha$. So $J_\alpha\vDash(M,u\vDash\phi)$, completing this side of the proof.
