Abstract:
In the early 2000s, the key questions of the theory of admissible rules (decidability by admissibility, the presence of a basis) were resolved for most basic non-classical logics. The question arose about the direction of development of this theory. One of the directions of further study of admissible rules became globally admissible inference rules, i.e. rules admissible in all (finitely approximable) extensions of a given logic or in some class of extensions. For them, the problem of decidability, the presence of a finite or explicit basis, etc. also arises.
In the presented work the problem of decidability of globally admissible rules of logic $S4$ is investigated. For rules, the model for which satisfies some natural properties, the necessary and sufficient condition of global admissibility in logic $S4 \ (Grz)$ is obtained. The specified properties of the model $M(r; X)$ do not depend on the choice of the given logic, which allowed to apply the technique of truth of the rule on the n-characteristic model. Based on the obtained description, an algorithm for checking the global admissibility of an arbitrary rule in a reduced form is proposed. Thus, the problem of global admissibility in logic $S4 \ (Grz)$ is decidable.
Keywords:modal logic, frame and model Kripke, admissible and globally admissible inference rule.
Fulltext:
PDF file (784 kB)