It is a well-known fact that while while Robinson arithmetic can interpret surprisingly strong theories, it cannot interpret $\mathsf{I}\Delta_0 + \mathrm{Exp}$, i.e., Peano arithmetic with induction restricted to $\Delta_0$ formulas together with an axiom stating that $2^x$ is a total function. This is a consequence of (a generalization of) Gödel's second incompleteness theorem and the fact that $\mathsf{I}\Delta_0 + \mathrm{Exp}$ interprets $\mathsf{I}\Delta_0 + \Omega_1 + \mathrm{Con}(\mathsf{Q})$ (where $\mathsf{Q}$ is of course Robinson arithmetic).
There is a broader notion of interpretation that is occasionally useful in relative consistency proofs, which is that of a forcing interpretation more literally known as a Kripke model. Kripke models are naturally thought of as semantics for intuitionistic logic, but through the double negation translation (which is implicitly used in e.g. set theoretic forcing), you can extract a consistent classical theory from a consistent intuitionistic theory.
It's clear that sufficiently smart theories such as $\mathsf{PA}$ (and probably $\mathsf{I}\Sigma_1$, although I am pretty far from an expert) are smart enough to show that for any given classical theory $T$, $\mathrm{Con}_{\mathrm{Int}}(T^{\neg\neg}) \to \mathrm{Con}(T)$, where $\mathrm{Con}_{\mathrm{Int}}$ denotes the consistency of an intuitionistic theory and $T^{\neg\neg}$ denotes the double negation translation of the classical theory $T$. I feel that this should yield a (possibly inefficient) proof that $\mathsf{PA}$ does not interpret a Kripke model of the double negation translation of $\mathsf{PA}+ \mathrm{Con}(\mathsf{PA})$, for instance, but it is entirely unclear to me that this reasoning goes through in the weaker context of $\mathsf{I}\Delta_0$ and other theories interpretable in $\mathsf{Q}$. It is also entirely possible that this is sensitive to the particular choice of proof system, as these things often are.
So all of this raises the question in my title.
Question. Does $\mathsf{Q}$ interpret a Kripke model of the double negation translation of $\mathsf{I}\Delta_0 + \mathrm{Exp}$?
I suspect that the answer is no, but assuming I am correct, I would like to know at least a sketch of a proof of this.
EDIT: Recall that a Kripke frame for the first-order language $\mathcal{L}$ is a partial order $(W, \leq)$ together with a family $\{M_w\}_{w\in W}$ of $\mathcal{L}$-structure such that for any $u$ and $v$ in $W$, if $u\leq v$, then $M_u$ is a subset of $M_v$ such that the inclusion map is a homomorphism (i.e., the interpretations of functions agree and for any relation symbol $R$, if $M_u \models R(\bar{a})$, then $M_v \models R(f(\bar{a}))$).
Given a Kripke frame $F = (W,\leq, \{M_w\}_{w \in W})$ and a first-order structure $A$, an interpretation of $F$ in $A$ consists of
a formula $\delta_W(\bar{x})$ in $n$ variables,
a bijection $f$ from the set of $n$-tuples satisfying $\delta_W$ to $W$,
a formula $\rho_{\leq}(\bar{x},\bar{y})$ in $2n$ variables such that for any $n$-tuples $\bar{a}$ and $\bar{b}$, $A \models \rho_{\leq}(\bar{a},\bar{b})$ if and only if $f(\bar{a}) \leq f(\bar{b})$,
a formula $\delta_M(\bar{z})$ in $m$ variables,
a function $g$ from the set of $m$-tuples satisfying $\delta_M(\bar{z})$ to $\bigcup_{w \in W} M_w$,
a formula $\kappa(\bar{x},\bar{z})$ in $n+m$ variables such that for any $\bar{a}$ in the domain of $f$ and $\bar{b}$ in the domain of $g$, $A \models \kappa(\bar{a},\bar{b})$ if and only if $g(\bar{b}) \in M_{f(\bar{a})}$,
for each $k$-ary function symbol $h$ in $\mathcal{L}$, a formula $\varphi_f(\bar{z}_0,\dots,\bar{z}_{k})$ in $(k+1)\cdot m$ variables such that for any $k+1$ $m$-tuples $\bar{a}_0,\dots,\bar{a}_k$ in the domain of $g$, $A \models \varphi_f(\bar{a}_0,\dots,\bar{a}_k)$ if and only if there is some $w \in W$ such that $M_w$ contains each of $f(\bar{a}_0),\dots,f(\bar{a}_k)$ and $M_w \models h(f(\bar{a}_0),\dots,f(\bar{a}_{k-1})) = f(\bar{a}_k)$ (note that if such a $w$ exists, then this is independent of the particular choice of $w$), and
for each $k$-ary relation symbol $R$ in $\mathcal{L}$, a formula $\varphi_R(\bar{z}_0,\dots,\bar{z}_{k-1},\bar{x})$ in $k\cdot m + n$ variables such that for any $\bar{a}_0,\dots,\bar{a}_{k-1}$ in the domain of $g$ and $\bar{b}$ in the domain of $f$, $A \models \varphi_R(\bar{a}_0,\dots,\bar{a}_{k-1},\bar{b})$ if and only if $g(\bar{a}_0),\dots,g(\bar{a}_{k-1})$ are all in $M_{f(\bar{b})}$ and $M_{f(\bar{b})}\models R(g(\bar{a}_0),\dots,g(\bar{a}_{k-1}))$.
This is just an interpretation in $A$ of $F$ encoded as a first-order structure in a particular way. We say that a classical theory $T$ has a forcing interpretation (I don't know how standard this term is) of an intuitionistic theory $S$ if every model $M$ of $T$ interprets a Kripke frame model $F$ of $S$ in a uniform way (i.e., witnessed by the same collection of formulas). That said, if it is true that every model $M$ of $T$ interprets a Kripke frame model $F$ of $S$ (with no uniformity assumption), then by a compactness argument we can show that there actually is a uniform forcing interpretation of $S$ in $T$.
By a tedious but easy induction, it is possible to show that for any $\mathcal{L}$-formula $\varphi(\bar{w})$ with $\bar{w}$ a $k$-tuple, there is a formula $\psi(\bar{z}_0,\dots,\bar{z}_{k-1},\bar{x})$ in the language of $A$ with $\bar{z}_0,\dots,\bar{z}_{k-1}$ $m$-tuples and $\bar{x}$ an $n$-tuple such that for any $m$-tuples $\bar{a}_0,\dots,\bar{a}_{k-1}$ in the domain of $g$ and $n$-tuple $\bar{b}$ in the domain of $f$, $f(\bar{b})\Vdash \varphi(g(\bar{a}_0),\dots,g(\bar{a}_{k-1}))$ if and only if $A \models \psi(\bar{a}_0,\dots,\bar{a}_{k-1},\bar{b})$. Furthermore, this conversion is very simple given the data of the interpretation. You just unravel the recursive definition of satisfaction in a Kripke frame.
So in this way, a forcing interpretation of $S$ in $T$ gives a computable reduction of $S$ to $T$ (if the languages involved are finite, otherwise we need to assume stuff about the complexity of the assignments of formulas to the non-logical symbols in $\mathcal{L}$) in a way that proves $\mathrm{Con}(T)\to \mathrm{Con}(S)$ in a sufficiently smart theory such as $\mathsf{PA}$.
