Is there a c.e. theory $T⊢\text{ZFC}$ in the language of set theory such that the minimum transitive model of $T$ exists but does not satisfy $V=L$?


You may assume that ZFC has transitive models. Note that $M$ is minimal iff $∀M' \, M'⊈M$ and minimum iff $∀M' \, M'⊇M$.


It may be tempting to consider ZFC + $0^\#$ (assuming large cardinal axioms), but while this theory has a minimum inner model (i.e. $L[0^\#]$), it has incomparable minimal transitive models. Model comparability uses iterability, but transitiveness does not suffice for iterability. Moreover, for every c.e. $T⊢\text{ZFC\P}+0^\#$ having a model $M$ with $On^M = α < ω\_1$, the intersection of all such $M$ equals $L\_α$, and furthermore a subset of $L\_α$ is definable (with parameters) in all such $M$ iff it is in $L\_{α^{+,\mathrm{CK}}}$. To see this (briefly), $0^\#$ allows $M$ to 'continue' $L$ beyond $α$, and $L\_{α^{+,\mathrm{CK}}}⊆(L\_{α^{+,\mathrm{CK}}})^M$ (the well-founded part of any model of KP being admissible), and so $L\_{α^{+,\mathrm{CK}}}∩V\_α=L\_α$. Also, existence of $M$ is $Σ^1\_1(α)$, so the intersection of all $M$ is at most $L\_{α^{+,\mathrm{CK}}}$.


A minimum transitive model of ZFC + $A$ for a *statement* $A$ cannot be produced through set forcing either. Also, I think that minimal models need not satisfy $V=HOD$; not sure about minimum models.


Thus, minimum transitive models usually either satisfy $V=L$ or do not exist. However, I suspect that exceptions exist, including in the form $L\_α[r]$ with $r∈ℝ$, but require an interesting coding argument. Perhaps there is such an $r$ computable from the theory of the least transitive model of ZFC $L\_α$, with $r$ self-verifying (in $L\_α[r]$) and yet weak enough for $L\_α[r]⊨\text{ZFC}$.


*Update:* I accepted Farmer Schlutzenberg's positive answer (see also the partial answers by Hamkins and Enayat). A remaining open problem is whether such a $T$ can be obtained by extending ZFC with a single statement.



Minimum transitive models and V=L
Yes, I claim you can in fact get one whose minimum model is a set forcing extension of a segment of $L$. Let $L\_\alpha$ be least modelling ZFC. Let $\mathbb{P}=\mathbb{P}^{L\_\alpha}$ be Jensen's forcing for adding a $\Pi^1\_2$-singleton, as defined over $L\_\alpha$; ZFC proves that forcing with $\mathbb{P}^L$ over $L$ adds a unique $L$-generic filter. Working in $V$, define the sequence $\left<p\_n\right>\_{n<\omega}$ through $\mathbb{P}$, which will be $L\_\alpha$-generic, as follows. Fix a recursive enumeration $\left<\varphi\_k\right>\_{k<\omega}$ of all formulas in the language of set theory in one free variable. Now let $p\_0=\emptyset$. Suppose we have defined $p\_n$. Let $\alpha\_n$ be the least $\beta$ such that $L\_\beta\preccurlyeq\_{\Sigma\_n}L\_\alpha$. Let $p\_{n+1}$ be the least $p\in\mathbb{P}$ such that $p\leq p\_n$ and $p$ is in all open dense subsets $D$ of $\mathbb{P}$ which are defined over some $L\_{\alpha\_i}$ by $\varphi\_j$, for some $(i,j)$ with $i,j\leq n$. (That is, for some such $(i,j)$, $D$ is the unique $D'\in L\_{\alpha\_i}$ such that $L\_{\alpha\_i}\models \varphi\_j(D')$.) This $p$ exists since there are only finitely many dense sets we consider here. This defines the sequence.


Let $G$ be the filter generated by $\left<p\_n\right>\_{n<\omega}$.
Since $L\_\alpha$ is pointwise definable, $G$ is $L\_\alpha$-generic. So $L\_\alpha[G]\models$ ZFC.


Now let $T$ be the following recursive (not just r.e.) theory extending ZFC, which will correspond to the construction above: for $n<\omega$ let $T\_n$ be ZFC + "$V=L[g]$ for some $(L,\mathbb{Q})$-generic filter $g$, where $\mathbb{Q}$ is Jensen's forcing in $L$, and defining $q\_n$ with respect to $L$ as in the construction above, we have $q\_n\in g$". (That is, note that there is a recursive sequence $\left<\psi\_n\right>\_{n<\omega}$ of formulas such that for each $n$, we have that $p\_n$ is the unique $p\in L\_\alpha$ such that $L\_\alpha\models\psi\_n(p)$. Have $T\_n$ assert that there is $q\in g$ (where $g$ is as above) such that $L\models\psi\_n(q)$. Thus, the sequence $\left<T\_n\right>\_{n<\omega}$ is recursive. Of course, the complexity of $\psi\_n$ increases with $n$. Note that the "$g$" is a bound variable, not some new constant, so I am working with only the language of set theory.) Now set $T=\bigcup\_{n<\omega}T\_n$. So $T$ is recursive.


Claim: $L\_\alpha[G]$ is the minimum transitive model of $T$.


Proof: Let $P$ be any transitive model of $T$. Then certainly $L\_\alpha\subseteq P$, and easily if $\alpha<\mathrm{OR}^P$ then $L\_\alpha[G]\subseteq P$. So we may assume $\alpha=\mathrm{OR}^P$. So $L^P=L\_\alpha$. But then letting $G'$ be the (unique) $(L\_\alpha,\mathbb{P})$-generic filter such that $P=L\_\alpha[G']$, we get $p\_n\in G'$ for each $n<\omega$, since $P\models T\_n$ for each $n$. But therefore $G'=G$, so $P=L\_\alpha[G]$, which suffices.


Remark: This construction is somewhat related to that for Proposition 34 of "On a Conjecture Regarding the Mouse Order for Weasels", arXiv:2207.06136, joint with Jan Kruschewski; (that proposition is stated rather generally, but in its simplest instantiation it gives an example of $G$ which is (only just) Cohen generic over $L\_{\omega\_1^{\mathrm{ck}}}$ but with KP failing in $L\_{\omega\_1^{\mathrm{ck}}}[G]$).


Remark 2: The question is rather related to a question of Harvey Friedman's, on which Woodin and Koellner made recent (boldface) progress. The question was (if I recall it precisely) whether there can be an ordinal $\alpha$ and a *single sentence* $\varphi$ such that there is a unique transitive model $M$ such that $\mathrm{OR}^M=\alpha$ and $M\models$ ZFC + "$V\neq L$" + $\varphi$. It was already known that any such model must satisfy "$0^\sharp$ does not exist", and I think also that it must satisfy "$V=\mathrm{HOD}$".


