О некоторых исчислениях модальной логики

Рассматриваются исчисления, получающиеся в результате добавления к исчислению $S5$ правил для кванторов и для равенства. В некоторых из этих исчислений формула $x=y\supset\square (x=y)$ оказывается невыводимой, в других она выводима. Для каждого из рассматриваемых исчислений строятся свободные ют сечения генценовские варианты, выводимыми объектами которых являются секвенции, и свободные от сечения генценовские генценовские варианты, выводимыми объектами которых являются системы секвенций. Строится погружающая операция из предикатного $S5$ в классическое исчисление предикатов, основанная на замене модальных знаков кванторами по дополнительному аргументу. Доказываются теоремы о специализации формы вывода в предикатном $S5$, и на их основе дано синтаксическое доказательство теоремы С. Крипке о неразрешимости одноместного фрагмента предикатного $S5$. Исследуется также вопрос о добавлении модальных связок к конструктивному исчислению предикатов. Библ. 15 назв.