Internal vs. external definability of inner models Suppose $\kappa$ is an inaccessible cardinal.  Is the following situation consistent?


*

*There is $p \in V_\kappa$ and a formula $\phi(x)$ such that there is exactly one $M \subseteq V_\kappa$ such that $M$ is a transitive set of size $\kappa$ and $M \models \phi(p)$.

*The $M$ above is not a definable class in $V_\kappa$, meaning there is no $q \in V_\kappa$ and formula $\psi(x,y)$ such that $M = \{ x \in V_\kappa : V_\kappa \models \psi(x,q) \}$.
 A: I will try to partially answer your question. I claim that if $\kappa$ is weakly compact then this situation is inconsistent: I will show that such an $M$ is necessarily definable in $V_\kappa$.
Define the finite set of formulae $\Lambda:=\{\phi(x)\} \cup \text{tc}(\phi(x))$, where tc denotes the transitive closure (with respect to the 'proper sub-formula' relation). Use reflection in $M$ to find a transitive $q \prec_{\Lambda} M$ such that $p \in q$ and $q \in M$.
For every $x \in V_\kappa$ we shall inductively construct a ${<}\kappa$-branching tree $T_x$. It will consist of sequences (always with a last element)  of transitive, $\Lambda$-elementary submodels containing $x$ and satisfying $\phi(p)$:
Set $\langle q \rangle$ to be the root of $T_x$. Assume that $\bar{y} \in T_x$ and $\bar{y}=\langle y_0, ... , y_\alpha\rangle$. Define the set of successors of $\bar{y}$ in $T_x$ as follows: $$\text{succ}_{T_x}(\bar{y}):=\{\bar{y}^{\frown} z \,\,\colon \,z \in V_{f(\bar{y})} \land y_\alpha \prec_{\Lambda} z  \land x, y_\alpha \in z \land z \, \text{is transitive} \, \}$$ where $f(\bar{y}):=\max(\vert y_\alpha \vert^+ , \vert x\vert^+)$. In the limit case let $(\bar{y}_\alpha)_{\alpha < \gamma}$ ($\bar{y}_\alpha$ has length $\alpha +1$) be an increasing chain and set $\bar{y}_\gamma:=\langle y_0,...,y_\alpha,... \rangle ^\frown y_\gamma$, where $y_\gamma:= \bigcup_{\alpha < \gamma} y_\alpha$.
I claim that $x \in M \Longleftrightarrow T_x \,\, \text{has height} \,\, \kappa$.
Assume that $x \in M$. Using reflection in $M$, Löwenheim-Skolem and Mostowski collapse (and $q \in M$) one can easily show that $T_x$ must have height $\kappa$.
On the other hand, assume that $T_x$ has height $\kappa$. Any branch through $T_x$ defines an increasing chain of transitive, $\Lambda$-elementary submodels. The direct limit of this chain is a transitive model $M' \subseteq V_\kappa$ of size $\kappa$, satisfying $\phi(p)$ and containing $x$. By your assumption $M'=M$ follows and so $x \in M$.
