Is there an abstract logic that defines the mantle?

Question

It is a known result by Scott and Myhill that the second-order version of $L$ yields $\mathrm{HOD}$. Recently, Kennedy, Magidor, and Väänänen (Inner models from extended logics: Part I and II) investigated inner models given by logics with generalized quantifiers, which yields a logic intermediate between first-order and second-order logic. It motivates the following question:

Is there a logic that produces the mantle?

(Here the choice of the mantle is somewhat arbitrary; we may replace it by 'generic mantle', 'symmetric mantle' or whatever. I will focus on the mantle in this question, but I welcome discussing other cases.)

Of course, the answer is trivial if we assume, like $V=L$ or $V=L[G]$ for some $L$-generic $G$. I want to ask the existence of logic which defines the mantle uniform to models of ZFC.

Is there a (ZFC-definable) abstract logic $\mathcal{L}$ such that the inner model given by $\mathcal{L}$ is (ZFC-provably) the mantle?

(Under model-theoretic terms, is there $\mathcal{L}$ such that for any model $M$ of $\mathsf{ZFC}$, the inner model given by $\mathcal{L}$ is the mantle of $M$?)

Here are some of my rough thoughts:

• Sublogics of higher-order logics are not the candidate for $\mathcal{L}$: the corresponding inner models of higher-order logics are $\mathrm{HOD}$ (if my reasoning is correct), so the sublogics yield a submodel of $\mathrm{HOD}$. However, $\mathrm{HOD}$ need not be the mantle. (Theorem 70 of Fuchs, Hamkins, and Reitz (Set-theoretic geology).)

• We can rule out $\mathcal{L}_{\kappa\kappa}$, which yields Chang model. The inner model given by $\mathcal{L}_{\kappa\kappa}$ is the least transitive model of ZF that contains all ordinals and is closed under $<\kappa$-sequences (Theorem II of Chang's Sets constructible using $L_{\kappa\kappa}$.) However, the mantle need not be closed under $<\kappa$-sequences. (A generic extension of $L$ would be an example.)

I would appreciate any comments or answers.

Answer 1

Combining Goldberg's comment and Hamkins' answer seems to work. Especially, for any inner model $M$ of ZF, we have an abstract logic $\mathcal{L}$ whose corresponding inner model $L^\mathcal{L}$ is $M$.

Consider the sublogic of $\mathcal{L}_{\infty,\omega}$ such that infinite conjunction and disjunctions are only allowed to set of formulas in $M$. In fact, $\mathcal{L}=\mathcal{L}_{\infty,\omega}^M$.

Define $\psi_A$ for $A\in M$ as Hamkins defined: to repeat the definition, $$\psi_A(x):= \bigvee_{a\in A} (\forall v : v\in u\leftrightarrow \psi_a(u)).$$ Then $\psi_A(x)$ is a member of $M$ by induction on $A\in M$.

We can see that if $A\in M$, $A\subseteq V_\alpha^M$ then $$A=\{u\in V^M_\alpha \mid V^M_\alpha\models \psi_A(u)\}.$$

Hence the $\alpha$th hierarchy $L_\alpha^\mathcal{L}$ contains $V^M_\alpha$ (It can be shown by induction on $\alpha$.) Therefore $M\subseteq L^\mathcal{L}$. On the other hand, an inductive argument shows that the $\alpha$th hierarchy $L^\mathcal{L}_\alpha$ is a member of $M$ (we need the absoluteness of the satisfaction relation for $\mathcal{L}$ between $M$ and $V$), so $L^\mathcal{L}\subseteq M$.