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.
