Can there be two different math?

Solution 1:

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!

Solution 2:

Are you thinking to a sort of "crucial experiment" like those used in empirical sciences in order to choose between two competing theories ?

You are assuming the union of the sets of $\Pi_1$ sentences and $\Sigma_1$ sentences as a sort of "empirical basis" of mathematical facts that forms the "evidence" against which compare a couple of competing theories (i.e. PA and PA').

If both theories agree on this basis, how can we decide between them ?

Assuming that PA and PA' are consistent, we know that they have models. If $\mathcal M$ is a model of PA (PA'), the (closure of) theorems of PA (PA') are sentences that express "true facts" about the model; is it right ?

Assume that we can find a $\Pi_2$ formula that is proved by (e.g.) PA and disproved by PA'.

But then, what are the evidence for/against it ? If the mathematical community does not share an "intuition" for or against the twin-prime conjecture, the only way left to affirm (or deny) a mathematical fact is through a proof (accepted by the math community) of it.

Is this case different from that of euclidean vs non-euclidean geometry ?

Added Dec, 20

Leaving aside the analogies, what PA' will looks like ? Assuming first-order logic with individual constant $0$, function symbol $'$ and two predicate symbols : $+$ and $.$, in order to obtain PA' it is necessary to add to the usual FO version of Peano Axioms, some new axiom that is not provable in PA itself.

This must be a statement undecidable on the basis of (FO version of) PA's axioms, otherwise PA' will be inconsistent (or PA itself).

(Note : is it true that this statement is like parallel postulate of euclidean geomtery ?, i.e. is undecidable on the basis of the remaining axioms)

Now we want that PA' behave like PA regarding the set of $\Pi_1$ and $\Sigma_1$ sentences : is it possible ?