Here is a list of selected open problems in the areas of my interests originally posted in 2002. They are grouped thematically. Click on a problem to get a comment and possibly some related questions. If you would like to make a comment or contribute a question, please mail to lbekl@yandex.ru. Presumably easier problems suitable, e.g., for a graduate project are marked by (*).

31.07.05. On the basis of part of the list below we have written a paper together with Albert Visser where we give an orderly overview and more extended comments to some questions. See: Beklemishev, L.D. and A. Visser (2005): Problems in the Logic of Provability. Department of Philosophy, Utrecht University, Logic Group Preprint Series 235, May 2005.

10.05.12. The current list of problems in provability algebras composed at the Workshop on Proof Theory and Modal Logic (aka Wormshop) in Barcelona, Spain, April 16-19, 2012: .pdf

Problems in Provability Logic

Intuitionistic arithmetic

The provability logic of Heyting arithmetic HA: decidability, axiomatization.
[Markov] The propositional logic of Kleene realizability.
[Plisko] The propositional logic of Gödel's Dialectica interpretation.
[De Jongh, Visser] Characterization of subalgebras of the Lindenbaum Heyting algebra of HA.
The predicate logics of some extensions of HA: HA+MP, HA+ECT₀.
The admissible propositional inference rules for HA+MP and HA+ECT₀.
Are the Lindenbaum Heyting algebras of HA and HA+RFN(HA) isomorphic?
Is the elementary theory of the Lindenbaum Heyting algebra of HA decidable? Which fragments of it are?
(*) [De Jongh, Visser] Is the downwards extension property of intuitionistic propositional theories equivalent to the property of being projective for infinitely axiomatizable theories?

Bounded arithmetic

The provability logic of bounded arithmetics S₂¹ and S₂: decidability, axiomatization.
(Subproblem) A possibly, though not likely, easier question: does it coincide with GL?
A possibly more relevant question: formulate the provability logic for the right notion of provability for S₂¹.
[Visser] Does the Harrington-Friedman-Goldfarb principle hold in S₂¹?
[Visser] Is Sigma_1-reflection principle equivalent to Sigma_1-disjunction property modulo consistency in S₂¹?

Bimodal and polymodal logics

Classification of bimodal provability logics for pairs of r.e. theories containing a sufficiently strong fragment of PA.
(Subproblem) Classification of bimodal provability logics for pairs of r.e. theories (T,U) such that U is a Pi_1-axiomatizable extension of T.
(Subproblem) Classification of bimodal provability logics of types GL_omega and D.
(*) Is the provability logic of (EA,PRA) a maximal bimodal provability logic of type D?
Provability logics of any natural pair of theories (T,U) such that U is a Pi_1-conservative extension of T, but U is not conservative over T w.r.t. boolean combinations of Sigma_1-sentences.
(*) Characterize the bimodal provability logics of (ISigma_1, IPi_2^-) and other natural pairs of incomparable fragments of PA.

Provability (Magari) algebras

Characterize the isomorphism types of the provability algebras of reasonable theories.
Characterize the definable elements in the provability algebra of PA.
[Shavrukov] Is the (forall)(exists)-fragment of the first order theory of the provability algebra of PA decidable? The same question for the (forall)(exists)(forall)-fragment. (In the following paper it is shown that the (forall)(exists)-fragment of the first order theory of the lattice of Sigma_1-sentences of PA is decidable: P. Lindström and V.Yu. Shavrukov (2008), The (forall)(exists) theory of Peano Sigma_1 sentences, Journal of Mathematical Logic, v.8, 205-208. Abstract The full first order theory of this lattice is undecidable.)
[Shavrukov] Are the provability algebras of PA and PA+Con(PA) isomorphic?
(*) Characterize the subalgebras of free Magari algebras on n generators, for every fixed n.

Interpretability logic and its kin

[Visser] Characterize the interpretability logic of all reasonable theories.
[Ignatiev] The logics of Sigma_1- and Sigma_2-conservativity over PA.
Pi_1-conservativity logics for theories below ISigma_1. (In the following paper it is shown that the logic is the standard one (ILM) for all reasonable theories containing EA plus the parameter-free Pi_1-induction schema: Beklemishev, L.D. and A. Visser (2004), On the limit existence principles in elementary arithmetic and related topics. Department of Philosophy, Utrecht University, Logic Group Preprint Series 224, February 2004. - 30.07.2005)
The interpretability and the Pi_1-conservativity logics for PRA.
Find an explicit axiomatization of the interpretability logic of EA.

Miscellaneous

[Artemov] Consider any arithmetical formula A(x) correctly defining an operator @: phi -> A[phi] on the Lindenbaum boolean algebra of PA. Characterize all possible logics of @. (06.02.2020: Extensions of GL provably satisfying the finite frame property are realizable as logics of formulas satisfying Löb conditions by the results of Fedor Pakhomov, "Semi-provability predicates and extensions of GL". In 11th International Conference on Advances in Modal Logic, Short Presentations, pages 110-115, 2016. Available on-line here.)
(*) [Visser] Do the propositional admissible rules of PA have a left adjoint? In other words, is there an operation # on modal formulas such that S proves Box A -> Box B iff GL proves A^#& Box A^# -> B ? Conjecture: no, and this should be easy to see. (Curiously, this conjecture turned out to be true in that it was easy to see, but false in its actual statement:-) A nice adjoint does exist. See my little note on it. - 10.03.2003)

Graded Provability Algebras

