>[!info] Definition $aa^{+}$ logic > First order logic with second order variables intended to signify countable subsets, where $\mathcal{M}\vDash aay\Phi(\mathbf{y}\dots)$ if there is a club of countable subsets of $\mathcal{M}$ such that the first admissible model (wrt y,...,$\mathcal{M}$) satisfies $\Phi(y, \dots)$. >[!note] Remark > Allows talking about the transitive collapse of sets **Theorem.** $0^{pistol}$, the sharp for a model with strong cardinal, is in $C(aa^{+})$. Claim. Iterate a countable mouse $(J_{\eta_{0}}^{\bar{E}},F_{0})$ up to $\lambda$ ($\mathrm{cf}(\lambda)>\omega$), where on a club of places you use the top extender. Then $N_{\lambda},F_{\lambda}$ are definable by the $aa^{+}$ logic . >[!info] Definition Jensen indexing > We put the extender $E$ on the $\rho$th place if, provided $\mathrm{crit}(E)=\kappa$, $\rho=\sup J_{E}''(\kappa ^{+})^{M}$ ## Defining a core model in $C(aa^{+})$ $N_{0}=0^{P}$. Define a $K^{c}$ construction in $C(aa^{+})$ by induction. $M_{0}=(V_{\omega},\varnothing)$. At stage $\nu$ (have $M_{\nu}$) ask whether there is an $\omega$-closed extender $\mathcal{F}_{\nu}$ that an be put into the sequence of $M_{\nu}$ (can be shown that there is at most one). Set $\mu_{\nu}=ON\cap M_{\nu}$. let $\bar{M}_{\nu}=(M_{\nu},\mathcal{F}_{\nu})$. This might not be a mouse. So let $M_{\nu+1}=\mathrm{Core}(\bar{M}_{\nu})$. Otherwise let $M_{\nu+1}=\mathrm{Rud}(M_{\nu}\cup \{M_{\nu}\})$ At limit stages you take "liminf" - only pieces that stabilize on the way compare $M_{\nu}$ with $N_{0}$ up to $\nu=\omega_{2}$. The claim is that $M_{\omega_{2}}$ must win.