Thinking about the recent threads on structural consequences of the Axiom of Foundation (AF) over ZF-AF, I've been trying to find some conservativity result which explains why AF doesn't seem to have consequences in "ordinary mathematics." Here's a candidate that came to mind.

Let's call a sentence fundamentally $\Pi_2$ if it is of the form $T \models \varphi,$ where $T$ is a recursively enumerable theory in second order logic and $\varphi$ is in the language of $T.$ Note that over ZF, the fundamentally $\Pi_2$ sentences are just the $\Pi_2$ sentences.

Is ZF conservative over ZF-AF with respect to fundamentally $\Pi_2$ sentences?

Some simple observations:

• ZFC is conservative over ZFC-AF with respect to fundamentally $\Pi_2$ sentences, since any model of a second order theory is isomorphic to one in the well-founded part of the universe by the well-ordering theorem.
• ZF+$\neg$ AC is not conservative over ZF-AF+$\neg$ AC with respect to fundamentally $\Pi_2$ sentences, since only the former proves that there is a linearly ordered set which is not well-orderable.
• ZF is conservative over ZF-AF with respect to fundamentally $\Sigma_2$ sentences (defined in the obvious manner), by considering the well-founded part of the universe.
• One cannot construct a counterexample to my conjecture using permutation models of ZFA, since fundamentally $\Sigma_2$ sentences can be transferred to a symmetric model of ZF by the Jech-Sochor Theorem.