I'll quote the following from the answer to this question
Gödel's work shows us how to write down an arithmetical statement that corresponds to Con(T) or ¬Con(T) for any theory T, as long as the set of axioms of T is Turing-recognizable.
Also it comments on that by saying:
This works purely syntactically, and does not depend in any way of having an interpretation of the language of T in mind
Clearly the answer is mentioning some syntactical way of "correspondence" between something written in some first order language from one side and the language of arithmetic on the other side.
I understand that Godel had shown that for consistency statements about effectively generated theories.
My question is:
Is there a way to have a similar syntactical correspondence between any axiom or theorem of any effectively generated set theory, and the language of arithmetic? For example is there an arithmetical sentence that corresponds to the axiom of pairing (in ZFC) for example?