Logic – Is There a Theory Stronger Than ZFC in Consistency?

incompletenesslogicset-theory

A theory $T$ in the language of set theory is stronger than another theory $T'$ in consistency if consistency of $T$ implies consistency of $T'$. If $T$ is able to formalize finite arguments, proves the consistency of $T'$ and does not prove its own consistency, then $T$ has to be stricly stronger than $T'$. (The above is from Kunen, Set theory, 2011, paraphrased in my language)

But every theory stricly stronger than $\mathsf{ZFC}$ that I have found proves consistency of $\mathsf{ZFC}$! For example, $\mathsf{MK}\vdash\operatorname{Con}(\mathsf{ZFC})$ where MK is the Morse-Kelley, and $\mathsf{ZFC}+\phi\vdash\operatorname{Con}(MK)$ where $\phi$ says that there is an inaccessible cardinal. Is there a set theory $T$ such that
$$S\vdash\operatorname{Con}(T)\implies\operatorname{Con}(\mathsf{ZFC})$$
$$S\not\vdash\operatorname{Con}(\mathsf{ZFC})\implies\operatorname{Con}(T)$$
but $T\not\vdash\operatorname{Con}(\mathsf{ZFC})$ (where $S$ is a metatheory that is either of $\mathsf{PA}$, $\mathsf{PRA}$, $\mathsf{ZFC}$)?

Edit: as pointed out in Toby's comment, the second condition $\operatorname{Con}(\mathsf{ZFC})\not \implies\operatorname{Con}(T)$ may not properly deliver the requirement that $T$ and $\mathsf{ZFC}$ should not be equally strong. Kunen's textbook mentions intuitionistic logic, so maybe this condition should be interpreted there somehow.

Second edit: I have restated conditions above within a metatheory $S$, as suggested in Toby's comment.

Best Answer

Here's a fun nonconstructive argument that such a theory - indeed, an extension of $\mathsf{ZFC}$ by a single sentence - must exist (for an actual example of such a sentence, apply Theorem 4 of Hamkins, Nonlinearity in the hierarchy of large cardinal consistency strength):

Let's fix our metatheory $S=\mathsf{PA}$, and suppose the answer to your question was negative. In particular, this means that for any sentence $\varphi$, if $\mathsf{PA}\not\vdash Con(\mathsf{ZFC})\rightarrow Con(\mathsf{ZFC}+\varphi)$ then $\mathsf{ZFC}+\varphi\vdash Con(\mathsf{ZFC})$. Let's abbreviate $Con(\mathsf{ZFC})\rightarrow Con(\mathsf{ZFC}+\varphi)$ by $\varphi^-$, and let's abbreviate $\varphi\rightarrow Con(\mathsf{ZFC})$ by $\varphi^+$. Then - rewriting the above implication as a disjunction and doing a bit of $\vdash$-juggling - this means that for any $\varphi$ whatsoever we have $$\mathsf{PA}\vdash\varphi^-\quad\mbox{or}\quad \mathsf{ZFC}\vdash\varphi^+$$ (or both). Say $\varphi$ is "type $1$" if the first disjunct holds via a proof shorter than any witnessing the second disjunct, and that $\varphi$ is "type $2$" if the second disjunct holds via a proof shorter than any witnessing the first disjunct. Note that by brute-force-searching we can computably tell the type of any sentence $\varphi$.

Under mild soundness assumptions, if $\varphi$ is type $1$ then $\mathsf{ZFC}+\varphi$ is consistent and if $\varphi$ is type $2$ then $\mathsf{ZFC}+\neg\varphi$ is consistent. But it's a standard exercise to show that there is no algorithm which, on input a sentence $\varphi$, can pick one of $\varphi$ or $\neg\varphi$ which is guaranteed to be consistent with $\mathsf{ZFC}$. So we have a contradiction.

Of course it would be nice to have an actual example of such a sentence! With enough work the above argument can in fact be turned into such an example, but Hamkins' argument cited above is a better way to get such an example.

Related Question