Complexity of a proper class of extendibles

Question

If consistent, is existence of a proper class of extendible cardinals provably equivalent to a $Σ^V_5$ statement?

Recall that in ZFC, a cardinal $κ$ is extendible iff for every $λ>κ$ there is an elementary embedding $j$ of $V_λ$ into some $V_μ$ with $\mathrm{crit}(j)=κ$. (In ZF, one also requires $j(k)>λ$, but this does not affect the above definition in ZFC.)

Extendibles are unusual in being a natural large cardinal property with high quantifier complexity (see this question for other examples of high quantifier complexity). The property of being some $V_μ$ is $Π^V_1$ (or $Π_1$ for short), being $λ$-extendible is $Σ_2$, and being extendible is $Π_3$, and so existence of an extendible cardinal is $Σ_4$, and existence of a proper class of extendibles is $Π_5$.

In the other direction, if $κ$ is extendible, then $V_κ ≺_{Σ_3} V$, and thus (assuming consistency) existence of an extendible cardinal is not equivalent in ZFC to a $Π_4$ statement. Analogously, I expect that existence of a proper class of extendibles is not provably (in ZFC) $Σ_5$, but it is easy to be confused by quantifier counting.

Offered in Q/A format as I was able to solve this question while working on its exposition.

Answer 1

No, it is not; existence of a proper class of extendible cardinals is not provable in ZFC from any consistent $Σ^V_5$ statement.

Assume a proper class of extendibles and let $φ$ be a true $Σ_5$ statement (or even the conjunction of all true $Σ_5$ statements), and let a set $S$ witness $φ$, and let $κ$ be the least extendible above $S$. Then $V_κ$ satisfies $\mathrm{ZFC} + φ \, +$ non-existence of a proper class of extendibles. ($V_κ ≺_{Σ_3} V$, so $V_κ$ satisfies all true $Π_4$ statements with parameters in $V_κ$, and by $S∈V_κ$, $V_κ ⊨ φ$.)

$V_κ ≺_{Σ_3} V$ is a standard fact about extendibles (as an aside, despite its similarity, being supercompact is $Π_2$) and follows from existence of arbitrarily high $λ$ such that $V_κ ≺ V_λ$ (or just $V_κ ≺_{Σ_3} V_λ$): Let $λ$ with $V_κ ≺ V_λ$ be large enough. By Downward Löwenheim-Skolem, $V_λ ≺_{Σ_1} V$, so $V_λ$ satisfies all true $Π_2$ statements with parameters in $V_λ$, so (since $λ$ is large enough relative to $κ$) $V_λ$ (and thus $V_κ$) satisfies all true $Σ_3$ statements with parameters in $V_κ$, so $V_κ ≺_{Σ_3} V$.