If a theory $A$ can prove $B$ consistent relative to $A$, and $A$ is consistent, does $B$ have to be consistent?

Let's say we have two sets of axioms $A$ and $B$ such that $\mathsf{ZF} \subseteq A \subseteq B$, and from $A$ we can prove that if $A$ is consistent, then $B$ is consistent as well (that is, $A \vdash \text{Con}(A) \rightarrow \text{Con}(B)$).

Now, if $A$ is consistent ($A \not\vdash \bot$), does it follow that $B$ is consistent ($B \not\vdash \bot$)?

My approach: I think the answer is "no":

Suppose $\mathsf{ZF}$ is consistent. Since $\mathsf{ZF} \not\vdash \text{Con}(\mathsf{ZF})$ (by the second incompleteness theorem), $A = \mathsf{ZF} + \lnot\text{Con}(\mathsf{ZF})$ is consistent as well. Since we have $A \vdash \lnot \text{Con}(\mathsf{ZF})$, we also have $A \vdash \lnot \text{Con}(A)$, and thus $A \vdash \text{Con}(A) \rightarrow \text{Con}(B)$ for any $B$.

Now, let $B = A + \bot$. Then $B$ is obviously inconsistent, so $A$ and $B$ are a counterexample to my "rule".

Does this look correct? Can one also give a counterexample without assuming the consistency of $\mathsf{ZF}$?

The philosophical reason why I think that this might be important is the following:

As far as I know, one important reason for accepting the axiom of choice is the following: Gödel proved (using $\mathsf{ZF}$) that if $\mathsf{ZF}$ is consistent, then so is $\mathsf{ZFC}$. So if $\mathsf{ZF}$ is usable, then so is $\mathsf{ZFC}$.

But if the answer to my question is "no", that argument is flawed: Suppose tomorrow somebody proves a contradiction from $\mathsf{ZFC}$. Then of course, from the contrapositive of Gödel's theorem, we can prove $\mathsf{ZF}$ inconsistent. But $\mathsf{ZF}$ might still be a perfectly usable, since we haven't proven a contradiction from it!

(If one takes the perspective of "believing" in $\mathsf{ZF}$ then this paradoxical situation looks as follows: one "knows" that a proof of a contradiction is "out there", but one can't find that proof, and that proof might have some nonstandard length, so that no mathematicians will ever be able to write it down!)

This is probably too vague for this site, but if anybody spots some holes in that argumentation, feel free to point them out!

• If there is a proof of a contradiction from $\mathsf{ZFC}$, then there is a proof of a contradiction from $\mathsf{ZF}$. – Andrés E. Caicedo Jun 30 '16 at 16:49
• I disagree with the vote to close - I think this is an appropriate question for this site. – Noah Schweber Jun 30 '16 at 17:34

You are correct that, if $A$ proves "$Con(A)\rightarrow Con(B)$" and $A$ is consistent, this in general tells us nothing about whether $B$ is consistent.
However, your criticism of the argument that ZFC is consistent if ZF is, is flawed: the proof of "$Con(ZF)\rightarrow Con(ZFC)$" takes place in a much weaker theory (Peano Arithmetic is enough). So as long as we believe that $PA$ is true (or merely correct about $\Sigma_1$ sentences), then that's enough.
• Also, note that even if full ZF were needed to prove this, the effect of a contradiction in ZFC would still be felt in ZF: namely, ZF would have to prove "I am inconsistent!" Now ZF might still be consistent, but I'm not sure ZF would be usable - surely we (most of the time :P) only care about set theories which don't prove plainly false $\Sigma_1$ facts! – Noah Schweber Jun 30 '16 at 17:35
• Uhm, where can I look up $\Sigma_1$ facts, and why is "I am inconsistent!" plainly false? – dankness Jun 30 '16 at 17:42
• @dankness If ZF is in fact consistent, then "ZF is inconsistent" is false; that's all I meant (presumably if we're using ZF, we believe ZF is consistent, in which case we believe "ZF is inconsistent" is false). Meanwhile, $\Sigma_1$ is a notation used to refer to part of the Levy hierarchy: basically, a sentence is $\Sigma_1$ if it has the form $\exists x_0, x_1, . . ., x_n\varphi$," where $\varphi$ uses only bounded quantifiers (e.g. quantifiers of the form $\forall x<y$ or $\exists x<y$). Inconsistency statements are of this form. – Noah Schweber Jun 30 '16 at 17:48
• @Noah. It may be worth adding that if $\mathsf{ZFC}$ is inconsistent, the proof that ${\rm Con}(\mathsf{ZF})\to{\rm Con}(\mathsf{ZFC})$ gives more than a proof of $\lnot{\rm Con}(\mathsf{ZF})$ from $\mathsf{ZF}$: It actually gives a proof of the inconsistency of $\mathsf{ZF}$. Your comments address what happens when $\mathsf{ZF}$ is actually consistent, and yet it proves the inconsistency of $\mathsf{ZFC}$, which is a slightly different thing. I point this out because the difference is subtle and may be worth making it explicit to the OP. – Andrés E. Caicedo Jun 30 '16 at 19:09
• @NoahSchweber No, no. Using Gödel's arguments you get in the real world with actual true numbers an explicit procedure that transforms a proof of an inconsistency in one theory into a proof of an inconsistency in another theory. As soon as you formalize this procedure into a (meta)theory, naturally we need to assume its $\Sigma_1$-soundness. – Andrés E. Caicedo Jun 30 '16 at 19:40