Authors: Joost Joosten, Luka Mikec and Albert Visser

Given two theories \(U,V\) with axiomsets that are polytime decidable so that \(U\) interprets \(V\) – we write \(U\rhd V\) – we will define a theory \(V'\) in the spirit of Feferman provability so that \(V'\) is extensionally the same as \(V\) and so that \(U\rhd V \to \Box_{ {\sf S}^1_2} (U\rhd V')\) becomes a trivial matter. We apply this technique to prove the two hierarchies of principles from [1] to be arithmetically sound in any theory containing \({\sf S}^1_2\).

Bibliography

1. E. Goris, and J. J. Joosten.,Two new series of principles in the interpretability logic of all reasonable arithmetical theories,Journal of Symbolic Logic,vol. 85 (1), pp. 1–25, 2020.