Interpolation and the interpretability logic of PA (Q867400)

The interpretability logic is a nonstandard modal logic which describes the relation of relative interpretability between arithmetical theories like \(T+A\) and \(T+B,\) where \(A\) and \(B\) are formulas (for detailed definitions see, e.g., [\textit{A. Visser}, ``An overview of interpretability logic'', in: M. Kracht et al. (eds.), Advances in modal logic. Vol. 1. CSLI Lect. Notes 87, 307--359 (1998; Zbl 0915.03020)] or [\textit{D. de Jongh} and \textit{G. Japaridze}, ``The logic of provability'', in: S. R. Buss (ed.), Handbook of proof theory, 475--546 (1998; Zbl 0915.03019]). The modal system ILM is the interpretability logic of Peano arithmetic. This system does not have the interpolation property. For this reason the author considers an extensions of the system ILM by an additional operator for \(\Sigma_1\)-ness. An axiomatization for this extension is given (the system ILM(S)). The author proved modal and arithmetical completeness of the system ILM(S) in an earlier paper. The main result of the paper under review is that the system ILM(S) does not have the interpolation property.