Basic question about encoding ZFC into PA 1) Are ZFC and PA arithmetic mutually interpretable if we extend PA to PA+A , where A is the set formulas of PA that result from the translation of the axioms of ZFC (or any large cardinal axioms extension of it)?
Assuming the answer is yes:
2) It is not clear to me if the formulas of ZFC, which in the language  $L_{\in}$ can be be written in $\Pi^0_n$ or $\Sigma^0_n$ format, are also translated into $\Pi^0_n$ or $\Sigma^0_n$ formulas of PA, or if we need to use higher order formulas of PA (I mean, if first-order PA is not enough). 
3) In such a case, are the higher order formulas ($\Pi^m_n$ or $\Sigma^m_n$, with $m,n \in Z $) of PA enough, or are there still formulas of ZFC (for instance, some large cadinal axioms) that cannot be translated (coded?) into any $\Pi^m_n$ or $\Sigma^m_n$ formula of PA? Well if such were the case then, I guess that ZFC+Large Cardinals and PA+A  would not be mutually interpretable.  
 A: If I understand correctly, the answer is no. 
When it comes to interpretations, there is actually quite a spectrum of slightly different notions. What seems to be the standard modern reference is:

Albert Visser. Categories of theories and interpretations. In Logic in Tehran, 284–341, Lect. Notes Log., 26, Assoc. Symbol. Logic, La Jolla, CA, 2006. MR2262326 (2007j:03083). 

In any case, at the very least you want an interpretation of a theory $T$ in a theory $S$ to satisfy that there is a more or less explicit "procedure" that assigns to each model of $S$ a model of $T$. However this is formalized, $\mathsf{ZFC}$ should be more than enough to carry out this assignment.  
It follows that, since $\mathsf{ZFC}$ proves the consistency of $\mathsf{PA}+A$, then the latter cannot interpret $\mathsf{ZFC}$: Otherwise, $\mathsf{ZFC}$ would prove its own consistency, against the incompleteness theorem. The argument does not change even if you let $A$ consist of all higher order formulas as you suggest in item 3. 
On the other hand, (assuming the consistency of $\mathsf{ZFC}$) if you allow the inclusion in $A$ of arithmetic consequences of large cardinal assumptions, then $\mathsf{ZFC}$ cannot interpret $\mathsf{PA}+A$: Otherwise, from any model of $\mathsf{ZFC}$ we would obtain a model of $\mathsf{PA}+\mathrm{Con}(\mathsf{ZFC+\mathrm{Con}(\mathsf{ZFC})})$. From this, we actually get $\mathrm{Con}(\mathsf{ZFC+\mathrm{Con}(\mathsf{ZFC})})$ in the model of $\mathsf{ZFC}$, since this is a $\Pi^0_1$ statement. But this means that the theory $\mathsf{ZFC}+\mathrm{Con}(\mathsf{ZFC})$ proves its own consistency, against the incompleteness theorem.
