Are there any proofs of 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 Jesh, mentioned it is no need of arithmetizing the syntax. My question is, does his proof crucially depends on Godel numbering? If the ansere is yes, is there any proofs 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?