[PDF] [arXiv]

This is a joint paper with Alfredo Roque Freire.

Abstract A theory $T$ is tight if different deductively closed extensions of $T$ (in the same language) cannot be bi-interpretable. Many well-studied foundational theories are tight, including PA [Visser2006], ZF, $Z_2$, and KM [Enayat2017]. In this article we extend Enayat’s investigations to subsystems of these latter two theories. We prove that restricting the Comprehension schema of $Z_2$ and KM gives non-tight theories. Specifically, we show that GB and $ACA_0$ each admit different bi-interpretable extensions, and the same holds for their extensions by adding $\Sigma^1_k$-Comprehension, for $k \ge 1$. These results provide evidence that tightness characterizes $Z_2$ and KM in a minimal way.