Can this semi-constructible structure satisfy existence of a measurable cardinal?

Question

If we add a primitive unary function symbol $\mathfrak L$ to the first order language of set theory.

Axiom of semi-constructibility: if $\phi^\alpha (y,x_1,\ldots,x_n)$ is a formula in which all and only the symbols $y,x_1, \ldots, x_n,\alpha$ occur free, also none of them occur as bound, that has all of its quantifiers bounded by $\mathfrak L_\alpha$, and $\alpha$ only occur in the bounds (i.e. the $\mathfrak L_\alpha$'s) ; then:

$\forall x_1 \in \mathfrak L_\alpha ,\ldots, \forall x_n \in \mathfrak L_\alpha: \{y \in \mathfrak L_\alpha \mid \phi^\alpha (y,x_1,\ldots,x_n)\} \in \mathfrak L_{\alpha+1}$

Also, add the following axioms:

$\mathfrak L_\lambda = \bigcup_{\alpha < \lambda} \mathfrak L_\alpha \text { for every limit ordinal } \lambda \\ \mathfrak L_{\alpha+1} \subset \mathcal P(\mathfrak L_\alpha)\\ L_{\alpha+1} \cap \mathfrak L_\alpha = L_\alpha \\ |\mathfrak L_{\omega+\alpha+1} |= |\mathfrak L_{\omega +\alpha}| \\ \mathfrak L_\omega = L_\omega $

Where $L_\alpha$ refers to the ordinary $\alpha$ constructible stage.

Define: $\mathfrak L = \bigcup \mathfrak L_\alpha$.

Now is $\sf ZFC + [V=\mathfrak L]$ consistent with existence of a measurable cardinal?

The point is that each $\mathfrak L_\alpha$ for an infinite $\alpha$ is not necessarily $L_\alpha$, it may contain non-constructible subsets of the prior stage, but there is a restrain on how many those can be that the cardinality of an infinite successor $\mathfrak L_\alpha$ is the same as that of the prior stage. This theory proves the Generalized Continuum Hypothesis, and may prove many other theorems of $\sf ZFC + [V=L]$. It is not clear to me if that restriction on the cardinality of successor stages may handicap the ability to get a model of this theory that satisfy the existence of a measurable cardinal.

Answer 1

No. Under the hypotheses, there are limit ordinals $\eta$ such that $\mathcal{P}(\eta)\cap L\subseteq\mathfrak{L}_{\eta+1}$, and therefore, for example, $L_{\eta+2}\cap\mathfrak{L}_{\eta+1}\neq L_{\eta+1}$, contradicting one of the requirements at $\alpha=\eta+1$. For e.g. let $\beta$ be such that $0^\sharp\in \mathfrak{L}_\beta$, and let $\eta>\beta$ be such that $V_\eta=\mathfrak{L}_\eta$ and $V_\eta\preccurlyeq_2 V$. Then for every $X\in\mathcal{P}(\eta)\cap L$, we have $X\in\mathfrak{L}_{\eta+1}$, because $X$ is easily enough definable from the parameter $0^\sharp$ over $V_\eta$. (So we must have $X\in\mathfrak{L}_{\eta+1}$ by the Axiom of semi-constructibility.)

As mentioned in Joel Hamkins's answer, if we drop the requirement that $L_{\alpha+1}\cap\mathfrak{L}_\alpha=L_\alpha$, then it is consistent. And aside from Hamkins's answer on this, Asaf Karagila's comments mentioned $L[U]$ (where $U$ is a normal measure), which also satisfies the weaker system.

Answer 2

Update. This answer is not correct, because it is a subtler matter to ensure that the levels are closed under relative constructibility while also maintaining $L_{\alpha+1}\cap\mathfrak{L}_\alpha=L_\alpha$. This answer works, however, if one should drop that requirement.

Two observations.

First, every model of ZFC with global choice can interpret a predicate making your theory true, and so yes, this theory is consistent with any of the usual ZFC large cardinal notions.

The reason is that with global choice, we can simply gradually put more and more sets into the $\mathfrak{L}_\alpha$ hierarchy, in such a way that obeys your requirements and such that every set will eventually appear.

But second, in fact every model of ZFC has a class forcing extension satisfying your theory, without adding sets. We can take as conditions in the forcing a specification of $\mathfrak{L}_\alpha$ up to some ordinal, satisfying your requirements so far. And we generically extend it taller. This forcing is $\kappa$-closed for every $\kappa$, and so it adds no sets, but it adds your pseudo-constructible hierarchy.