-
69On propositional quantifiers in provability logicNotre Dame Journal of Formal Logic 34 (3): 401-419. 1993.
-
62Bimodal logics for extensions of arithmetical theoriesJournal of Symbolic Logic 61 (1): 91-124. 1996.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Σ 1 ); (IΣ m , IΣ n ) for $1 \leq m etc. For the case of finitely axiomatized extensions of theories these results are extended to modal logics with propositional constants
-
52Kripke semantics for provability logic GLPAnnals of Pure and Applied Logic 161 (6): 756-774. 2010.A well-known polymodal provability logic inlMMLBox due to Japaridze is complete w.r.t. the arithmetical semantics where modalities correspond to reflection principles of restricted logical complexity in arithmetic. This system plays an important role in some recent applications of provability algebras in proof theory. However, an obstacle in the study of inlMMLBox is that it is incomplete w.r.t. any class of Kripke frames. In this paper we provide a complete Kripke semantics for inlMMLBox . Firs…Read more
-
52Provability logics for natural Turing progressions of arithmetical theoriesStudia Logica 50 (1). 1991.Provability logics with many modal operators for progressions of theories obtained by iterating their consistency statements are introduced. The corresponding arithmetical completeness theorem is proved
-
50Induction rules, reflection principles, and provably recursive functionsAnnals of Pure and Applied Logic 85 (3): 193-242. 1997.A well-known result states that, over basic Kalmar elementary arithmetic EA, the induction schema for ∑n formulas is equivalent to the uniform reflection principle for ∑n + 1 formulas . We show that fragments of arithmetic axiomatized by various forms of induction rules admit a precise axiomatization in terms of reflection principles as well. Thus, the closure of EA under the induction rule for ∑n formulas is equivalent to ω times iterated ∑n reflection principle. Moreover, for k < ω, k times it…Read more
-
48On the induction schema for decidable predicatesJournal of Symbolic Logic 68 (1): 17-34. 2003.We study the fragment of Peano arithmetic formalizing the induction principle for the class of decidable predicates, $I\Delta_1$ . We show that $I\Delta_1$ is independent from the set of all true arithmetical $\Pi_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 $\Delta…Read more
-
47Topological completeness of the provability logic GLPAnnals of Pure and Applied Logic 164 (12): 1201-1223. 2013.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 are called GLP-spaces whenever they satisfy all the axioms of GLP. We develop some constructions to build nontrivial GLP-spaces and show that GLP is complete w.r.t. the class of all GLP-spaces
-
44Franco Montagna’s Work on Provability Logic and Many-valued LogicStudia Logica 104 (1): 1-46. 2016.Franco Montagna, a prominent logician and one of the leaders of the Italian school on Mathematical Logic, passed away on February 18, 2015. We survey some of his results and ideas in the two disciplines he greatly contributed along his career: provability logic and many-valued logic
-
44Proof-theoretic analysis by iterated reflectionArchive for Mathematical Logic 42 (6): 515-552. 2003.Progressions of iterated reflection principles can be used as a tool for the ordinal analysis of formal systems. We discuss various notions of proof-theoretic ordinals and compare the information obtained by means of the reflection principles with the results obtained by the more usual proof-theoretic techniques. In some cases we obtain sharper results, e.g., we define proof-theoretic ordinals relevant to logical complexity Π1 0 and, similarly, for any class Π n 0 . We provide a more general ver…Read more
-
42On Provability Logics with Linearly Ordered ModalitiesStudia Logica 102 (3): 541-566. 2014.We introduce the logics GLP Λ, a generalization of Japaridze’s polymodal provability logic GLP ω where Λ is any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP ω yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP Λ and the decidability of GLP Λ for recursive orderings Λ. Further, we give a restricted axiomatization of the variable-free frag…Read more
-
40Provability algebras and proof-theoretic ordinals, IAnnals of Pure and Applied Logic 128 (1-3): 103-123. 2004.We suggest an algebraic approach to proof-theoretic analysis based on the notion of graded provability algebra, that is, Lindenbaum boolean algebra of a theory enriched by additional operators which allow for the structure to capture proof-theoretic information. We use this method to analyze Peano arithmetic and show how an ordinal notation system up to 0 can be recovered from the corresponding algebra in a canonical way. This method also establishes links between proof-theoretic ordinal analysi…Read more
-
37On bimodal logics of provabilityAnnals of Pure and Applied Logic 68 (2): 115-159. 1994.We investigate the bimodal logics sound and complete under the interpretation of modal operators as the provability predicates in certain natural pairs of arithmetical theories . Carlson characterized the provability logic for essentially reflexive extensions of theories, i.e. for pairs similar to . Here we study pairs of theories such that the gap between and is not so wide. In view of some general results concerning the problem of classification of the bimodal provability logics we are particu…Read more
-
35On the complexity of arithmetical interpretations of modal formulaeArchive for Mathematical Logic 32 (3): 229-238. 1993.
-
33A proof-theoretic analysis of collectionArchive for Mathematical Logic 37 (5-6): 275-296. 1998.By a result of Paris and Friedman, the collection axiom schema for $\Sigma_{n+1}$ formulas, $B\Sigma_{n+1}$ , is $\Pi_{n+2}$ conservative over $I\Sigma_n$ . We give a new proof-theoretic proof of this theorem, which is based on a reduction of $B\Sigma_n$ to a version of collection rule and a subsequent analysis of this rule via Herbrand's theorem. A generalization of this method allows us to improve known results on reflection principles for $B\Sigma_n$ and to answer some technical questions lef…Read more
-
33Review: Raymond M. Smullyan, Diagonalization and Self-Reference (review)Journal of Symbolic Logic 61 (3): 1052-1055. 1996.
-
32Induction Rules, Reflection Principles, and Provably Recursive FunctionsBulletin of Symbolic Logic 8 (2): 302. 2002.
-
31Reflection algebras and conservation results for theories of iterated truthAnnals of Pure and Applied Logic 173 (5): 103093. 2022.
-
30Positive provability logic for uniform reflection principlesAnnals of Pure and Applied Logic 165 (1): 82-105. 2014.We deal with the fragment of modal logic consisting of implications of formulas built up from the variables and the constant ‘true’ by conjunction and diamonds only. The weaker language allows one to interpret the diamonds as the uniform reflection schemata in arithmetic, possibly of unrestricted logical complexity. We formulate an arithmetically complete calculus with modalities labeled by natural numbers and ω, where ω corresponds to the full uniform reflection schema, whereas n
-
25Wolfgang Burr. Fragments of Heyting arithmetic. The journal of symbolic logic, vol. 65 , pp. 1223–1240 (review)Bulletin of Symbolic Logic 8 (4): 533-534. 2002.
-
24A many-sorted variant of Japaridze’s polymodal provability logicLogic Journal of the IGPL 26 (5): 505-538. 2018.
-
24Provability, complexity, grammarsAmerican Mathematical Society. 1999.(2) Vol., Classification of Propositional Provability Logics LD Beklemishev Introduction Overview. The idea of an axiomatic approach to the study of ...
-
23Inexhaustibility: a non-exhaustive treatment and a survey on transfinite progressions (review)Bulletin of Symbolic Logic 14 (2): 258-259. 2008.
-
212002 european summer meeting of the association for symbolic logic logic colloquium'02Bulletin of Symbolic Logic 9 (1): 71. 2003.
-
20Dick de Jongh and Franco Montagna. Provable fixed points. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 34 , pp. 229–250 (review)Journal of Symbolic Logic 58 (2): 715-717. 1993.