One example might be Addison's theorem: **Theorem** (Addison). The set of arithmetical sets is not itself arithmetical. The above theorem is a $ZFC$ result, but its proof uses forcing.