[wubrr]

Any links/examples of why this isn't possible? My thinking is - if all existing set theory and set theoretic proofs are expressed in finite set-theoretic statements/expressions - can't we 'encode' these expressions within the system of arithmetic?

[Kranar]

Do I have links off the top of my head that directly address this, no unfortunately I do not. I do have links to different pieces that you can use to understand this, however. First is the notion of the consistency strength of a formal system which basically is the ability of one formal system to prove the consistency of another formal system [1].

ZFC is strictly stronger than PA in the sense in that ZFC can prove the consistency of PA [2].

From this, however, it follows that PA can not prove the consistency of ZFC. If PA could prove the consistency of ZFC then ZFC would be able to prove the consistency of itself, which we know from Godel's incompleteness theorem would mean that ZFC is inconsistent [3].

So this gives one concrete proof that ZFC can produce that PA can not produce, namely the consistency of PA itself.

[1] https://en.wikipedia.org/wiki/Equiconsistency#Consistency_st...

[2] https://mathoverflow.net/questions/66121/is-pa-consistent-do...

[3] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...