If I understand correctly, there are two facts proven by Gödel's second incompleteness theorem, for a formal theory containing arithmetic
1) It is possible to express the consistency of the theory with a formula Con by arithmetizing the syntax
2) If the theory is consistent, then it does not prove Con.
What I don't understand is how it can be generalized to the fact that such a theory cannot prove its own consistency. Maybe there are other ways of expressing the consistency of the theory with another formula, which does not require to arithmetize the syntax !
For instance, I don't see why Gödel's theorem implies that ZFC cannot prove that there exists a set which satisfies ZFC (which would imply the consistency of ZFC).
As far as I understand, the key to the second incompleteness theorem is the diagonal lemma, but this assumes an encoding of the formulae into objects of the theory and I don't understand clearly why such an encoding is fundamentally necessary in order to be able to express the consistency.