As per usual, let PA denote Peano Arithmetic and ZFC denote Zermelo-Fraenkel set theory with choice. Furthermore, ZFC 'validates' PA, in the sense that it proves that the PA axioms hold for the standard model of the natural numbers. Arguably, PA also validates ZFC, albeit in a weaker sense. In particular, note that, if ZFC is consistent, then the sentences it proves about the natural numbers do not contradict the theorems of PA.
However, I'm wondering: can we find theories PA' and ZFC' that contradict the more usual PA and ZFC, but which validate each other in much the same way that PA and ZFC validate each other? Obviously the answer is 'yes', but what if we further require that PA and PA' agree on on all $\Pi_1$ sentences and all $\Sigma_1$ sentences, and similarly that ZFC and ZFC' agree on all $\Pi_1$ sentences and all $\Sigma_1$ sentences in the language of arithmetic?
Then we'd have no 'trial-and-error' method for choosing between the foundation (PA,ZFC) versus the foundation (PA',ZFC'), since it is only $\Pi_1$ and $\Sigma_1$ sentences in the language of arithmetic that can actually be checked in a mechanical fashion. More precisely, the $\Pi_1$ sentences of arithmetic are precisely those that can be mechanically falsified (if false), while $\Sigma_1$ sentences are those that can be mechanically verified (if true).
So is this possible?
And if so, how do we decide which is the correct, true math? (And, is this even a coherent idea?)
For instance, it is known that the twin-prime conjecture is $\Pi_2$. What if the PA/ZFC approach to math proves that the twin-prime conjecture is true, while the PA'/ZFC' approach proves that its false? What then?
Yes. Let $S$ be our chosen foundational system. Even if we somehow know that $S$ is $Σ_1$-sound, we still cannot rule out the possibility that $S$ is $Σ_2$-unsound! Here truth and arithmetical soundness are of course defined with respect to the natural numbers in the meta-system.
First consider any ω-consistent formal system $T$ that has a proof verifier program and uniformly interprets PA. We shall construct an ω-consistent formal system $T'$ that is unsound.
For any sentence $P$ over $T$ we say that $T \vdash_ω P$ iff there is some $1$-parameter sentence $Q$ such that $T \vdash Q(0),Q(1),Q(2),\cdots$ and $∀k(Q(k)) \vdash P$, namely iff there is a proof of $P$ over $T$ using at most one application of the ω-rule. Now this itself can be expressed as a $Σ_3$-sentence, namely that there is a $1$-parameter arithmetic sentence $ωProv_T$ such that $T \vdash_ω P$ iff $\mathbb{N} \vDash ωProv_T(\ulcorner P \urcorner)$. We can write this succinctly using a new modal operator $ω⬜$, where $T \vdash_ω P$ iff $\mathbb{N} \vDash ω⬜_T P$.
Then it can be shown that $T \vdash_ω$ and $ω⬜_T$ satisfy the modal fixed-point theorem and the Hilbert-Bernays provability conditions, namely: $ \def\imp{\Rightarrow} $
If $T \vdash_ω P$ then $T \vdash_ω ω⬜_T P$.
$T \vdash_ω ω⬜_T P \land ω⬜_T ( P \imp Q ) \imp ω⬜_T Q$.
$T \vdash_ω ω⬜_T P \imp ω⬜_T ω⬜_T P$.
Thus the same proof of Lob's theorem immediately shows that if $T \vdash_ω ω⬜_T P \imp P$ then $T \vdash_ω P$. Since $T$ is ω-consistent, we have $T \nvdash_ω \bot$ and hence $T \nvdash_ω \neg ω⬜_T \bot$. Thus $T' \overset{def}= T + ω⬜_T \bot$ is ω-consistent. But by ω-consistency of $T$ we have $\mathbb{N} \nvDash ω⬜_T \bot$, and hence $T'$ is $Σ_3$-unsound.
Side remark: Since $\mathbb{N} \vDash \neg ω⬜_T \bot$, we also have that $T'' \overset{def}= T + \neg ω⬜_T \bot$ is ω-consistent, and so $T'$ and $T''$ are mutually incompatible ω-consistent extensions of $T$.
Next notice that you cannot possibly know whether your $S$ is not like $T'$, based on just knowing that $S$ is $Σ_1$-sound. So it is possible that $S$ is like $T'$ in being $Σ_3$-unsound and yet prove only true $Σ_1$-sentences. We can however generate all proofs of $S$ and see whether $S \vdash ω⬜_S \bot$. That would tell us that $S$ is unsound. If $S$ also interprets the weak predicative system ACA, we could generate all proofs and see whether $S$ proves itself arithmetically unsound, which would tell us that it has no $ω$-model.
A stronger but non-constructive approach is to note that there is no program using only the halting oracle $H$ that can determine the truth-value of any $Σ_2$-sentence, because that would contradict the unsolvability of the halting problem relative to $H$.
Now take any $Σ_1$-sound formal system $S$ that has a proof verifier program and interprets PA. Let $S'$ be $S$ plus all true $Π_1$-sentences. Then $S'$ is consistent, because otherwise $S$ proves some finite disjunction of false $Σ_1$-sentences, which is equivalent to a single false $Σ_1$-sentence. Also there is a program $V$ using $H$ that enumerates the theorems of $S'$, which includes all true $Σ_2$-sentences. By the consistency of $S'$ and the above fact, $V$ will fail to enumerate all the true $Π_2$-sentences. Thus there is a $Π_2$-sentence $U$ that is true but not provable in $S'$. Then $S+¬U$ is clearly not $Σ_2$-sound. Also, if $S+¬U$ is $Σ_1$-unsound, then $S+¬U$ proves some false $Σ_1$-sentence $F$, and hence $S+¬F$ proves $U$, which is impossible by choice of $U$. Thus $S+¬U$ is $Σ_1$-sound.
It turns out that this non-constructive approach can be made into a completely constructive one as described in this answer, which in short is by unfolding the constructive proof of the incompleteness theorem using the zero-guessing problem, relativized to the halting oracle, to construct an explicit true $Π_2$-sentence that $S'$ cannot prove. Hence the follow-up question in my comment is answered!