A criterion for admissibility of rules in the modal system S4 and intuitionistic logic.

*(English. Russian original)*Zbl 0598.03013
Algebra Logic 23, 369-384 (1984); translation from Algebra Logika 23, No. 5, 546-572 (1984).

This important paper contains a positive solution of the Kuznetsov- Friedman problem on decidability of the set of rules admissible in intuitionistic propositional logic Int. It is known (Harrop 1960, Mints 1968) that Int is structurally incomplete, i.e. there are admissible but inderivable rules. Inference rules are defined as pairs of formulas with propositional parameters \(A(x_ 1,...,x_ n)/B(x_ 1,...,x_ n)\); such a rule is admissible iff Int\(\vdash A(C_ 1,...,C_ n)\) implies Int\(\vdash B(C_ 1,...,C_ n)\) for all formulas \(C_ 1,...,C_ n\). The rule is derivable iff Int\(\vdash A(x_ 1,...,x_ n)\to B(x_ 1,...,x_ n).\)

The positive solution of this problem by the author was preceded by his investigation of the same problem for other intermediate and modal logics. Call a logic A-decidable if the set of its admissible rules is decidable. The following logics were proved by the author to be A- decidable: S5 (1979), tabular and pre-tabular logics (1981), extensions of S4.3 (1982), logics of finite slices (1984), S4 and Int (the present paper), Grz (1984, published in 1986).

It follows from the results of the paper that the universal first order theories of Lindenbaum algebras for S4 and Int (i.e. of \(F_{\omega}(S4)\) and \(F_{\omega}(Int))\) are decidable (while their first-order theories are not - see the author’s paper in Mat. Zametki 37, No.6, 797-802 (1985; Zbl 0593.03041).

The positive solution of this problem by the author was preceded by his investigation of the same problem for other intermediate and modal logics. Call a logic A-decidable if the set of its admissible rules is decidable. The following logics were proved by the author to be A- decidable: S5 (1979), tabular and pre-tabular logics (1981), extensions of S4.3 (1982), logics of finite slices (1984), S4 and Int (the present paper), Grz (1984, published in 1986).

It follows from the results of the paper that the universal first order theories of Lindenbaum algebras for S4 and Int (i.e. of \(F_{\omega}(S4)\) and \(F_{\omega}(Int))\) are decidable (while their first-order theories are not - see the author’s paper in Mat. Zametki 37, No.6, 797-802 (1985; Zbl 0593.03041).

Reviewer: V.B.Shekhtman

##### MSC:

03B45 | Modal logic (including the logic of norms) |

03F50 | Metamathematics of constructive systems |

03B25 | Decidability of theories and sets of sentences |

03B55 | Intermediate logics |

03B60 | Other nonclassical logic |

03G25 | Other algebras related to logic |

##### References:

[1] | G. E. Mints, ”Admissible and arbitrary rules,” Zap. Nauchn. Sem. LOMI Akad. Nauk SSSR,8, 189–191 (1968). · Zbl 0207.00401 |

[2] | G. E. Mints, ”Arbitrariness of admissible rules,” J. Sov. Math.,6, No. 4 (1976). |

[3] | V. V. Rybakov, ”Admissible rules of pretable modal logics,” Algebra Logika,20, No. 4, 440–464 (1981). · Zbl 0489.03005 |

[4] | V. V. Rybakov, ”The decidability of the admissibility problem in extensions of the logic S4.3,” Sixth All-Union Conf. of Math. Logic, Lecture Theses, Tbilisi (1982), p. 158. |

[5] | V. V. Rybakov, ”The decidability of the admissibility problem in finite-layer modal logics,” Algebra Logika,23, No. 1, 100–116 (1984). · Zbl 0576.03012 |

[6] | V. V. Rybakov, ”Elementary theories of free closure algebras,” Sixteenth All-Union Conf. on Algebra, Lecture Theses, Leningrad (1981), p. 116. · Zbl 0489.03005 |

[7] | A. I. Tsitkin, ”On admissible rules in the intuitionistic propositional logic,” Mat. Sb.,102, No. 2, 314–323 (1977). · Zbl 0386.03011 |

[8] | A. I. Tsitkin, ”On structurally complete superintuitionistic logics,” Dokl. Akad. Nauk SSSR,241, No. 1, 40–43 (1978). · Zbl 0412.03009 |

[9] | H. Freedman, ”A hundred and two problems in mathematical logic,” J. Symb. Logic,40, No. 2, 113–130 (1975). · Zbl 0318.02002 · doi:10.2307/2271891 |

[10] | R. Harrop, ”Concerning formulas of the types AVC, A\(\times\)B(x) in intuitionistic formal systems,” J. Symb. Logic,25, No. 1, 27–32 (1960). · Zbl 0098.24201 · doi:10.2307/2964334 |

[11] | J. Port, ”The deducibilities of S5,” J. Philos. Logic,10, 409–422 (1981). · Zbl 0475.03005 · doi:10.1007/BF00248735 |

[12] | K. Segerberg, ”An essay in classical modal logic,” University of Uppsala, Uppsala (1971). · Zbl 0311.02028 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.