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 ZFC, 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 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. Same goes for ZFC over ZFC-AF.
- ZF+$\neg$ AC is not conservative over ZF-AF+$\neg$ AC with respect to fundamentally $\Sigma_2$ sentences, since only the former proves that there is a linearly ordered set which is not well-orderable.
- 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.
