# Higher Order Provability Statements Over A Given Sentence

If I have a sentence $$S$$ over $$\mathrm{PA}$$ (or some similar theory which can encode FOL), I can look at the set $$X_S$$ which contains $$S$$ and is closed under the standard logical connectives as well as the provability predicate. So $$X_S$$ contains sentences like '$$S$$ is true and PA proves that PA does not prove that $$S$$ is false'.

How many of these sentences can be shown to be logically equivalent, say, in the context of ZFC? In other words, how many sentences about all meta truth values concerning $$S$$ can be formed that don't reduce to some simpler statement?

I already read about $$\Sigma_1$$-soundness, which is is not provable in PA, but I didin't get whether it's provable in ZFC, just like consistency of PA isn't provable in PA itself but in ZFC, as far as I can remember.