# Formalizing consistency implications

Let $T$ be an axiomatizable theory extending minimal arithmetic, and $T'$ an axiomatizable extension of $T'$. Let $\square_{A}$ be the standard provability predicate for $A$.

Is it true that $T\vdash \neg\square_{T'}\bot \rightarrow \neg\square_{T}\bot$?

And if $T$ extends Peano arithmetic?

Obviously, the sentence as stated is true, and it is easy to give an argument to that effect. But it is provable from within the theory itself?

I am fairly sure it is as long as $T$ extends minimal arithmetic, but I cannot seem to find a nice, short argument showing that.

My first thought was that since the sentence is a $\Sigma$-sentence then it was a given that it is provable from minimal arithmetic. But then I realized that it is not a $\Sigma$-sentence.

I suppose that if I dug into the construction of the provability predicates then I could prove what I want, but that seems like hard work and I rather have an argument which gave me a better intuition about provability in arithmetic.

• Why do you suspect it is true (or false)? More context would make it easier to write a helpful answer to this question. Sep 18, 2016 at 12:00
• @CarlMummert Sure! I will provide more context. Sep 18, 2016 at 15:52
• (@Jsevillamol Hello!) Sep 18, 2016 at 19:31

The main issue is whether $T$ proves that $T'$ is an extension of $T$. So we should be working with axiomatized theories rather than axiomatizable theories. There are also two senses in which one theory can extend another. Finally, rather than looking at $$\lnot \Box_{T'} \bot \to \lnot \Box_{T} \bot,$$ I think it is easier to look at the contrapositive scheme $$\Box_{T}\phi \to \Box_{T'} \phi.$$
Sense 1: $T$ proves that "every $T$-derivation is a $T'$-derivation". Then $T$ will easily prove the scheme $$\Box_{T}\phi \to \Box_{T'} \phi.$$ This will be the case, for example, if $T$ proves that every axiom of $T$ is an axiom of $T'$. One way to make that happen is to take $T' = T + \psi$ for some new axiom $\psi$, and then define the axiomatization of $T'$ in the natural way.
We can also make unnatural axiomatizations of that same $T'$ so that $T$ cannot prove that $T$ is a subset of $T'$, even though $T$ is actually a subset of $T'$. One way to do that is to say that, given a Gödel number $n$ for a formula $\psi$, we let $n$ be an axiom of $T'$ if and only if $n$ is an axiom of $T$ and there is no $T$-derivation of $0=1$ with Gödel number less than $n$. Then $T$ will be unable to prove that $T'$ has an infinite set of axioms, due to the incompleteness theorem.
Sense 2: More generally, suppose that $T$ proves that "every axiom of $T$ is derivable in $T'$". Then it only takes a small amount of induction (much less than is in PA) for $T$ to prove the scheme $$\Box_{T}\phi \to \Box_{T'} \phi.$$ The induction is needed to convert each application of a $T$-axiom into a $T'$-derivation of that axiom. It seems unlikely to me that the scheme could be proved with only induction on quantifier-free formulas, because there is no telling how many $T$-axioms have to be converted. But the scheme will be provable with induction on $\Sigma^0_1$ formulas.