A question on rank-to-rank embeddings Consider a non-trivial elementary embedding $j:V_\lambda\to V_\lambda$ and, for each $A\subset V_\lambda$, set $j(A)=\bigcup_{\delta<\lambda}j(A\cap V_\delta)$.
In Implications between strong large cardinals, Annals of Pure and Applied Logic 90 (1997) 79-90, Laver says that $j:(V_\lambda, \in,A)\to (V_\lambda, \in, j(A))$ is an elementary embedding.
I think that this is equivalent to $j$ being $\Sigma_0^1$-elementary, i.e., it satisfies the definition of elementary embedding for formulas with second order variables but without second order quantifiers.
Could someone provide a hint or a reference for this fact? I think I could prove it from a particular case, namely, that $\forall x\in V_\lambda\exists y\in V_\lambda\ (x,y)\in A$ implies $\forall x\in V_\lambda\exists y\in V_\lambda\ (x,y)\in j(A)$.
Does this case follow easily from $j$ being elementary? I cannot see it.
Edited:
I have found a proof in chapter 2 of these notes (theorem 0.4), but I think that the proof has a gap, since it considers skolem functions $f_i$ and assumes tacitly that $j(f_i)$ are also total functions, but they could be just partial functions.
 A: Here is the author of the notes you quoted. Thank you very much for pointing this out, there is indeed a gap in the proof: I truly took for granted that if $f$ is total then $j^+(f)$ is total (more specifically, that if $f$ is a Skolem function, then $j^+(f)$ is a Skolem function, but once one has totality, the rest is easy).
