# What is the consistency strength of iterated sharps?

I've been interested in sharps such as $$0^\sharp$$, $$0^{\sharp \sharp}$$ and $$\mathbb{R}^\sharp$$, so I wondered about iterating sharps. Let $$n \in \omega$$ and $$x \in V$$. Define $$x^{\sharp n}$$ like so:

• If $$n = 0$$, $$x^{\sharp n} = x$$.
• If $$n = n' + 1$$ for $$n' \in \omega$$, $$x^{\sharp n} = (x^{\sharp n'})^\sharp$$.

What is the consistency strength of $$\forall n: 0^{\sharp n} \textrm{ exists}$$? Obviously it should be above $$0^\sharp \textrm{ exists}$$, $$0^{\sharp \sharp} \textrm{ exists}$$, etc.

• This statement is weaker than "for all reals $x$, $x^\sharp$ exists", which itself is weaker than existence of $\omega_1$-Erdos cardinal. May 18, 2022 at 16:57
• Okay, I think I understand. Could you go into any more detail? May 18, 2022 at 17:02
• Mildly related: mathoverflow.net/q/351913/7206 May 19, 2022 at 9:34