Extensions of $PA+\neg Con(PA)$ with large consistency strength

Question

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?

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.