Abstract:
In [2] the classification of extensions of the minimal logic $\mathrm{J}$ using slices was introduced and decidability of the classification was proved. We will consider extensions of the logic $ \mathrm{GL} = \mathrm{J} + (A \vee \neg A) $. The logic $\mathrm{GL}$ and its extensions have been studied in [8, 9]. In [6], it is established that the logic $\mathrm{GL}$ is strongly recognizable over $\mathrm{J}$, and the family of extensions of the logic $\mathrm{GL}$ is strongly decidable over $\mathrm{J}$. In this paper we prove strong decidability of the classification over $\mathrm{GL}$: for every finite set $ Rul $ of axiom schemes and rules of inference, it is possible to efficiently calculate the slice number of the calculus obtained by adding $ Rul $ as new axioms and rules to $\mathrm{GL}$.