This is a talk in the Online Logic Seminar on 2023 October 5.

[slides]

The notion of tightness, introduced by Visser, gives a notion of semantic completeness for a theory. Specifically, a theory T is tight if any two distinct extensions of T cannot be bi-interpretable. Important foundational theories like PA and ZF are tight. Consequently interpretations of extensions of these theories must lose information. For example, ZF + ¬AC can interpret ZFC by restricting to the constructible universe while ZFC can interpret ZF + ¬AC via, essentially, forcing. But these interpretations destroy information about the original universe, and the tightness of ZF implies there are no alternative interpretations which avoid this problem.

Enayat asked whether the full strength of theories like ZF or full second-order arithmetic is necessary for the tightness results and conjectured that this property can be used to give a characterization of these theories. Phrased in the contrapositive: must it be that any strict subtheory of these theories admits distinct, bi-interpretable extensions? Alfredo Roque Freire and I investigated this question for subsystems of second-order arithmetic, providing some evidence for Enayat’s conjecture. Namely, we show that if you restrict the comprehension axiom to formulae of a bounded complexity then you can find two distinct yet bi-interpretable extensions of the theory. The main idea of the construction, not uncommon for work in logic, goes back to an old observation by Mostowski that while truth is not arithmetically definable, it is definable over the arithmetical sets.