Tightness and solidity in fragments of Peano Arithmetic

It was shown by Visser that Peano Arithmetic has the property that any two bi-interpretable extensions of it (in the same language) are equivalent.

Enayat proposed to refer to this property of a theory as \emph{tightness} and to carry out a more systematic study of tightness and its stronger variants that he called neatness and solidity.

Enayat proved that not only $\mathsf{PA}$, but also $\mathsf{ZF}$ and $\mathsf{Z}_2$ are solid.

On the other hand, it was shown in later work by a number of authors that many natural proper fragments of those theories are not even tight.

Enayat asked whether there is a proper solid subtheory of the theories listed above.

We answer that question in the case of $\mathsf{PA}$ by proving that for every $n$, there exist both a solid theory and a tight but not neat theory strictly between $\mathsf{I}\Sigma_n$ and $\mathsf{PA}$.

Moreover, the solid subtheories of $\mathsf{PA}$ can be required to be unable to interpret $\mathsf{PA}$.

We also provide simple examples of proper solid subtheories of $\mathsf{ZF}$ and $\mathsf{Z}_2$, as well as further separations between properties related to tightness, including an example of a sequential theory that is neat but not semantically tight in the sense of Freire and Hamkins.