On the proofs of arithmetical completeness for interpretability logic.
Domenico Zambella · Notre Dame Journal of Formal Logic · 1992
Visser proved that ILP is the interpretability logic of any finitely axiomatizable theory containing IΔ 0 4-SUPEXP, Berarducci and Shravrukov proved that ILM is the interpretability logic of PA.But these proofs are not based directly on the natural semantics of interpretability logic (i.e., Veltman models).We give simpler alternative proofs of the arithmetical completeness of ILP and ILM directly based on finite Veltman models.We will provide a general setup for arithmetical completeness proofs of interpretability logic which is in the style of Solovay's arithmetical completeness proof of provability logic.