*(The original version of this question was much narrower and less natural; but see the edit history if interested.)*

****

Say that a **good logic** is a regular logic $\mathcal{L}$ containing $\mathsf{FOL}$ and having the finite use property and the strong downward Lowenheim-Skolem property together with, for each finite language $\Sigma$, an injection $i_\Sigma$ from the set of sentences $\mathcal{L}[\Sigma]$ to $\omega$ (I'll abbreviate $i=\{i_\Sigma:\Sigma$ a finite language$\}$). Using $i$ to conflate sentences with naturals appropriately, we can define an inner model $$M_\mathcal{L}^r:=L[r,\models_\mathcal{L}]$$ for each real $r$. Strong dLS (= "For every $X\subseteq\mathfrak{A}$ in a finite language there is a $\mathfrak{B}$ with $\vert\mathfrak{B}\vert\le X\cdot\aleph_0$ and $X\subseteq\mathfrak{B}\preccurlyeq_\mathcal{L}\mathfrak{A}$") ensures that we have a nice condensation phenomenon in the $M_\mathcal{L}^r$s, at least once $r$ is "strong enough" to code the relevant basic information, so these are in my opinion reasonably natural modifications of $L$ to consider.

Intuitively, due to the complexity of $i$ we might need the real $r$ to "unpack" things appropriately; for example, if we take $\mathcal{L}$ to be the "Tarski-Vaughtification" of second-order logic (see e.g. [here](https://mathoverflow.net/questions/387138/compactness-number-for-a-fragment-of-second-order-logic)) and use the obvious $i$ then we can really only hope for good behavior if we're given a real coding which second-order sentences are actually in $\mathcal{L}$. For this reason, I'm going to focus on the behavior of these models on a cone:

> **Definition**: The *ideal inner model theory* of a good logic $\mathcal{L}$ is the first-order theory $$\mathsf{IIMT}_\mathcal{L}:=\{\varphi\in\mathsf{FOL}[\{\in\}]: \exists r\forall s\ge_Tr M_\mathcal{L}^s\models\varphi\}.$$

Due to the on-a-cone focus, the specific "coding map" $i$ used will play no role.

[A secondary question](https://mathoverflow.net/questions/434670/very-l-like-models-part-2-combinatorics) focuses on combinatorics; here, I'm going to ask more specifically about large cardinals.

> **Question**: Is it consistent (relative to large cardinals) that there is a good logic $\mathcal{L}$ such that $\mathsf{IIMT}_\mathcal{L}$ contains "There is a measurable cardinal?"