Сильная консервативность и полнота для фрагментов инфинитарной логики действий

Аннотация

В работе рассматриваются фрагменты инфинитарной логики действий, т.е. алгебраической логики *-непрерывных решёток Клини с делениями, с точки зрения следования из (возможно бесконечных) множеств гипотез. Результаты статьи разбиваются на две группы. Во-первых, доказано, с помощью теоремы о нормализации сечений, что элементарные фрагменты, получаемые ограничением множества связок, являются в сильном смысле консервативными в полной системе. Это означает, что консервативность имеет место не только для чистой выводимости, но и для выводимости из множеств гипотез. Утверждение доказано в присутствии итерированных делений --- составных связок из деления и итерации Клини в знаменателе. Во-вторых, для фрагмента с делениями, пересечением и итерированными делениями доказаны свойства сильной полноты относительно естественных классов моделей на алгебрах языков и алгебрах бинарных отношений.