Here is a list of selected open problems in the areas of my interests. 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 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.

Problems in Provability Logic

Intuitionistic arithmetic

  1. The provability logic of Heyting arithmetic HA: decidability, axiomatization.
  2. [Markov] The propositional logic of Kleene realizability.
  3. [Plisko] The propositional logic of Gödel's Dialectica interpretation.
  4. [De Jongh, Visser] Characterization of subalgebras of the Lindenbaum Heyting algebra of HA.
  5. The predicate logics of some extensions of HA: HA+MP, HA+ECT0.
  6. The admissible propositional inference rules for HA+MP and HA+ECT0.
  7. Are the Lindenbaum Heyting algebras of HA and HA+RFN(HA) isomorphic?
  8. Is the elementary theory of the Lindenbaum Heyting algebra of HA decidable? Which fragments of it are?
  9. (*) [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

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

Bimodal and polymodal logics

  1. Classification of bimodal provability logics for pairs of r.e. theories containing a sufficiently strong fragment of PA.
  2. (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.
  3. (Subproblem) Classification of bimodal provability logics of types GL_omega and D.
  4. (*) Is the provability logic of (EA,PRA) a maximal bimodal provability logic of type D?
  5. 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.
  6. (*) The bimodal provability logics of (ISigma_1, IPi_2^-) and other pairs of incomparable fragments of PA.

Provability (Magari) algebras

  1. Characterize the isomorphism types of the provability algebras of reasonable theories.
  2. Characterize the definable elements in the provability algebra of PA.
  3. [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.
  4. [Shavrukov] Are the provability algebras of PA and PA+Con(PA) isomorphic?
  5. (*) Characterize the subalgebras of free Magari algebras on n generators, for every fixed n.

Interpretability logic and its kin

  1. [Visser] The interpretability logic of all reasonable theories.
  2. [Ignatiev] The logics of Sigma_1- and Sigma_2-conservativity over PA.
  3. 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)
  4. The interpretability and the Pi_1-conservativity logic for PRA.
  5. An axiomatization of the interpretability logic of EA.


  1. [Artëmov] 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 @.
  2. (*) [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

  1. Formulate some general (algebraic) sufficient conditions for the well-foundedness of graded provability algebras.
  2. Develop generalizations of the notion of graded provability algebra suitable for the proof-theoretic analysis of ATR0 and KP_omega.
  3. Develop a definability theory for graded provability algebras that would allow the box operator to be applicable to (definably) infinite sets of elements.
  4. Find a new combinatorial independent principle that would be motivated by Kripke models for GLP.
  5. 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 recently 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)
  6. 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)
  7. (*) Axiomatize the logic of GPA's in the sorted language, where sort n corresponds to arithmetical Pi_{n+1}-sentences.
  8. (*) 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.
  9. (*) [Ignatiev] Consider the ordering A<0 B iff "GLP proves A -> <0> B" on the Lindenbaum algebra of GLP. Is the ordering well-founded, of height epsilon_0+1?

Problems in Arithmetic and Proof Theory

Reflection Principles

  1. Develop versions of reflection principles suitable for an axiomatization of the bounded arithmetic theories S2i and T2i over PV.
  2. The same for the fragments of Heyting arithmetic HA over the intuitionistic elementary arithmetic.
  3. 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.
  4. Find the analog of Schmerl's reduction formula for the Church-Kleene ordinal Omega_1.
  5. Are the collection principles BSigma_n equivalent to some form of reflection over EA?

Delta_n-Induction in Arithmetic

  1. [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)
  2. 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 maxi<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)
  3. 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?
  4. 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?