One of the major remaining open problems in Provability Logic.
Studied by A. Visser in his Ph.D. dissertation
Aspects of Diagonalization and Provability, Utrecht, 1981.
Partial results:
- Decidability of the letterless fragment. (Visser, see above)
- More generally, the logic of Sigma_1-substitutions, that is,
the logic where the variables are interpreted as Sigma_1-sentences,
is decidable.
A. Visser. Propositional combinations of Sigma-sentences
in Heyting's arithmetic.
Department of Philosophy, Utrecht University,
Logic
Group Preprint Series 117, 1994.
- A number of valid principles that go beyong the intuitionistic
version of GL are known. (Visser, Leivant)
- Recently it was shown by Visser that the propositional
admissible rules of HA coincide with those of intuitionistic
propositional logic.
A. Visser. Rules and arithmetics. Department of Philosophy, Utrecht University,
Logic
Group Preprint Series 186, June 1998.
Every such rule yields a valid principle of the
logic in question. The admissibility of a rule is decidable by Rybakov.
Iemhoff recently gave an axiomatization of the basis of admissible rules,
conjectured by Visser and De Jongh. It follows from her result that
every admissible rule is also HA-provably admissible.
- An obvious upper bound to the arithmetical complexity of the logic
is Pi_2.