The decidability of admissibility problems for modal logics S4.2 and S4.2Grz and superintuitionistic logic KC (Q1317616)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The decidability of admissibility problems for modal logics S4.2 and S4.2Grz and superintuitionistic logic KC |
scientific article |
Statements
The decidability of admissibility problems for modal logics S4.2 and S4.2Grz and superintuitionistic logic KC (English)
0 references
12 April 1994
0 references
In studies dealing with intuitionistic logic the following question arises: Is the admissibility problem for the logic Int decidable? (the Kuznetsov-Friedman problem). In a paper of \textit{V. V. Rybakov} [Algebra Logika 20, 440-464 (1981; Zbl 0489.03005)], it was noted that a rule \(\alpha/\beta\) is admissible in a superintuitionistic logic \(\lambda\supseteq\text{Int}\) if and only if the rule \(T(\alpha)/T(\beta)\) is admissible in \(\sigma(\lambda)\) -- the greatest modal companion of \(\lambda\) -- where \(T(\alpha)\) is the Gödel translation of the formula \(\alpha\). In another paper of Rybakov [ibid. 23, No. 5, 546-572 (1984; Zbl 0598.03013)], the Kuznetsov-Friedman problem was solved positively, using this fact and the decidability of the admissibility problem for modal logic S4, the modal companion of Int. Of special interest among superintuitionistic logics is the logic KC with the Weak Law of Excluded Middle. The greatest modal companion of KC is the logic S4.2Grz. In the present paper we obtain algorithms to verify whether the inference rules in the modal logics S4.2Grz are admissible. As a consequence, it is proved that the admissibility problem for KC is decidable.
0 references
admissibility problem
0 references
superintuitionistic logic
0 references
Kuznetsov-Friedman problem
0 references
decidability
0 references
Weak Law of Excluded Middle
0 references
modal companion
0 references
algorithms
0 references