Anyway, I think this is true. In fact, I think the following is true:
Lemma If $f:V_\lambda\to V_\lambda$ is a partial function, then $j^+(dom(f))=dom(j^+(f))$.
This is not immediate: by definition, $j^+(dom(f))=\bigcup_{n\in\omega}j(dom(f)\cap V_{\kappa_n})$; on the other hand, $dom(j^+(f))=\bigcup_{n\in\omega}j(dom(f\cap V_{\kappa_n}))$, and the single summands are not equal, for example if $f$ is the critical sequence then $j(dom(f\cap V_{\kappa_n}))=\{0,\dots,n-2\}$, while $j(dom(f)\cap V_{\kappa_n})$ is always $\omega$. 
The following is an attempt for proving this. I don't see any errors (but then again, I didn't in my notes). Sorry for the unpleasant wall of equations, that is just how I did it. Maybe there is another, more synthetic way to prove it.
Proof of Lemma. The trick is to uniformize the division in pieces, i.e., to consider $dom(f\cap V_{\kappa_n})\cap V_{\kappa_m}$. Then
$j^+(dom(f))=\bigcup_{m\in\omega}j(dom(f)\cap V_{\kappa_m})=\bigcup_{m\in\omega}j(\bigcup_{n\in\omega}dom(f\cap V_{\kappa_n})\cap V_{\kappa_m})$
because the dominion of the union of functions is the union of the dominions of the single functions. But now $\langle dom(f\cap V_{\kappa_n})\cap V_{\kappa_m}:n\in\omega\rangle$ is an $\omega$-sequence bounded in $V_{\kappa_m}$, therefore it is in $V_\lambda$, so we can carry the $j$ inside
$\bigcup_{m\in\omega}j(\bigcup_{n\in\omega}dom(f\cap V_{\kappa_n})\cap V_{\kappa_m})=\bigcup_{m\in\omega}\bigcup_{n\in\omega}j(dom(f\cap V_{\kappa_n})\cap V_{\kappa_m})=$
$=\bigcup_{n\in\omega}\bigcup_{m\in\omega}j(dom(f\cap V_{\kappa_n})\cap V_{\kappa_m})$.
$dom(f\cap V_{\kappa_n})$ is an element of $V_\lambda$, therefore there exists an $m$ such that it is in $V_{\kappa_m}$, so that is just a finite union.
$\bigcup_{m\in\omega}\bigcup_{n\in\omega}j(dom(f\cap V_{\kappa_n})\cap V_{\kappa_m})=\bigcup_{n\in\omega}j(dom(f\cap V_{\kappa_n}))=j^+(dom(f))$.
A: EDIT: Here's a complete proof, due to Hugh Woodin.
Let $j : V_\lambda \to V_\lambda$ be an elementary embedding. To show that $j$ is $\Sigma^1_0$, it suffices to show that $j : (V_\lambda, A) \to (V_\lambda, j(A))$ is elementary for any $A\subseteq V_\lambda$. Towards this, we show that for arbitrary $A\subseteq V_\lambda$, $j : (V_\lambda, A) \to (V_\lambda, j(A))$ is $\Sigma_0$ and hence, being cofinal, $\Sigma_1$. Once we know $j:(V_\lambda, A) \to (V_\lambda, j(A))$ is $\Sigma_n$, the fact that $j: (V_\lambda, A,B) \to (V_\lambda, j(A),j(B))$ is $\Sigma_n$ where $B$ codes (an enhanced version of) the $\Sigma_n$ truth predicate of $(V_\lambda, A)$ will imply $j : (V_\lambda, A) \to (V_\lambda, j(A))$ is $\Sigma_{n+1}$. Here are the details:
Claim 1: For any $A\subseteq V_\lambda$, $j:(V_\lambda, A) \to (V_\lambda, j(A))$ is $\Sigma_1$. 
Proof: By induction on formula complexity, $(V_\kappa,X\cap V_\kappa)\prec_0(V_\lambda,X)$ for any $\kappa < \lambda$ and $X\subseteq V_\lambda$ so that for any $x\in V_\lambda$ and any $\Sigma_0$ formula $\varphi$ in the language of set theory with a predicate, $(V_\lambda,A)\vDash \varphi(x)$ if and only if $(V_\kappa,A\cap V_\kappa)\vDash \varphi(x)$ if and only if $ (V_{j(\kappa)},j(A\cap V_{\kappa}))\vDash \varphi(j(x))$ if and only if $(V_\lambda,j(A))\vDash \varphi(j(x))$ (where $\kappa = \text{rk}(x)$). Now since $j$ is $\Sigma_0$ and cofinal, $j$ is $\Sigma_1$: $\Sigma_1$ always goes up, and given a $\Sigma_0$ formula $\varphi(x,y)$, if $(V_\lambda, j(A))\vDash \exists y\ \varphi(j(x),y)$, then for some $\kappa< \lambda$, $(V_\lambda, j(A))\vDash \exists y\in j(V_\kappa)\ \varphi(j(x),y)$ so $(V_\lambda, A)\vDash \exists y\in V_\kappa\ \varphi(x,y)$ since $j$ is $\Sigma_0$.
Claim 2: For any $A\subseteq V_\lambda$ and any $n < \omega$, $j:(V_\lambda, A) \to (V_\lambda, j(A))$ is $\Sigma_n$.
Proof: Proceeding by induction on $n\geq 1$, suppose that for any $X\subseteq V_\lambda$, $j : (V_\lambda, X) \to (V_\lambda, j(X))$ is $\Sigma_n$. Fix $A\subseteq V_\lambda$, and we will show $j:(V_\lambda, A) \to (V_\lambda, j(A))$ is $\Sigma_{n+1}$. Let $F = \langle \kappa_k : k <\omega\rangle$ be the critical sequence, and let $$B = \{(\ulcorner \exists y\ \psi(x,y)\urcorner,k) : \psi\in \Pi_{n-1}\wedge (V_\lambda, A)\vDash\exists y\in V_{\kappa_k}\ \psi(x,y)\}$$
The set $B$ is an enhanced version of the theory of $(V_\lambda,A)$, and the purpose of this enhancement is to ensure that the fact that $B$ is the theory of $(V_\lambda,A)$ is a $\Pi_n$ scheme, so that $j(B)$ is (an enhanced version of) the theory of $(V_\lambda,j(A))$ by the induction hypothesis. Fix a $\Sigma_n$ formula $\varphi(x)$ and a $\Pi_{n-1}$ formula $\psi(x,y)$ such that $\varphi(x) = \exists y\ \psi(x,y)$. First, $$(V_\lambda, A, F, B)\vDash \forall x\ (\varphi(x)\to \exists k< \omega\ (\ulcorner\varphi(x)\urcorner,k)\in B)$$ and second,
$$(V_\lambda, A, F, B)\vDash \forall x\ \forall k\ \left((\ulcorner\exists y\ \psi(x,y)\urcorner,k)\in B\to \forall \alpha\ (F(k) = \alpha\to \exists y\in V_\alpha\ \psi(x,y))\right)$$
Both statements are $\Pi_n$, and hence $(V_\lambda,j(A),j(F),j(B))$ satisfies the corresponding statements after applying $j$, which guarantees that $$j(B) = \{(\ulcorner \exists y\ \psi(x,y)\urcorner,k) : \psi\in \Pi_{n-1}\wedge (V_\lambda, j(A))\vDash\exists y\in V_{\kappa_{k+1}}\ \psi(x,y)\}$$
It follows now that $j : (V_\lambda,A)\to (V_\lambda,j(A))$ is $\Sigma_{n+1}$: If $\varphi(x,y)$ is $\Sigma_n$, then $(V_\lambda,A)\vDash \forall y\ \varphi(x,y)$ if and only if $(V_\lambda,A,B)\vDash \forall y\ \exists k < \omega\ (\ulcorner\varphi(x,y)\urcorner,k)\in B$ if and only if $(V_\lambda,j(A),j(B))\vDash \forall y\ \exists k < \omega\ (\ulcorner\varphi(j(x),y)\urcorner,k)\in j(B)$ since $j : (V_\lambda,A,B)\to (V_\lambda,j(A),j(B))$ is $\Sigma_1$, and this is equivalent to $(V_\lambda,j(A))\vDash \forall y\ \varphi(j(x),y)$ by our calculation of $j(B)$.
