I've noticed that recently you have asked a few questions about my work, and so let me thank you; you are kind to take an interest.
This particular question can be seen as part of the subject of set-theoretic potentialism, which my co-author Øystein Linnebo and I recently investigated in our paper:
In that paper, we consider several different notions of set-theoretic accessibility, as below, from forcing accessibility to Grothendieck-Zermelo potentialism to rank extensions or transitive extensions or submodel potentialism and others.
In each case, for each concept of accessibility we determine the corresponding modal logic of that concept of potentialism. In other related work, W. Hugh Woodin and I recently looked at the case of top-extensional set-theoretic potentialism, proving that the modal logic is S4.
(You may also be interested in my more philosophical remarks on this topic at the end of my paper, The modal logic of arithmetic potentialism and the universal algorithm.)
Nevertheless, despite all that, I am very sorry to say that none of these cases are exactly the case you asked about, which is outer-model accessibility. Outer-model potentialism is certainly a natural case of potentialism, and so let me try to tell you what I know about it. Like forcing potentialism, this would be a case of width potentialism and height actualism, since outer models increase only the width of the universe and not the height.
First, let us fix a countable model of ZFC plus V=L, say, and consider it in the context of all its outer models. Since we can force so as to destroy any stationary set in this model, while preserving others, we see that there is an infinite family of independent buttons, "the $n^{th}$ stationary set in the $L$-least partition of $\omega_1^L$ is no longer stationary." This can be made true in an outer model (by forcing) and once true, remains true in all further outer models; and the statements can be controlled independently. And since we also have a family of independent switches arising from the GCH patterns, it follows by the main modal logic analysis (as in Structural connections...), it follows that the modal logic of outer-models is contained within S4.2. And it certainly contains S4, because it is reflexive and transitive.
So the answer to your question this a modal logic between S4 and S4.2.
I don't actually know which side it will end up on, or if it will end up strictly between, and I think this is a good question.
If you hope to prove that the model logic is S4.2, then usually one does this by proving an directedness or amalgamation theorem. The problem here, however, is that we already know that outer model possibility is not directed, since you can move from a model to outer models in incompatible ways that cannot be amalgamated (this is due to Mostowski). So that avenue of showing (.2) is valid is closed off. I don't know if (.2) is valid for this notion of possibility or not, but I am inclined against it. I think there will be fundamentally incompatible possibily necessary statements, which is to say, railway switches, and this will be incompatible with S4.2.
If you hope to prove that only S4 is valid, then you could follow some of the recent work on the universal algorithm and universal finite sets. The general consequence of the existence of these finite sequences with the universal extension property is that they cause the existence of railyard labelings, which then cause the modal logic to be contained in S4. I don't know if there is any universal finite sequence phenomenon for outer models, and this also is an interesting question.
So I believe that the exact modal logic of outer-model potentialism is an open question.
Yes, the minimal transitive model of ZFC is pointwise definable.
The minimal transitive model of ZFC, known as the Shephardson-Cohen model, is the model $\langle L_\alpha,\in\rangle$, where the ordinal $\alpha$ is smallest such that this is a model of ZFC.
Let me make a few observations about it.
The minimal model is not only minimal, but least. That is, if $M$ is any transitive model of ZFC, then the constructible universe $L^M$ of that model will also be a model of ZFC and have the form $L_\gamma$, and so the minimal model $L_\alpha$ will be contained within it.
It follows that the minimal transitive model of ZFC exists if and only if there is a transitive model of ZFC.
The minimal model might not exist — it is consistent with ZFC that there is no transitive model of ZFC. For example, in the minimal model $L_\alpha$ itself, there is no element that is a transitive model of ZFC. So it is consistent with ZFC that the minimal model does not exist.
The existence of the minimal transitive model of ZFC has some mild consistency strength. If there is a transitive model $M$ of ZFC, then of course Con(ZFC) must hold. But since the model is transitive, we get Con(ZFC) holding inside $M$, and so Con(ZFC+Con(ZFC)) holds. But then this holds also inside $M$, and so Con(ZFC+Con(ZFC+Con(ZFC))) holds, and so on. One can iterate this process transfinitely. So the existence of the minimal model implies a tower of iterated consistency statements transcending ZFC.
Theorem. The minimal transitive model of ZFC is pointwise definable.
Proof. Suppose that $L_\alpha$ is the minimal transitive model of ZFC. This model satisfies $V=L$ and consequently has a definable global well ordering of the universe. This implies that the model has definable Skolem functions, picking out the least witness for any existential property. The set of definable elements of $L_\alpha$ is therefore closed under Skolem witnesses and is therefore an elementary substructure of $L_\alpha$. By condensation, this collection is isomorphic by the Mostowski collapse to a model $L_\beta$, which must be a model of ZFC, and which furthermore is pointwise definable, since we had included only definable elements. Since $\beta\leq\alpha$, it follows by minimality that $\beta=\alpha$. And so $L_\alpha$ is pointwise definable. $\Box$
If one equips the minimal transitive model of ZFC with all its definable classes, then one achieves a minimal transitive model of Gödel-Bernays GBC set theory.
Meanwhile, Kameryn Williams proved in his dissertation result that there is no minimal transitive model of Kelley-Morse set theory.
The forcing paper you mention is the following, where we proved that every countable model of ZFC and indeed GBC has a class forcing extension that is pointwise definable:
Best Answer
An infinite set (or class) of ordinals is said to be immune if it neither contains nor is disjoint from any infinite constructible subset of its supremum. The main result of the paper reads as follows: There exists an immune class of ordinals in a cardinal-preserving and GCH-preserving class generic extension of L.