Abstract A formula φ is called n-provable in a formal arithmetical theory S if φ is provable in S together with all true arithmetical ${{\rm{\Pi }}_n}$ -sentences taken as additional axioms. While in general the set of all n -provable formulas, for a fixed $n > 0$ , is not recursively enumerable, the set of formulas φ whose n -provability is provable in a given r.e. metatheory T is r.e. This set is deductively closed and will be, in general, an extension of S . We prove that these theories can be naturally axiomatized in terms of progressions of iterated local reflection principles. In particular, the set of provably 1-provable sentences of Peano arithmetic $PA$ can be axiomatized by ${\varepsilon _0}$ times iterated local reflection schema over $PA$ . Our characterizations yield additional information on the proof-theoretic strength of these theories (w.r.t. various measures of it) and on their axiomatizability. We also study the question of speed-up of proofs and show that in some cases a proof of n -provability of a sentence can be much shorter than its proof from iterated reflection principles.

Provability logic GLP is well-known to be incomplete w.r.t. Kripke semantics. A natural topological semantics of GLP interprets modalities as derivative operators of a polytopological space. Such spaces satisfying all the axioms of GLP are called GLP-spaces. We develop some constructions to build nontrivial GLP-spaces and show that GLP is complete w.r.t. the class of all GLP-spaces.

Gurevich and Neeman introduced Distributed Knowledge Authorization Language (DKAL). The world of DKAL consists of communicating principals computing their own knowledge in their own states. DKAL is based on a new logic of information, the so-called infon logic, and its efficient subsystem called primal logic. In this article, we simplify Kripkean semantics of primal logic and study various extensions of it in search to balance expressivity and efficiency. On the proof-theoretic side we develop cut-free Gentzen-style sequent calculi for the original primal logic and its extensions.

Sergei Adian, Lev Beklemishev, Albert Visser; Proof and Computation, Journal of Logic and Computation, Volume 21, Issue 4, 1 August 2011, Pages 541–542, https:/

Journal Article Editorial Get access S. I. Adian, S. I. Adian Search for other works by this author on: Oxford Academic Google Scholar M. Baaz, M. Baaz Search for other works by this author on: Oxford Academic Google Scholar L. D. Beklemishev L. D. Beklemishev Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 15, Issue 4, August 2005, Page 409, https://doi.org/10.1093/logcom/exi036 Published: 01 August 2005

We study a propositional polymodal provability logic GLP introduced by G. Japaridze. Previous treatments of this logic, due to Japaridze and Ignatiev, heavily relied on some non-finitary principles such as transfinite induction up to ε0 or reflection principles. In fact, the closed fragment of GLP gives rise to a natural system of ordinal notation for ε0 that was used for a proof-theoretic analysis of Peano arithmetic and for constructing simple combinatorial independent statements. In this paper, we study Ignatiev's universal model for the closed fragment of this logic. Using bisimulation techniques, we show that several basic results on the closed fragment of GLP, including the normal form theorem, can be proved by purely finitary means formalizable in elementary arithmetic. As a corollary, the system of ordinal notation for ε0 based on the closed fragment of GLP is shown to be provably isomorphic to the standard system of ordinal notation up to ε0. We also settle negatively some conjectures by Ignatiev.

Abstract We study the fragment of Peano arithmetic formalizing the induction principle for the class of decidable predicates,IΔ1. We show thatIΔ1is independent from the set of all true arithmetical Π2-sentences. Moreover, we establish the connections between this theory and some classes of oracle computable functions with restrictions on the allowed number of queries. We also obtain some conservation and independence results for parameter free and inference rule forms of Δ1-induction. An open problem formulated by J. Paris (see [4, 5]) is whetherIΔ1proves the corresponding least element principle for decidable predicates,LΔ1(or, equivalently, the Σ1-collection principleBΣ1). We reduce this question to a purely computation-theoretic one.

Abstract We characterize the bimodal provability logics for certain natural (classes of) pairs of recursively enumerable theories, mostly related to fragments of arithmetic. For example, we shall give axiomatizations, decision procedures, and introduce natural Kripke semantics for the provability logics of (IΔ0 + EXP, PRA); (PRA, IΣn); (IΣm, IΣn) for 1 ≤ m < n; (PA, ACA0); (ZFC, ZFC + CH); (ZFC, ZFC + ¬CH) etc. For the case of finitely axiomatized extensions of theories these results are extended to modal logics with propositional constants.