# Is there an arithmetic sentence for every theorem or axiom of an effectively generated set theory?

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?

In Gödel coding, axioms/sentences/proofs in the language of set theory (or any countable first-order language) get coded not as arithmetical sentences, but as individual natural numbers. So e.g. the axiom of pairing might correspond to $$4729581$$.
Note that $$\text{Con}(T)$$ is a priori not a sentence of $$T$$, but a sentence of the metatheory: "there is no proof of $$\bot$$ from the axioms of $$T$$". This is what gets coded as an arithmetical sentence: "there is no natural number which is the code of a proof of $$\bot$$ from the axioms of $$T$$".
More generally, if the codes for the axioms of $$T$$ are recursively enumerable, then for any sentence $$\varphi$$ in the langauge of $$T$$, there is an arithmetical sentence expressing "there is a proof of $$\varphi$$ from the axioms of $$T$$".