[proofplan] The point is to separate the external ultrapower construction carried out in $V$ from an internal construction available to $L$. If $L$ could define the predicate $A \mapsto A \in U$ on its own subsets of $\kappa$, then Separation inside $L$ would collect exactly the constructible subsets of $\kappa$ that belong to $U$. That collected set is precisely $U^L$, contradicting the hypothesis $U^L \notin L$. To rule out indirect definitions of the ultrapower data, we reduce the predicate $A \mapsto A \in U$ to the $U$-equivalence and $U$-membership relations using characteristic functions of constructible subsets of $\kappa$. Thus any internal definition of either relation would again define $U^L$, contradicting $U^L \notin L$. [/proofplan] [step:Assume that $L$ defines the restriction of $U$ to its subsets of $\kappa$] Assume toward contradiction that there are a first-order formula $\varphi(x,y)$ in the language of set theory and a parameter $a \in L$ such that, for every $A \in \mathcal P(\kappa)^L$, $L \models \varphi(A,a)$ if and only if $A \in U$. Let $X := \mathcal P(\kappa)^L = \{A \in L : A \subseteq \kappa\}$. Since $L$ is a model of the power set axiom internally, $X$ is the power set of $\kappa$ as computed in $L$, and hence $X \in L$. [/step] [step:Use Separation inside $L$ to collect the definable part of the measure] Because $L$ is a model of ZFC and $X,a \in L$, apply the Separation axiom schema inside $L$ to the set $X$, the parameter $a$, and the formula $\varphi(x,a)$. Viewed externally from $V$, this gives a set $Y \in L$ such that $Y = \{A \in X : L \models \varphi(A,a)\}$. By the assumed definition of the predicate $A \mapsto A \in U$ on $X$, for every $A \in X$ we have $A \in Y$ if and only if $A \in U$. Therefore $Y = U \cap X = U \cap \mathcal P(\kappa)^L = U^L$. Thus $U^L = Y \in L$, contradicting the hypothesis $U^L \notin L$. [guided] We now use the fact that definability over $L$ from parameters in $L$ is usable by the axioms of $L$ itself. The set to which Separation will be applied is $X := \mathcal P(\kappa)^L$. This is not an external proper class: it is the power set of $\kappa$ as computed by $L$, so $X \in L$. The assumed definition says that the formula $\varphi(x,a)$ exactly recognizes membership in the external measure $U$ when its input is a constructible subset of $\kappa$. In symbols, for every $A \in X$, $L \models \varphi(A,a)$ if and only if $A \in U$. Since both $X$ and $a$ belong to $L$, Separation inside $L$ forms the subset of $X$ cut out by $\varphi(x,a)$. Define $Y := \{A \in X : L \models \varphi(A,a)\}$. The Separation axiom schema in $L$ gives $Y \in L$. Now identify $Y$. For $A \in X$, the definition of $Y$ gives $A \in Y$ if and only if $L \models \varphi(A,a)$. The assumed correctness of $\varphi$ gives $L \models \varphi(A,a)$ if and only if $A \in U$. Combining the two equivalences, for every $A \in X$, $A \in Y$ if and only if $A \in U$. Hence $Y$ is exactly the collection of constructible subsets of $\kappa$ that lie in $U$: $Y = U \cap X = U \cap \mathcal P(\kappa)^L = U^L$. Since $Y \in L$, this implies $U^L \in L$, contradicting the hypothesis. [/guided] [/step] [step:Recover the external measure predicate from any internal definition of the ultrapower relations] The contradiction shows that no such formula $\varphi(x,y)$ and parameter $a \in L$ exist. Thus $L$ cannot define the predicate $A \mapsto A \in U$ on $\mathcal P(\kappa)^L$ from parameters in $L$. Let $F^L_\kappa := \{f \in L : f:\kappa \to L\}$. For $A \in \mathcal P(\kappa)^L$, let $\mathbb{1}_A:\kappa \to L$ be the characteristic function of $A$, so $\mathbb{1}_A(\xi)=1$ for $\xi \in A$ and $\mathbb{1}_A(\xi)=0$ for $\xi \in \kappa \setminus A$. Let $c_0:\kappa \to L$ and $c_1:\kappa \to L$ be the constant functions with values $0$ and $1$, respectively. Inside $L$, the graph of $\mathbb{1}_A$ is uniquely defined from the parameters $A$ and $\kappa$ by the formula saying that its domain is $\kappa$ and its value at $\xi$ is $1$ exactly when $\xi \in A$ and $0$ otherwise. Likewise, the graphs of $c_0$ and $c_1$ are uniquely defined from $\kappa$ by the formulas saying that their domains are $\kappa$ and their constant values are $0$ and $1$. Since $A,\kappa,0,1 \in L$, these three functions are elements of $L$, and hence belong to $F^L_\kappa$. Any formula defining $=_U$ or $\in_U$ from a parameter $b \in L$ may therefore be combined with the fixed parameter $\kappa$ and with $b$ coded as a single parameter in $L$. Suppose first that the binary relation $=_U$ on $F^L_\kappa$ were definable over $L$ from a parameter in $L$. For every $A \in \mathcal P(\kappa)^L$, $\{\xi \in \kappa : \mathbb{1}_A(\xi)=c_1(\xi)\}=A$. Therefore $A \in U$ if and only if $\mathbb{1}_A =_U c_1$. The assumed definition of $=_U$ would then define the predicate $A \mapsto A \in U$ on $\mathcal P(\kappa)^L$ from parameters in $L$, contradicting the first part of the proof. Suppose next that the binary relation $\in_U$ on $F^L_\kappa$ were definable over $L$ from a parameter in $L$, where externally $f \in_U g$ if and only if $\{\xi \in \kappa : f(\xi) \in g(\xi)\} \in U$. For every $A \in \mathcal P(\kappa)^L$, the ordinal facts $0 \in 1$ and $0 \notin 0$ give $\{\xi \in \kappa : c_0(\xi) \in \mathbb{1}_A(\xi)\}=A$. Therefore $A \in U$ if and only if $c_0 \in_U \mathbb{1}_A$. The assumed definition of $\in_U$ would again define the predicate $A \mapsto A \in U$ on $\mathcal P(\kappa)^L$ from parameters in $L$, another contradiction. Hence neither the $U$-[equivalence relation](/page/Equivalence%20Relation) nor the induced $U$-membership relation is definable over $L$ from parameters in $L$. Consequently, there is no ultrapower construction internal to $L$ whose quotient relation and membership relation are the external relations determined by $U$, and $L$ cannot internally define the associated ultrapower embedding determined by this external measure. [/step]