A little while ago, I asked whether or not there could be a countable transitive model satisfying the same $ZFC$ theory as $V$ (assuming that we're working within some $V$, or (if you like) that there is a unique maximal universe of sets denoted by `$V$'). The answer was emphatically yes, in fact such a theory is given by Feferman. What we can do is add a constant symbol $M$ to the language of $ZFC$, and then add the following axioms:
(1) $M$ is countable and transitive.
(2) (Axiom Scheme) For every $\phi$ in the language of set theory (without $M$), $\phi \leftrightarrow \phi^M$.
This latter axiom has to be a scheme; if it were done with a single axiom we would violate Tarski's Theorem. However, the extensions is quite weak---it turns out to be a conservative extensions of $ZFC$ (by the Reflection Theorem). One can also get a similar effect with a truth predicate: we add a truth predicate, add Tarski's $T$-axioms, and then using reflection in the expanded language get a $V_\alpha$ which we then Skolemise and Collapse to get a countable transitive model that is an elementary substructure of $V$.
My question: Move to the case where we consider $MK$ class theory over $V$, a two-sorted first-order theory of sets and classes with an impredicative class comprehension scheme. Suppose we have a "philosophically acceptable" interpretation of the variables so we can give $MK$ its `full' semantics (or just work in a $(V_\kappa, \in, V_\kappa +1)$ with $\kappa$ inaccessible if you have foundational queasiness). Can we pull the same trick? i.e. Is the axiom system:
(1) $M$ is countable and transitive.
(2) (Axiom Scheme) For every $\phi$ in the language of $MK$ (without $M$), $\phi \leftrightarrow \phi^M$.
My worry: Insistence on the full semantics for $MK$ ensures that there's uncountably many sentences satisfied by $V$, and so you can't have such a countable transitive model; in any $(M, \in, C) \models MK$, $C$ is always countable.
Similarly, the truth predicate tactic seems dodgy; such a predicate is going to be third-order, not just second-order.
However, I'm mindful that I'm playing fast and loose here---$MK$ is still just a garden variety countable first-order language, so I wonder if there can be a countable transitive model that is an elementary substructure of $V$ as regards $MK$.
[EDIT: I should say more about what I'm interested in. This subdivides the question a bit:
Can there be such a $(M, \in , C)$ when $C$ is countable.
Can there be an elementary substructure of $V$ (either countable or uncountable) $(M, \in, C)$.
Sneaky aim: I'm trying to figure out whether there's a relevant difference (in either set-sized or countable structures) between having an elementary submodel of $V$ relative to $ZFC$ vs. relative to $MK$.]
Following up on my sketch in the comments, here's a proof that axioms (1) and (2) (where $\phi$ has no parameters) are conservative over $MK$ plus the choice schema:
(CC) $\forall x\exists X\phi(x, X) \to \exists Y\forall x\phi(x, Y_x)$
where $Y_x = \{y:\langle x, y\rangle\in Y\}$, and the $\omega$-dependent choice schema:
(DC) $\forall X\exists Y\phi(X, Y) \to \exists Z\forall n\in\omega\phi(Z_n, Z_{n+1})$
See Victoria Gitman's slides here for more details.
The idea is to construct a witness to (1) and (2) for any finite collection $\phi_0,...,\phi_n$ of formulas. In what follows I will assume that these formulas are closed under subformulas, and that they contain $\exists x(x = y)$, $\exists X(X = Y)$, $\exists x(x\in X \wedge x\not\in Y)$.
Let $\mbox{dom}(X) = \{x: \exists y\langle x, y\rangle\in X\}$ and $\mbox{rng}(X) = \{y: \exists x\langle x, y\rangle\in X\}$, and let $X^1 = \mbox{dom}(X)$ and $X^2 = \mbox{dom(rng}(X))$. Say that $X$ is a countable model if $X^1$ and $X^2$ are countable. In other words, $X$ codes a countable set domain $X^1$ and a countable class domain $\{\mbox{rng}(X)_y: y\in X^2\}$.
Now, suppose $X$ is a countable model. By CC, there is a $Y^{\exists x/X\phi_i}$ such that whenever $\vec{x}\in X^1$, $\vec{y}\in X^2$, and $\exists x/X\phi_i(x/X,\vec{x},\vec{\mbox{rng}(X)_y})$, then:
$\phi_i(Y^{\exists x/X\phi_i}_{\langle \vec{x}, \vec{y}\rangle}, \vec{x}, \vec{\mbox{rng}(X)_y})$
and otherwise $Y^{\exists x/X\phi_i}_{\langle \vec{x}, \vec{y}\rangle} = \emptyset$.
For simplicity, here and below I assume that when $\exists x/X\phi_i$ takes a set witness, $Y^{\exists x/X\phi_i}_{\langle\vec{x}, \vec{y}\rangle}$ is the corresponding set. Then let $Z$ be such that:
$Z^1 = \{Y^{\exists x/X\phi_i}_{\langle \vec{x}, \vec{y}\rangle}: \vec{x}\in X^1 \wedge \vec{y}\in X^2, \mbox{for $\exists x/X\phi_i$ that take set witnesses}\}$
$\mbox{rng}(Z) = \{\langle \langle \exists x/X\phi_i, \vec{x},\vec{y}\rangle, z\rangle: z\in Y^{\exists x/X\phi_i}_{\langle \vec{x}, \vec{y}\rangle}, \mbox{for $\exists x/X\phi_i$ that take class witnesses}\}$
So $Z$ is a countable model closed under witnesses for the $\phi_i$ with parameters from $X$. From DC, it the follows that there is a countable sequence $Y$ of countable models such that $Y_0 = \emptyset$ and $Y_{n+1}$ is closed under witnesses for the $\phi_i$ with parameters from $Y_n$. Given such a sequence, let $Z$ be such that:
$Z^1 = \bigcup_{n\in\omega} Y^1_n$
$\mbox{rng}(Z) = \{\langle \langle n, x\rangle, y\rangle: \langle x, y\rangle\in \mbox{rng}(Y_n)\}$
It is then straightforward to verify that $Z$ is a countable model closed under witnesses for the $\phi_i$ for its parameters. It follows that $\phi_i^Z$ iff $\phi_i$ for parameters from $Z$ (where $\phi_i^Z$ is the result of restricting set quantifiers in $\phi_i$ to $Z^1$ and class quantifiers to $\{\mbox{rng}(Z)_y: y\in Z^2\}$). Finally, note that for the countable set model $M = \langle Z^1, \{Z^1\cap \mbox{rng}(Z)_y: y\in Z^2\}\rangle$, we have:
$M\vDash \phi_i(\vec{x},\vec{Z^1\cap \mbox{rng}(Z)_y})$ iff $\phi_i^Z(\vec{x},\vec{\mbox{rng}(Z)_y})$
It follows that the countable transitive collapse of $M$, $M'$, is elementarily equivalent to $V$ for sentences among the $\phi_i$. So $M'$ is our desired witness to (1) and (2).