In September 1984, Vladimir Rybakov published his algorithm to determine the admissible rules of intuitionistic propositional logic. Creating this algorithm was no easy matter: the conceptual machinery required to do so had to be created nearly from scratch. Numerous logicians have used and explored comparable concepts in the years since. At the end of my time as a PhD candidate, I connected Rybakov’s approach to these now well-understood concepts. The resulting paper Decidability of Admissibility has just been published.
Proofs and refutations
A formal logical system typically consists of a language to talk about (formulas) and a mechanism of axioms and rules to construct proofs of some of these formulas. These formulas can be interpreted in hypothetical situations (models). In a well-designed system, every formula that can be proven is true in all models (soundness) and every formula that cannot be proven can be refuted by a model (completeness). Many concepts that logicians work with exist either on the side of the models or on the side of the proofs, and ideally, have a mirror image on the other side.
Can you create an algorithm that determines whether a formula can be proven? That depends on the logic. A common approach to create such an algorithm is to step through the mirror. Instead of searching for a proof of the formula, you can search for a model that refutes it. After all, if no such model exists then there must a proof. You can therefore determine whether a proof exists for a formula by checking all models that could refute it one-by-one. There is a significant caveat: this only works if you don’t need to check too many models and checking them doesn’t take too much time.
Making sure that these caveats are met is no small feat, as in principle there may be infinitely many models — or infinitely large models – you would have to check. The challenge is in showing that it suffices to only check a bounded and finite amount of things. This approach works for intuitionistic propositional logic, as first shown in 1946 — although an algorithm had been already provided through other means in 1934.
A problem by Friedman
When you add new rules to a logical system you create new ways of making proofs. As a consequence, a formula that wasn’t provable before now very well may be. When adding a rule doesn’t make any new formula provable, the rule is said to be an admissible rule. In his 1975 paper of 102 problems, Harvey Friedman asked for an algorithm that determines whether a rule is admissible in intuitionistic propositional logic. Rybakov provided the answer in his groundbreaking paper in 1984.
Rybakov applied what amounts to an intricate variant of the trick we described above. His approach uses theoretical concepts that were still very new at the time. Hence these intricacies had to be solved from scratch. Metaphorically, he was painting a multi-storied mural without pre-made scaffolding. This works out well if you’re tall enough or can jump really well, but it definitely adds to the challenge.
In the years since 1984, the concepts used in Rybakov’s approach have been explored in multiple settings. When working on my dissertation, I came across well-studied notions that could be applied as theoretical scaffolding to Rybakov’s approach. A key role is played by exact formulas (related to proofs of formulas) and their mirror-image extendible formulas (related to models that refute formulas).
In my paper, I introduced generalized versions of these concepts based on the 2013 preprint by Nick & Guram Bezhanishvili. These generalizations provided adequate scaffolding to re-paint Rybakov’s mural, making the overall approach more accessible. The concepts as described in my paper are used throughout my dissertation — especially chapter 4 on decidability.
When writing all of this in 2014, I definitely had the benefit of hindsight. I am very grateful for having had the opportunity to learn from the logicians who work in this field. Dick de Jongh, who first published about exact formulas in 1982, introduced me to this notion and to his approach to universal models. I learned about the early origins of this field through Alex Citkin, who has been writing about admissible rules since 1977 and whose early insights shaped the field.
Vladimir Rybakov met with me in March 2014 to discuss my ideas, which helped me to better understand his way of thinking. Later that year, I submitted my paper to the Bulletin of Symbolic Logic. This paper has finally been published in March 2021. It took quite some time, but looking back, I’m grateful for having had the opportunity to make this journey.