Can there be two different math?

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?

• I don't see how you can say that $\sf ZFC$ and $\sf PA$ validate each other where $\sf ZFC$ is much much stronger. – Asaf Karagila Aug 12 '13 at 1:43
• @AsafKaragila, if ZFC is consistent, then it doesn't contradict PA (interpreted as talking about $\mathbb{N}$); so, I regard that as a form of validation. – goblin Aug 12 '13 at 1:46
• Sure, ZFC "validates" PA in proving its consistency (via a model), but in what sense does PA "validate" ZFC? – hardmath Aug 12 '13 at 1:49
• I would like to thank my lawyer, @hardmath, for taking care of the follow up while I was typing an answer somewhere else. :-) – Asaf Karagila Aug 12 '13 at 1:50
• Hello! Did you understand my answer? I've edited it because the first version had a slight error. Also, I've just edited the linked post to prove the generalization. It implies that even if we somehow know that our foundational system is $Σ_n$-sound, we still might not know that it is $Σ_{n+1}$-sound. From a certain viewpoint, this is as bad as it can be. – user21820 Dec 31 '17 at 8:37

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!

• Follow-up question: Does anyone know a nice constructive way to extend any given $Σ_1$-sound system to another $Σ_1$-sound system that is $Σ_2$-unsound? – user21820 Dec 13 '17 at 12:42

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 ?

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.
Now we want that PA' behave like PA regarding the set of $\Pi_1$ and $\Sigma_1$ sentences : is it possible ?
• I'm trying to follow your suggestion: to use $\Pi_1$ sentences and $\Sigma_1$ sentences as "empirical basis" of mathematical facts that are the "evidence" for "testing" PA and PA'. If we cannot use it to choose between them, and assuming both consistent, we can say that PA has a model $\mathcal M$ and PA' a model $\mathcal M'$. "Our" numbers are the intended model of PA, but if PA disproves the twin-prime conjecture, what we must do? Stay with the conjecture, and so conclude that "our" numbers are nor more the intended model of PA, or stay with PA, and conclude that the conjecture is false? – Mauro ALLEGRANZA Dec 20 '13 at 11:03