The logic of Turing progressions

Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) First-order arithmetic and fragments (03F30) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Abstract: Turing progressions arise by iteratedly adding consistency statements to a base theory. Different notions of consistency give rise to different Turing progressions. In this paper we present a logic that generates exactly all relations that hold between these different Turing progressions given a particular set of natural consistency notions. Thus, the presented logic is proven to arithmetically sound and complete for a natural interpretation, named the emph{Formalized Turing progressions} (FTP) interpretation.

Review text

\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.

Recommendations

Cites work

Cited in

(11)

This page was built for publication: The logic of Turing progressions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2176413)