Provability logics for natural Turing progressions of arithmetical theories (Q804564)

In this paper Beklemishev defines a normal modal logic that has for each \(\xi < \varepsilon_0\) a modality \([\xi]\). The intended arithmetical interpretation of each modality \([\xi]\) will be a formalization in \(\mathbf{PA}\) of ``provable in the \(\xi\)-th Turing progression of some base theory \(T\)''. The logic \(\mathbf{TL}\varepsilon_0\) is presented. This logic is proven to be sound in that it generates modal principles \(\phi\) that are provable in \(\mathbf{PA}\) under any arithmetical interpretation \(\phi^{\ast}\) of \(\phi\). The base theory is chosen to be \(\mathbf{PA}\) so that transfinite induction up to any ordinal \(\lambda < \varepsilon_0\) is available. Next, modal semantics for \(\mathbf{TL}\varepsilon_0\) and certain fragments is given and modal completeness results are provided. These modal models can be embedded into arithmetic using a Solovay function to prove that \(\mathbf{TL}\varepsilon_0\) is arithmetically complete. By taking all theorems of \(\mathbf{TL}\varepsilon_0\) as axioms and adding reflexion to the logic one obtains after closing under modus ponens the logic \(\mathbf{TL}^{+}_{\varepsilon_0}\) that generates exactly the modal principles \(\phi\) that are true in the standard model under any arithmetical interpretation \(\phi^{\ast}\) of \(\phi\). It is shown that both \(\mathbf{TL}\varepsilon_0\) and \(\mathbf{TL}^{+}_{\varepsilon_0}\) are decidable.