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.

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

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.