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 lev@phil.uu.nl.
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

## Bounded arithmetic

## Bimodal and polymodal logics

## Provability (Magari) algebras

## Interpretability logic and its kin

## Miscellaneous

# Graded Provability Algebras

# Problems in Arithmetic and Proof Theory

## Reflection Principles

## Delta_n-Induction in Arithmetic

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.

- 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
_{0}. - The admissible propositional
inference rules for HA+MP and HA+ECT
_{0}. - 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?

- The provability logic of bounded arithmetics S
_{2}^{1}and S_{2}: 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_{2}^{1}. - [Visser]
Does the Harrington-Friedman-Goldfarb principle
hold in S
_{2}^{1}? - [Visser]
Is Sigma_1-reflection principle equivalent to Sigma_1-disjunction
property modulo consistency in S
_{2}^{1}?

- 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.
- (*) The bimodal provability logics of (ISigma_1, IPi_2^-) and other pairs of incomparable fragments of PA.

- 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.
- [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.

- [Visser] 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 logic for PRA.
- An axiomatization of the interpretability logic of EA.

- [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 @.
- (*) [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.
- Develop generalizations of the notion of graded provability
algebra suitable for the proof-theoretic analysis of ATR
_{0}and KP_omega. - 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 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) - 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.
- (*) 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.
- (*) [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?

- Develop versions of reflection principles suitable for
an axiomatization of the bounded arithmetic theories
S
_{2}^{i}and T_{2}^{i}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?

- [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<x}f(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?