There is a large hierarchy of theories strengthening $PA$ eg $PA+Con(PA)$, $PA+Con(PA+Con(PA))$,..., second-order arithmetic and $ZFC$, ordered by consistency strength.

Is there an extension of $PA+\neg Con(PA)$ with large consistency strength? By which I mean is there some axiom (or axiom scheme) $A$ such that $PA$ proves that $Con(PA+\neg Con(PA)+A)\rightarrow Con(T_1)$ and $Con(T_2)\rightarrow Con(PA+\neg Con(PA)+A)$ for some strong theory $T_1$ (eg. $ZFC$) and some not necessarily distinct theory $T_2$?

I think I have an example of such an axiom but I’m not sure how to prove it’s consistent under appropriate assumptions. Consider the following axiom $P$:

If $N$ is the length in symbols of the shortest proof of a contradiction in $PA$ the there is no proof of a contradiction in $ZFC$ in fewer than $\log(N)$ symbols

Obviously this statement depends on how exactly proofs in $PA$ and $ZFC$ are formalized, this should be done in a sensible way such that proofs in $ZFC$ are not automatically much shorter than similar proofs in $PA$.

$PA$ proves that $Con(PA+\neg Con(PA)+P)\rightarrow Con(ZFC)$. Informally this is because if $PA$ is consistent then the $N$ referred to in $P$ must be a nonstandard number and if the shortest proof of a contradiction in $ZFC$ is longer than $log(N)$ it must also be nonstandard. So $ZFC$ is consistent.

More carefully and reasoning in $PA$:
Assume $Con(PA+\neg Con(PA)+P)$. Since by assumption $PA$ is consistent, for each $n$ we have that $PA$ proves that "the length of shortest $PA$ proof of a contradiction is greater than $n$". If $ZFC$ were inconsistent and had a proof of a contradiction of length $m$ then $PA$ would prove that "the length of shortest $PA$ proof of a contradiction is greater than $\lceil e^m \rceil$" contradicting $Con(PA+\neg Con(PA)+P)$. So $ZFC$ must be consistent.

But I’m not sure how to show the reverse implication that $Con(ZFC)\rightarrow Con(PA+\neg Con(PA)+P)$.

I therefore have two questions.

Question 1: Is there a consistent theory extending $PA+\neg Con(PA)$ with consistency strength greater than or equal to $ZFC$?

Question 2: Assuming appropriate consistency assumptions is $PA+\neg Con(PA)+P$ consistent?


1 Answer 1


Let $T$ be the theory PA + ¬Con(PA), plus the axiom asserting that there is no proof of a contradiction in ZFC (or ZFC+LC etc.) of size below $k$, where $k$ is the smallest such that $\newcommand\PA{\textsf{PA}}\PA_k$ is inconsistent, where this is the basic arithmetic theory plus $\Sigma_k$ induction.

That is, the theory $T$ asserts that PA is inconsistent, but at the smallest inconsistent level of $\Sigma_k$ induction, there is no proof of a contradiction in ZFC of size less than $k$. (Thus, I use not the size of the smallest proof of a contradiction, as with your $P$, but rather the amount of induction needed to support an inconsistency.)

First of all, I claim, T is consistent relative to consistency assertions about ZFC. To see this, consider a nonstandard model of PA+Con(ZFC) with a nonstandard number $k$. Since the model thinks PA is consistent, it also thinks $\PA_k$ does not prove its own consistency, and so it can form a complete consistent Henkin theory extending $\PA_k+\neg\text{Con}(\PA_k)$. Since $k$ is nonstandard, this includes all the standard axioms of $\PA$. Interpreting this theory gives an end-extension of the original model in which $\PA+\neg\text{Con}(\PA_k)$ holds, but there will be no proof of a contradiction in ZFC below $k$, since the original model didn't have one and it is an end-extension. So it is a model of $T$.

It seems we get Con(ZFC) implies Con(T) over PA, since if we work in PA+Con(ZFC), then we have Con(PA+Con(PA)), and so we can interpret a nonstandard model of PA+Con(PA). Let $k$ be nonstandard in this model with no smaller proofs of a contradiction in ZFC, and then proceed as above to interpret a still tallermodel of PA+$\neg\text{Con}(\PA_k)$, and this taller model will be a model of T since there were no proofs of a contradiction from ZFC below $k$.

Conversely, if we assume Con(T), then in particular Con(PA), and so in PA+Con(T) we can prove that the $k$ that arises in any model of T must be nonstandard (using Mostowski reflection), and so there can be no standard proof of a contradiction in ZFC, and so Con(ZFC) holds.

Thus, $T$ is equiconsistent with ZFC over PA. And we could have used any much stronger theory if we had wished.

  • $\begingroup$ This argument doesn't seem to show consistency of your statement $P$, since the proof of a contradiction in PA in the end-extension will be much bigger than $k$ and indeed in the end-extension above the original nonstandard PA model, with it's log therefore also outside, so we can't seem to know that ZFC isn't refuted by that stage. $\endgroup$ Nov 6, 2023 at 1:15
  • 1
    $\begingroup$ Thank you for your excellent and prompt answer! My delay in accepting it lay only in my intending to mull it over and then promptly moving on to other things. $\endgroup$
    – Tom Bouley
    Dec 3, 2023 at 2:50
  • $\begingroup$ Does it matter that you defined $k$ as the smallest such that $\mathsf{PA}_k$ is inconsistent, or would the argument work just as well with the length of the smallest proof of inconsistency in $\mathsf{PA}$? (In other words, what can be said about the theory $T'$ which says “$\mathsf{PA}$ is inconsistent and no proof of a contradiction in $\mathsf{ZFC}$ comes before the earliest proof of a contradiction in $\mathsf{PA}$”? I can make this into a separate question if you think the answer is too long for a comment.) $\endgroup$
    – Gro-Tsen
    Jan 19 at 9:08
  • $\begingroup$ @Gro-Tsen My argument wouldn't work if you did it that way. We know how to control exactly the level of the theory $\text{PA}_k$ that becomes inconsistent in the interpreted model, but we have much less control over the size of the proofs of contradiction (which are necessarily much larger). I'm not sure how to analyze your theory $T'$, which is closer to the OP's question, and this is why in my answer I moved to $\text{PA}_k$ instead. $\endgroup$ Jan 19 at 16:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.