The Mouse Set Theorem Just Past Projective

TL;DR

This paper proves that the minimal ladder mouse $M^{ld}$ contains exactly the reals that are $oldsymbol{ riangle^1_{oldsymbol{oldsymbol{ ext{omega+1}}}}}$, establishing a key connection between mice and projective sets just past the projective hierarchy.

Contribution

The paper provides a detailed proof that the set of reals in $M^{ld}$ equals $Q_{\omega+1}$, confirming the mouse set theorem just past the projective hierarchy.

Findings

$\mathbb{R} \cap M^{ld} = Q_{\omega+1}$ established

Confirmed the inclusion $Q_{\omega+1} \subseteq M^{ld}$

Connected the minimal ladder mouse to the projective hierarchy

Abstract

We identify a particular mouse, $M^{\text{ld}}$, the minimal ladder mouse, that sits in the mouse order just past $M_n^{\sharp}$ for all $n$, and we show that $\mathbb{R}\cap M^{\text{ld}} = Q_{\omega+1}$, the set of reals that are $\Delta^1_{\omega+1}$ in a countable ordinal. Thus $Q_{\omega+1}$ is a mouse set. This is analogous to the fact that $\mathbb{R}\cap M^{\sharp}_1 = Q_3$ where $M^{\sharp}_1$ is the the sharp for the minimal inner model with a Woodin cardinal, and $Q_3$ is the set of reals that are $\Delta^1_3$ in a countable ordinal. More generally $\mathbb{R}\cap M^{\sharp}_{2n+1} = Q_{2n+3}$. The mouse $M^{\text{ld}}$ and the set $Q_{\omega+1}$ compose the next natural pair to consider in this series of results. Thus we are proving the mouse set theorem just past projective. Some of this is not new. $\mathbb{R}\cap M^{\text{ld}} \subseteq Q_{\omega+1}$ was known in the 1990's. But $Q_{\omega+1} \subseteq M^{\text{ld}}$ was open until Woodin found a proof in 2018. The main goal of this paper is to give Woodin's proof.