We discuss a technique called recursive compression for proving undecidability results. The method has developed independently in mathematics and theoretical computer science, and gives a way of showing some decision problem is undecidable by reducing the halting problem to it. Recursive compression was used by Durand, Romashchenko, and Chen in 2008 to give an alternate proof that the Wang tiling problem is undecidable. In quantum information theory, recursive compression was used by Ji, Natarajan, Vidick, Wright, and Yuen in 2020 to prove the MIP*=RE result that the halting problem is reducible to approximating the quantum value of a nonlocal game. We formulate a general recursive compression lemma which abstracts the technique used in these applications. We also prove a converse of the recursive compression lemma showing that the halting problem is polytime reducible to an r.e. language if and only if there is a recursive compression proof. Finally, we generalize the recursive compression lemma throughout the arithmetical hierarchy, giving a way to show that a language is $\Sigma^0_k$-hard. This is joint work with Seyed Sajjad Nezhadi and Henry Yuen.