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.
 A: 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.
