On a Problem of Friedman and its Solution by Rybakov: Decidability of the Admissible Rules in Intuitionistic Propositional Logic
Jeroen Goudsmit · Utrecht University Repository (Utrecht University) · 2014
Rybakov (1984) proved that the admissible rules of IPC are decidable. We give a proof of the same theorem, using the same core idea, but couched in the many notions that have been developed in the mean time. In particular, we illustrate how the argument can be interpreted as using refinements of the notions of exactness and extendibility.