The omega-rule interpretation of transfinite provability logic
type: Item
instance of: scholarly article
title: The omega-rule interpretation of transfinite provability logic
zbMATH Open document ID: 1429.03211
author: David Fernández-Duque
author: Joost J. Joosten
published in: Annals of Pure and Applied Logic
publication date: 2018-02-06T00:00:00Z
full work available at URL: https://arxiv.org/abs/1302.5393
full work available at URL: https://biblio.ugent.be/publication/8566402
review text: For any linear order $\Lambda$, the polymodal provability logic $\mathsf{GLP}_\Lambda$ (generalizing the logic $\mathsf{GLP}_\omega$ introduced by Japaridze) has modal operators $[\xi]$ for each $\xi\in\Lambda$, representing a chain of provability operators of increasing strength. Japaridze's logic has various arithmetical interpretations in the literature: for example, for subsystems of first-order arithmetic, $[n]\phi$ may be interpreted as $n$-times iterated $\omega$-provability, or provability relative to the set of true $\Pi_n$ sentences. The latter was exploited by \textit{L. D. Beklemishev} [Ann. Pure Appl. Logic 128, No. 1--3, 103--123 (2004; Zbl 1048.03045)] to give a modal logic proof of the ordinal analysis of PA in terms of $\varepsilon_0$. \par This paper investigates the interpretation of $\mathsf{GLP}_\Lambda$ for a recursive well-order $\Lambda$ in systems of a second-order arithmetic $T$, where $[\xi]\phi$ denotes provability from $T$ using the $\omega$-rule with nesting depth at most $\xi$. It is shown that $\mathsf{GLP}_\Lambda$ is sound and complete under this interpretation for theories $T\supseteq\mathrm{ACA}_0$ meeting certain conditions, and more generally, that the same holds for any so-called $\Lambda$-uniform proof predicate for $T$. In particular, the authors include a self-contained, relatively simple Solovay-style arithmetical completeness proof for $\mathsf{GLP}_\Lambda$. The paper is intended as a groundwork for a possible future ordinal analysis of subsystems of second-order arithmetic in the spirit of Beklemishev's method.
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03F45
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 6835071
zbMATH Keywords: provability logic
zbMATH Keywords: omega rule
zbMATH Keywords: iterated provability
zbMATH Keywords: arithmetical completeness
MaRDI profile type: Publication
OpenAlex ID: W2963814436
Wikidata QID: Q120514402
arXiv ID: 1302.5393
cites work: Some results on cut-elimination, provable well-orderings, induction and reflection
cites work: Computable structures and the hyperarithmetical hierarchy
cites work: Provability logics for natural Turing progressions of arithmetical theories
cites work: Independent numerations of theories and recursive progressions
cites work: Iterated local reflection versus iterated consistency
cites work: Provability algebras and proof-theoretic ordinals. I
cites work: Q5483298
cites work: Kripke semantics for provability logic GLP
cites work: A simplified proof of arithmetical completeness theorem for provability logic GLP
cites work: On provability logics with linearly ordered modalities
cites work: Topological completeness of the provability logic GLP
cites work: Q4196401
cites work: The analytical completeness of Dzhaparidze's polymodal logics
cites work: Q4397069
cites work: Q3128959
cites work: PREDICATIVITY THROUGH TRANSFINITE REFLECTION
cites work: On the proof of Solovay's theorem
cites work: The polytopologies of transfinite provability logic
cites work: Q5419879
cites work: Models of transfinite provability logic
cites work: Q3773876
cites work: The classical and the ω-complete arithmetic
cites work: Q5286672
cites work: A Topological Study of the Closed Fragment of GLP
cites work: On strong provability predicates and the associated modal logics
cites work: Q5202654
cites work: \(\Pi_1^0\)-ordinal analysis beyond first-order arithmetic
cites work: Bounded Induction and Satisfaction Classes
cites work: ON THE ITERATED ω‐RULE
cites work: Proof theory. The first step into impredicativity
cites work: Q4040890
cites work: Q3395521
cites work: Provability interpretations of modal logic
DOI: 10.1016/J.APAL.2017.12.006
description: scientific article