Is there a proof of the second incompleteness theorem of Godel for set theory which doesn't use Arithmetization of Syntax (Godel numbering)?

I came across a short proof by Thomas Jech (here), but I think he uses Godel numbering for defining "k" in his proof. Nevertheless Bagaria in his article (here) in referencing Jech, mentioned there is no need of arithmetizing the syntax.

My question is, does his proof crucially depend on Godel numbering? If the answer is yes, is there a proof of second incompleteness theorem for Set theory(ZFC) which doesn't need some fixed coding of formulas by proving there is no model of ZFC, in ZFC itself?, or the use of such coding is unavoidable?