The logic of Turing progressions (Q2176413)

\textit{A. M. Turing} [Proc. Lond. Math. Soc. (2) 45, 161--228 (1939; Zbl 0021.09704)] introduced what are known as Turing progressions, which are hierarchies of theories such that, given an initial theory \(T,\) we can construct a transfinite sequence of extensions of \(T\) by iteratedly adding \(n\)-consistency statements. There are various ways one can define Turing progression. \textit{L. Beklemishev} [in: Advances in modal logic. Vol. 9. Proceedings of the 9th conference (AiML 2012), Copenhagen, Denmark, August 22--25, 2012. London: College Publications. 89--94 (2012; Zbl 1331.03040); Stud. Log. 50, No. 1, 109--128 (1991; Zbl 0728.03017)] studied smooth Turing progressions. In the paper under review, the system TS\textbf{C} (for Turing-Schmerl calculus) that generate exactly all relations that hold between these different Turing progressions is presented. The language of TS\textbf{C} is a propositional modal language that contains modalities of the form \(\langle n^\alpha\rangle\), where \(\alpha\in\Lambda\) for some fixed ordinal \(\Lambda\) and \(n\in\omega\). The intended reading of \(\langle n^\alpha\rangle \varphi \) is the \(n\)-consistency \(\alpha\) times iterated over the arithmetical interpretation of \(\varphi\). It is shown that each modal formula is equivalent to monomial normal form. The logic TS\textbf{C} is proven to be arithmetically sound and complete for the formalized Turing progressions interpretation.