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?