Formulate some general (algebraic) sufficient conditions for the well-foundedness of graded provability algebras. (06.02.2020: A paper by F. Pakhomov and J. Walsh, Reflection ranks and ordinal analysis, contains a result stating a sufficient condition in terms of the soundness of the interpretation of diamond as the uniform reflection principle for Pi_1^1 formulas in second-order arithmetic.)
Develop generalizations of the notion of graded provability algebra suitable for the proof-theoretic analysis of ATR₀ and KP_omega. (06.06.2020: Beklemishev and Pakhomov, Reflection algebras and conservation results for theories of iterated truth, develop the notions suitable for the analysis of theories of predicative strength up to the level of ATR₀.)
Develop a definability theory for graded provability algebras that would allow the box operator to be applicable to (definably) infinite sets of elements.
Find a new combinatorial independent principle that would be motivated by Kripke models for GLP.
Does PA prove consistency of the propositional theory axiomatized over GLP by formulas <n>T, for all n? (The answer is "yes". This problem was solved in L.D. Beklemishev, J.J. Joosten, M. Vervoort (2005): A finitary treatment of the closed fragment of Japaridze's provability logic. Journal of Logic and Computation, v.15, No.4, 2005, 447-463. abstract, .pdf. - 30.07.2005)
Make a fine estimation of the constant for the independent Worm principle à la Weiermann. (This problem is recently solved by G. Lee and A. Weiermann. - 25.12.2002)
(*) Axiomatize the logic of GPA's in the sorted language, where sort n corresponds to arithmetical Pi_{n+1}-sentences. (This has been done in the Master's Thesis of Gerald Berger and published in: Gerald Berger, Lev Beklemishev, Hans Tompits, A many-sorted variant of Japaridze's polymodal provability logic. -06.06.2020)
(*) Axiomatize the fragment of GLP in the language with the following connectives: T, &, <n>, for all n, and =. Develop an arithmetical interpretation of the language, where the variables are interpreted as (possibly infinitely axiomatized) arithmetical theories. (This fragment of GLP has been axiomatized by Evgeny Dashkov, see E.V. Dashkov (2012), On a positive fragment of the provability logic GLP , Mathematical Notes, v.91, No.3, p. 331-346. Abstract. - 10.05.2012)
(*) Show that the positive fragment of the standard provability logic GL (see the previous problem) is arithmetically complete w.r.t. the interpretation of Diamond as full uniform reflection schema in PA. -10.05.2012 (The strictly positive logic of the uniform reflection schema in PA has been characterized in L. Beklemishev, Positive provability logic for uniform reflection principles, Ann. Pure Appl. Logic, 165:1 (2014), 82-105. In fact, this logic strictly extends the strictly positive fragment of GL, the situation turned out to be more interesting than naively conjectured. -06.06.2020)
(*) [Ignatiev] Consider the ordering A<₀ B iff "GLP proves A -> <0> B" on the Lindenbaum algebra of GLP (more precisely, on the part of the Lindenbaum algebra strictly above 0). Is the ordering well-founded, of height epsilon_0? (A positive answer to this question easily follows from the results of this paper: Beklemishev, L.D. (2010): Kripke semantics for provability logic GLP. Annals of Pure and Applied Logic, v. 161, No. 6, 2010, p. 737-744. Preliminary version in: Logic Group Preprint Series 260, November 2007. There it is shown that GLP is complete w.r.t. a certain class of well-founded Kripke models of height less than epsilon_0. Alexandra Podgaits worked out the details in her student paper. - 10.05.2012)

Problems in Arithmetic and Proof Theory

Reflection Principles

Develop versions of reflection principles suitable for an axiomatization of the bounded arithmetic theories S₂ⁱ and T₂ⁱ over PV.
The same for the fragments of Heyting arithmetic HA over the intuitionistic elementary arithmetic.
The same for the fragments of KP_omega over some weak basic set theory. Clarify the analogy between the set-theoretic and the arithmetical reflection principles.
Find the analog of Schmerl's reduction formula for the Church-Kleene ordinal Omega_1.
Are the collection principles BSigma_n equivalent to some form of reflection over EA?

Delta_n-Induction in Arithmetic

[Paris] Is IDelta_n equivalent to LDelta_n? In particular, are the induction schema and the least element principle for Delta_1-formulas equivalent over EA? (This problem was surprisingly solved in the positive in T. Slaman, Sigma_n-bounding and Delta_n-induction. Proc. Amer. Math. Soc., 132: 2449-2456, 2004. The remaining question is whether IDelta_1 is equivalent to LDelta_1 over IDelta_0 (i.e. without assuming the totality of exponentiation). See the following paper for some schemata weaker than Delta_1-induction for which the corresponding question has a negative solution: Beklemishev, L.D. (2003): Quantifier-free induction and the least element schema. Trudy MIAN (Proceedings of the Steklov Institute of Mathematics), v. 242, 50-67. Preliminary version in: Department of Philosophy, Utrecht University, Logic Group Preprint Series 222, April 2003. - 30.07. 2005)
Is there a function f with an elementary graph such that the closure of elementary functions and f under composition and search recursion does not contain the function max_i<xf(i)? (The answer is "no" by the above result of Slaman (and the results of the following paper on search recursion: Beklemishev, L.D. (2003): On the induction schema for decidable predicates. The Journal of Symbolic Logic, 68 (1), p. 17-34. - 30.07.2005)
Is the closure of EA+A, where A is a Pi_2-sentence, by non-nested applications of Delta_1-induction rule always finitely axiomatizable?
Is there a Pi_2-sentence A such that the closure of the theory EA+A under the (k+1)-fold applications of Delta_1-induction rule is properly weaker than the closure under the k-fold applications of this rule, for each k?