  This theorem is proved in much the same way as the well-known result that the set of (codes of) valid sentences of the second-order language of arithemetic  L2 is not second-order definable in its coding structure  ℕ.  To get this latter result, one first observes that  ℕ  is characterized by a single  L2-sentence, and then shows that, if the result were false, then “truth in  ℕ”  for  L2-sentences would be definable by an  L2-formula, thereby violating Tarski's theorem on the undefinability of truth. 