*Throughout, we work in the class theory $\mathsf{MK}$ (although I'm open to tweaking this), "logic" means "set-sized logic whose semantics is definable over $V$," and "$\mathcal{J}\approx\mathcal{K}$" means that the logics $\mathcal{J}$ and $\mathcal{K}$ are equivalent in the sense that for every $\mathcal{J}$-sentence $\varphi$ there is a $\mathcal{K}$-sentence $\psi$ with the same model class and conversely.*

****

I'm interested in two (types of) transformations of logics:

First, we have the various **infinitarizations**. Given a regular cardinal $\kappa$ and a logic $\mathcal{J}$, let $\mathbb{I}_\kappa(\mathcal{J})$ be the smallest logic containing $\mathcal{J}$ and closed under Boolean combinations of size $<\kappa$ and quantification over tuples of size $<\kappa$. And, given a *singular* cardinal $\lambda$, let $\mathbb{I}_\lambda(\mathcal{J})=\bigcup_{cf(\kappa)=\kappa<\lambda}\mathbb{I}_\kappa(\mathcal{J})$. Note that we have $\mathbb{I}_{\kappa_0}\circ\mathbb{I}_{\kappa_1}=\mathbb{I}_{\max\{\kappa_0,\kappa_1\}}$.

Second, we have **modalization**. Given a logic $\mathcal{J}$, let $\mathbb{M}(\mathcal{J})$ be the smallest logic $\mathcal{K}$ such that $\mathcal{J}\subseteq\mathcal{K}$ and, for every $\mathcal{K}$-sentence $\varphi$, there is a $\mathcal{K}$-sentence $\Box\varphi$ with the property that for every structure $\mathfrak{A}$ we have $\mathfrak{A}\models_\mathcal{K}\Box\varphi$ iff $\mathfrak{B}\models_\mathcal{K}\varphi$ for every $\mathfrak{B}$ containing $\mathfrak{A}$ as a substructure.

By an argument$^1$ similar to the proof of the [Los-Tarski theorem](https://en.wikipedia.org/wiki/%C5%81o%C5%9B%E2%80%93Tarski_preservation_theorem), we have $\mathbb{M}(\mathbb{I}_{\theta}(\mathsf{FOL}))\approx\mathbb{I}_{\theta}(\mathsf{FOL})$ whenever $\theta$ is a limit of strongly compact cardinals, giving a conditional answer to Questions 57/58 of [Hamkins/Woloszyn](https://arxiv.org/abs/2009.09394). Moreover, assuming Vopenka's Principle the same argument can be extended to arbitrary logics, yielding the following:

> $(\star)$ For every logic $\mathcal{J}$ and every infinite cardinal $\kappa$ there is a logic $\mathcal{K}$ such that $\mathcal{J}\le\mathcal{K}$ and $$\mathcal{K}\approx\mathbb{M}(\mathcal{K})\approx\mathbb{I}_\kappa(\mathcal{K}).$$ 

This uses [Makowsky's theorem](https://www.jstor.org/stable/2273786?seq=1) that VP implies the existence of strong compactness numbers for all logics. Moreover, there is some heuristic evidence (namely [this MO answer of Trevor Wilson](https://mathoverflow.net/a/377527/8133)) that we can't replace VP with anything weaker unless we find a genuinely different line of attack. My question is whether this is in fact the case:

> Over the base theory $\mathsf{MK}$, does $(\star)$ have any nontrivial consistency strength?

****

$^1$For completeness, let me sketch the argument mentioned above; I can add details if anyone is interested.

Suppose $\theta$ is a limit of strongly compact cardinals and $\varphi\in\mathcal{L}_{\theta,\theta}$; I'll show that $\Box\varphi$ is semantically equivalent to an $\mathcal{L}_{\theta,\theta}$-sentence (the rest of the argument is a routine induction on complexity, and a rephrasing of this paragraph to be about *formulas* rather than *sentences*). Let $\kappa$ be a strongly compact cardinal such that $\theta\in\mathcal{L}_{\kappa,\kappa}$, and let $\mathbb{S}$ be the set of $\mathcal{L}_{\kappa,\kappa}$-sentences which are purely existential and inconsistent with $\neg\varphi$. The disjunction $\sigma:=\bigvee\mathbb{S}$ is again an $\mathcal{L}_{\theta,\theta}$-sentence; I claim $\sigma$ is semantically equivalent to $\Box\varphi$. Trivially $\mathfrak{A}\models\sigma\implies\mathfrak{A}\models\Box\varphi$. In the other direction, suppose $\mathfrak{B}\models\Box\varphi$. Then the atomic diagram of $\mathfrak{B}$ is inconsistent with $\neg\varphi$. By strong compactness of $\kappa$, this means that there is a subset of the atomic diagram of $\mathfrak{B}$ of cardinality $<\kappa$ which is inconsistent with $\neg\varphi$. But this means $\mathfrak{A}\models\sigma$.