| Результаты этапа: Установлена связь между квадратами Сегерберга модальных логик и тождествами в реляционных алгебрах. Найдено новое, более короткое доказательство финитной аппроксимируемости квадратов Сегерберга минимальной модальной логики К. Доказана финитная аппроксимируемость квадратов Сегерберга полимодальных логик с аксиомами рефлексивности и сериальности. Введено понятие импликативной глубины суперинтуиционистской логики; для некоторых локально табличных логик найдены ее значения или верхние оценки.
Найдены достаточные условия для полноты по Крипке логики, получающейся расширением некоторой логики модальностью транзитивного замыкания. Более точно, доказано, что если модальная логика является канонической и допускает определимые фильтрации, то ее расширение модальностью транзитивного замыкания является полной по Крипке и тоже допускает определимые фильтрации.
Построены полные аксиоматические системы для градуированных полимодальных логик с зависимыми модальностями, в которых некоторые из модальностей могут быть транзитивными, а зависимости выражены в виде импликаций между модальностями.
Интуиционистская эпистемическая логика IEL (С. Артемов, Т. Протопопеску, 2014) описывает модальность знания в контексте интуиционистской логики. В отличие от классической логики знаний здесь справедлив принцип ко-рефлексии, утверждающий, что из интуиционистской верности факта можно извлечь справедливость утверждения об его известности. Обратное не имеет места, т.е утверждение о знании факта оказывается менее информативным, чем утверждение об его истинности. Ранее в процессе исполнения проекта была предложена топологическая семантика для логики IEL, доказаны соответствующие теоремы о корректности и полноте, установлена разрешимость логики IEL. В 2015 г. получены аналогичные результаты для расширения IEL+ логики IEL принципом идемпотентности знания.
Исходная формулировка логики IEL представляет собой исчисление гильбертовского типа. Найдены эквивалентные секвенциальные формулировки. Они задают ту же логику, но различаются поведением процедуры поиска вывода снизу-вверх.
Описана семантика некоторых логик доказательств для двух взаимодействующих дедуктивных систем разной дедуктивной силы. Доказаны теоремы о полноте.
Доказан критерий выводимости во фрагменте исчислении Ламбека без умножения с правилом ослабления в терминах сетей доказательства.
Для расширения исчисления Ламбека с помощью экспоненциальной и субэкспоненциальной (допускающей только правила сокращения и перестановки) модальностей построены исчисления генценовского типа,
правильно учитывающие ламбеково ограничения на непустоту левой части секвенций. Для этих исчислений доказана алгоритмическая неразрешимость проблем выводимости, в том числе во фрагменте с одним делением.
Для исчисления Ламбека, обогащённого итерацией Клини, построено инфинитарное исчисление генценовского типа и доказана полнота относительно языковых моделей его фрагмента без умножения, в котором связка "итерация" допускается только в знаменателях.
Построено полное интуиционистское исчисление высказываний, использующее только эквиваленцию и конъюнкцию в качестве единственных логических связок.
Проведено сравнение различных интерпретаций базисной логики предикатов. Доказано, что семантика абсолютной арифметической реализуемости и семантика, основанная на примитивно-рекурсивной реализуемости, введенной С. Салехи, не совпадают. А именно, построен пример предикатной форимулы, которая примитивно-рекурсивно реализуема, но не является абсолютно арифметиччески реализуемой.
|
