What can the extremely large cardinals tell us about small sets?

Are there any applications of the largest large cardinals to consistency results concerning, say, cardinals below $\aleph_{\aleph_\omega}$? Or perhaps to prove results in descriptive set theory? I am thinking of ZFC + Axiom I0, ZF + Reinhardt, ZF + Berkeley. See here for definitions. The largest cardinal I know of to be used for a consistency result is a 2-huge cardinal to prove the consistency of $(\aleph_3,\aleph_2,\aleph_1) \twoheadrightarrow (\aleph_2,\aleph_1,\aleph_0)$.

I would be remiss not to mention the results of Laver about left-distributive algebras proved using Axiom I3. Some of the results have not been brought down to ZFC. This is remarkable and I suppose answers the question as posed, but my motivation is to see if there are forcing constructions aimed at small cardinals that use these very large cardinals.

• There is of course Friedman's programme to get links between Con(HUGE) and the concrete incompleteness of structures that to be seem no larger than $2^{\aleph_0}$. How much this can be seen to answer your question is debatable though... Sep 26 '16 at 23:42
• But now I see that you have been discussing related issues on the fom mailing list, so the above comment should be taken as meant for others. Sep 26 '16 at 23:44

The paper Generic $I_0$ at $\aleph_\omega$ by Vincenzo Dimonte might be of interest to you. It introduces the notion of being generic $I_0$ at $\aleph_\omega$ (Def. 3.1 of the paper), and proves several consequences of it. In particular it is shown that if eneric $I_0$ holds at $\aleph_\omega$, then $\aleph_\omega$ is Jonsson.
Of course it is open if generic $I_0$ at $\aleph_\omega$ can be consistent!.
• Yes, unfortunately the paper on generic $I_0$ does not give a forcing construction as it is asked in the question, it just says IF there is a forcing construction with such and such properties THEN there are consequences on small cardinals so specific that it would be weird if they do not come from $I_0$. For what is worth, I don't know any attempt of proving even just generic 3-huge, and I don't know any forcing construction that uses $I_0$ in a meaningful way. Oct 4 '16 at 16:30