A countable language to express the theory of ZFC + “there exists a proper class of $\text{I0}$ cardinals”

Question

Does there exist a countable language (i.e. a language with countably many symbols) $\mathcal{L}$ of set theory such that the theory ZFC + "there exists a proper class of $\text{I0}$ cardinals" can be expressed by countably many statements in $\mathcal{L}$, assuming that the length of each statement is finite? If no, why? If yes, what can be an example of such language?

Answer 1

Yes. You can phrase $\rm I0$ in $\sf ZFC$, so you can just say that for every $\alpha$ there is $\kappa>\alpha$ which is the critical point of an $\rm I0$ embedding.

The reference here is:

Woodin, W. Hugh, Suitable extender models. II: Beyond $\omega$-huge, J. Math. Log. 11, No. 2, 115-436 (2011). ZBL1248.03069.

And the general fact is that if $\alpha$ is $\Sigma_2$-reflective, and there is an embedding $j\colon L_\alpha(V_{\lambda+1})\to L_\alpha(V_{\lambda+1})$, then we can derive an extender and define the ultrapower embedding that will witness $\rm I0$.