Feferman interpretability and applications

Joost Joosten

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.

 Overview  Program