Corollary 2.2.17 (Godel-Rosser Theorem). Let $T$ be a consistent $L_{\mathrm{PA}}$-theory extending $\text{PA}{}^{-}$ and admitting a recursively enumerable axiomatisation. Then $T$ is ${\mathrm{\Pi }}_1$-incomplete: there is a ${\mathrm{\Pi }}_1$-sentence $\tau$ such that $T⁄⊢\tau$ and $T⁄⊢\neg \tau$.