...actually, if the wizard students weren't already familiar with first-order logic, the chances are roughly infinity to zero against them already being familiar with the principle that you may freely assume a proposition's quoted provability within a quoted system, in order to prove the unquoted proposition within the unquoted system.
Without which principle this problem is in fact unsolvable. Oops.
Well, you could state about yourself that you were adopting some informal version of that principle, it's not like humans actually meet the assumptions for the simple version of the math. But, yeah, that probably makes it a lot harder to see how the solution works, doesn't it.