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 firstname.lastname@example.org.
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
in Barcelona, Spain, April 16-19, 2012: .pdf
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
(*) 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
Characterize the definable elements in the provability algebra
[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
(*) 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
[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.
(*) [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)
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 a definability theory for graded provability algebras that
would allow the box operator to be applicable to (definably) infinite sets
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)
(*) 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)
Develop versions of reflection principles suitable for
an axiomatization of the bounded arithmetic theories
S2i and T2i 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
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)
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?