Семинары
Все семинары можно посмотреть на нашем Youtube канале.
Докладчик: Анна Задаля
Название: Сложность логики LTL
YouTube
Дата: 15.11.2024
Аннотация:
Темпоральные логики являются расширениями классической логики высказываний, полученными путём добавления специальных модальностей. Эти модальности, темпоральные операторы, позволяют формулировать утверждения, истинность которых может меняться с течением времени. Простота и выразительность темпоральных логик позволяют использовать их для описания работы различных систем, когда важно уделить внимание последовательности переходов между различными состояниями системы. Логика LTL, также известная как логика линейного времени, впервые была описана в [1].
Данный доклад будет посвящён вычислительной сложности логики линейного времени, а также некоторых её фрагментов.
[1] A. Pnueli. The temporal logic of programs, In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (Providence, RI.). IEEE, New York, 1971, pp. 46-57.
Докладчик: Александр Герасимов
Название: Бесконечнозначная первопорядковая логика Лукасевича: исчисления для поиска вывода и полнота инфинитарного аналитического исчисления для предварённых предложений. Часть вторая
YouTube
Дата: 08.11.2024
Аннотация:
Бесконечнозначная первопорядковая логика Лукасевича относится к математическим нечётким логикам и служит для формализации приближённых рассуждений. Множество всех общезначимых предложений (и множество всех общезначимых предварённых предложений) этой логики неперечислимо; поэтому для неё не существует полного исчисления с рекурсивным множеством аксиом и конечным числом рекурсивных правил вывода. В докладе мы покажем, как удалось доказать полноту одного инфинитарного аналитического исчисления для предварённых предложений данной логики с помощью построений, полученных при разработке ориентированных на поиск вывода исчислений для рассматриваемой логики.
Доклад основан на статьях:
[1] A.S.Gerasimov, "Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic", Siberian Electronic Mathematical Reports, Vol.17, 2020, pp.1869-1899, https://doi.org/10.33048/semi.
[2] A.S.Gerasimov, "Comparing calculi for first-order infinite-valued Lukasiewicz logic and first-order rational Pavelka logic", Logic and Logical Philosophy, Vol.32, No.2, 2022, pp.269-318, https://doi.org/10.12775/LLP.
а также на некоторых неопубликованных результатах докладчика.
В начале второй части доклада будет изложено основное из его первой части, прошедшей 27.09.2024; так что прослушивание первой части доклада не обязательно для понимания второй.
Докладчик: Дарья Криницина
Название: Формализация теории ∞-категорий
YouTube
Дата: 18.10.2024
Аннотация:
Я расскажу про теорию типов, чем она отличается от теории множеств и как с ее помощью можно прийти к понятию ∞-категории.
Докладчик: Borja Sierra Miranda
Название: Non-wellfounded master modality: from cut admissibility to cut elimination (доклад на английском языке)
YouTube
Дата: 11.10.2024
Аннотация:
In a previous talk, we provided a method for eliminating cuts in non-wellfounded proofs with a local-progress condition, these being the simplest kind of non-wellfounded proofs. The method consisted of splitting the proof into nicely behaved fragments. This paper extends our method toproofs based on simple trace conditions. The main idea is to split the system with the trace condition into infinitely many local-progress calculi that together are equivalent to the original trace-based system. This provides cut elimination, via cut admissibility, using only basic tools of structural proof theory and corecursion, which is needed due to the non-wellfounded character of proofs. We will employ our method to obtain syntactic cut elimination for K+, the system of modal logic with the master modality.
Докладчик: Елена Попова
Название: Логика свидетельств: обзор
YouTube
Дата: 04.10.2024
Аннотация:
Доклад будет посвящен обзору логик свидетельств. Это явные аналоги модальных логик, в которых вместо модальности \Box используются выражения вида "t:ф", где t -- свидетельский терм. Они интерпретируются как "t есть свидетельство в пользу ф". Первая пропозициональная логика свидетельств LP, введенная С.Н. Артёмовым в 1995 году, соответствует модальной логике S4 (см. [1]). Дальнейшие исследования (см. [2] в качестве обзорной работы) описывают логики свидетельств для модальных систем K, KT, K4 и других. Семантика для этих логик была определена и изучена С.Н. Артёмовым и М. Фиттингом. В докладе мы опишем наиболее известные логики свидетельств, их свойства и семантику для них. Также планируется обсудить логику свидетельств первого порядка. Мы опишем синтаксис этой логики, её семантику и связь с модальной логикой предикатов.
1. Artemov S. N. Operational Modal Logic : tech. rep. / Mathematical Sciences Institute, Cornell University. 1995. No. 95–29.
2. Artemov S. N., Fitting M. Justification Logic: Reasoning with Reasons. Cambridge University Press, 2019.
Докладчик: Александр Герасимов
Название: Бесконечная первопорядковая логика Лукасевича
YouTube
Дата: 27.09.2024
Аннотация:
Бесконечнозначная первопорядковая логика Лукасевича относится к математическим нечётким логикам и служит для формализации приближённых рассуждений. Множество всех общезначимых предложений (и множество всех общезначимых предварённых предложений) этой логики неперечислимо; поэтому для неё не существует полного исчисления с рекурсивным множеством аксиом и конечным числом рекурсивных правил вывода. В докладе мы покажем, как удалось доказать полноту одного инфинитарного аналитического исчисления для предварённых предложений данной логики с помощью построений, полученных при разработке ориентированных на поиск вывода исчислений для рассматриваемой логики.
Доклад основан на статьях:
[1] A.S.Gerasimov, "Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic", Siberian Electronic Mathematical Reports, Vol.17, 2020, pp.1869- 1899, https://doi.org/10.33048/semi.
[2] A.S.Gerasimov, "Comparing calculi for first-order infinite-valued Lukasiewicz logic and first-order rational Pavelka logic", Logic and Logical Philosophy, Vol.32, No.2, 2022, pp.269-318, https://doi.org/10.12775/LLP.
а также на некоторых неопубликованных результатах докладчика.
Докладчик: Станислав Сперанский
Название: Сильная неразрешимость и первая теорема Гёделя о неполноте
YouTube
Дата: 20.09.2024
Аннотация:
Теория Г называется сильно неразрешимой, если всякая теория, совместная с Г, неразрешима. Известно, что такие теории существуют: в качестве примера можно взять некоторую конечно аксиоматизируемую «минимальную» арифметику, которую мы будем обозначать через MA. Из сильной неразрешимости MA следует современная версия первой теоремы Гёделя о неполноте (в форме Россера), а также теорема Чёрча над арифметической сигнатурой. На самом деле, первая теорема Гёделя в известном смысле равносильна сильной неразрешимости MA (по модулю нескольких простых наблюдений). Кроме того, MA интерпретируется в теории дискретно упорядоченных колец, а потому последняя также сильно неразрешима.
В ходе доклада мы обсудим сильную неразрешимость MA и ряд смежных результатов.
Докладчик: Елена Попова
Название: Логика свидетельств первого порядка со связывающей модальностью
YouTube
Дата: 07.06.2024
Аннотация:
Доклад будет посвящен логике свидетельств первого порядка (Яворская 1998; Артемов, Яворская, 2001). Первопорядковая логика свидетельств дает возможность различать глобальные и локальные параметры в доказательствах. Например, для формулы F(x) с параметром x следует различать следующие утверждения:
«t --- доказательство формулы F(x), содержащей x свободно»,
«t --- доказательство формулы F(x) для конкретного значения x», где x рассматривается как параметр.
В языке модальной логики первого порядка тоже можно различать глобальные и локальные параметры с помощью связывающих модальностей (Артемов, Яворская, 2016). В докладе будет представлена логика свидетельств первого порядка одновременно со свидетельскими термами и связывающими модальностями. Будет рассмотрена семантика Крипке для данной логики, а также изложена теорема о сильной полноте.
Литература:
S.N. Artemov and T.L. Yavorskaya. On first order logic of proofs. Moscow Mathematical Journal, 1:475–490, 2001.
S.N. Artemov & T.L. Yavorskaya. Binding modalities. Journal of Logic and Computation, 26(1):451–461, 2016.
T.L. Yavorskaya. Nonaxiomatizability of predicate logics of proofs. Vestnik Moskovskogo Universiteta. Seriya 1. Matematika. Mekhanika, (6):18–22, 1998.
S.N. Artemov & M. Fitting. Justification Logic: Reasoning with Reasons, New York: Cambridge University Press. 2019.
Докладчик: Borja Sierra Miranda
Название: Coalgebraic proof translations for non-wellfounded proofs (доклад на английском языке)
YouTube
Дата: 31.05.2024
Аннотация:
Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constraint to the possible infinite paths appearing in a proof. Among these conditions, one of the simplest is enforcing that any infinite path goes through the premise of a rule infinitely often. Systems of this kind appear for modal logics with conversely well-founded frame conditions like GL or Grz.
In this talk, we introduce a uniform method to define proof translations for such systems, guaranteeing that the condition on infinite paths is preserved. In addition, as particular instance of our method, we establish cut-elimination for a non-wellfounded system of the logic Grz. Our proof relies only on the categorical definition of corecursion via coalgebras and it has a highly resemblance to cut elimination in the (standard) finitary setting.
Докладчик: Александр Гагарин
Название: Произведения хорновых модальных логик
YouTube
Дата: 24.05.2024
СЛАЙДЫ
Аннотация:
Среди полимодальных логик часто рассматривают те, что получаются "комбинированием" нескольких одномодальных. Один из таких способов комбинации это, так называемое, произведение двух модальных логик. Известны различные примеры как разрешимых (например, KxK), так и неразрешимых (например, K4xK4) произведений.
В докладе будет рассмотрена конструкция "фильтрации через бисимуляцию" (V. Shehtman. Filtration via Bisimulation. In Advances in Modal Logic 2004, pp. 289-308) применительно к некоторым произведениям хорновых логик. Конкретно планируется доказать критерий разрешимости произведений вида (K + ♢^n ☐p -> ☐^m p) x (K + ♢^k ☐p -> ☐^l p).
Докладчик: Swapnil Ghosh
Название: An Exploration of Contraction Free Arithmetic (доклад на английском языке)
YouTube
Дата: 10.05.2024
Аннотация:
We will present a proof-theoretic study of Contraction-Free Arithmetic (CFA), which is a first-order arithmetical theory based on a logic (GQC) that constitutes the multiplicative fragment of LK without the structural rules of contraction. In the first part of the talk, we provide some justifications for our choices in the axiomatization of CFA and thus claim that CFA is a natural framework to study the effects of removing contraction on arithmetic. We go on the show that any Π_2 formula provable in the arithmetical theory of I∆_0 is also provable in CFA. Subsequently, we utilize the coding of finite sequences in I∆0 and show that any primitive recursive function is provably recursive in CFA. In the final part of the talk, we provide a classification of provably recursive functions of CFA and show that the provably recursive functions of CFA is exactly the class of primitive recursive functions. Consequently, the essential result of the present work is that CFA not only expands the class of provably recursive functions beyond those of I∆_0, but also establishes its distinctiveness from PA
Докладчик: Федор Пахомов
Название: Тесные и Сверх-Тесные порядки
YouTube
Дата: 26.04.2024
Аннотация:
В этом докладе я дам введение в теорию тесных (wqo) и сверх-тесных (bqo) порядков. Также я расскажу про подсчет максимальных порядковых типов линеаризаций тесных порядков и про изучение этих понятий с точки зрения обратной математики.
В качестве вводного текста к этой теме можно использовать R. Fraisse "Theory of Relations" (https://www.google.com/books/
Докладчик: Виталий Гулевский
Название: Двойственность в интуиционистской логике высказываний
YouTube
Дата: 12.04.2024
Аннотация:
Двойственной по отношению к теории доказательства концепцией является теория опровержения. Наша цель состоит в том, чтобы понять, как выявить такую формулу, для которой есть доказательство тогда, когда наперед заданная его не имеет. Мы рассмотрим предложенный в статье новый подход к построению двойственной формулы для произвольной пропозициональной формулы. Этот новый алгоритмический метод построения основан на теоретико-автоматном взгляде на поиск доказательств.
Доклад основан на статье Paweł Urzyczyn, «Duality in Intuitionistic Propositional Logic», 26th International Conference on Types for Proofs and Programs (TYPES 2020). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021.
Докладчик: Дарья Криницина
Название: Теорема Биркгофа для квазимногообразий
YouTube
Дата: 05.04.2024
Аннотация:
Я расскажу доказательство аналога теоремы Биркгофа для квазимногообразий. Данная теорема утверждает что некоторый класс алгебр К может быть аксиоматизирован квазитождествами тогда и только тогда когда он замкнут относительно взятия изоморфизмов подалгебр произведений ультрапроизведений (ISPP_U) и содержит тривиальную
алгебру. Для доказательства теоремы вводится важнейшая конструкция ультрапроизведения и используются знаменитые теоремы логики -- теорема Лося и теорема о компактности.
Литература: S. Burris, H. P. Sankappanavar. "A course in universal algebra." https://www.math.uwaterloo.ca/
Докладчик: Владимир Шейн
Название: Внутренняя логика топосов и её приложения в алгебраической геометрии
YouTube
Дата: 22.03.2024
Аннотация:
В любой категории существует “внутренний язык”, определяемый функтором точек Гротендика. В случае, когда категория обладает некоторой дополнительной структурой, этот язык позволяет описывать и обобщать базовые понятия математической логики с категорной точки зрения. В своём докладе я напомню несколько вещей из логики топосов, после чего расскажу как внутренняя логика в категории пучков на топологическом пространстве (или, более общо, схеме) может использоваться, чтобы доказывать нетривиальные результаты в алгебраической геометрии.
Литература: S. Mac Lane, I. Moerdijk. Sheaves in Geometry and Logic (Общий учебник по теории топосов)
Ingo Blechschmidt. Using the internal language of toposes in algebraic geometry, (https://arxiv.org/abs/2111.03
Докладчик: Александр Колпащиков
Название: Неразрешимые суперинтуиционистские исчисления и закон исключённого третьего
YouTube
Дата: 15.03.2024
Аннотация:
В тридцать пятом выпуске Оксфордского руководства по логике приводится доказательство существования неразрешимой суперинтуиционистской логики. Докладчик использовал этот метод для доказательства, что такая неразрешимая логика может содержать ещё и формулу ¬p∨¬¬p (закон исключённого третьего). Будет рассказано про машины Минского, сопоставление машинам шкал Крипке, создание формул, опровергаемых лишь в определённых точках шкалы, и про то, как инструкции неразрешимой машины Минского нам помогают при определении искомой аксиоматики. Доклад основан на 16 главе книги Александра Чагрова и Михаила Захарьящева -- Modal Logic. Oxford, 1997.
Докладчик: Никита Лукашов
Название: Допустимые правила в модальных логиках
YouTube
Дата: 01.03.2024
СЛАЙДЫ
Аннотация:
Правило вывода в логике L называется допустимым, если множество теорем логики L не изменяется при добавлении к ней этого правила. В своём прошлом докладе я рассказал о проблеме допустимости в интуиционистской логике высказываний IPC и её решении. Те же самые вопросы о разрешимости и наличии базиса допустимых правил можно спросить про модальные логики.
В 1984 и 1990 г.г. В.В. Рыбаков показал разрешимость проблемы допустимости в модальных логиках S4 и GL соответственно, а также установил у них отсутствие конечного базиса допустимых правил вывода. Позже Владимиром Владимировичем был предложен бесконечный базис допустимых правил в S4. Наиболее общие результаты относительно допустимости правил вывода в модальных логиках были получены Э. Ержабеком в 2005 г. Опираясь на результаты С. Гилярди в теории унификации для модальной логики, он построил явный бесконечный базис допустимых правил для логик, расширяющих K4 (в частности, Э. Ержабек предложил более простой базис допустимых правил в логике S4, чем у В.В. Рыбакова). Ключевая идея его доказательства состояла в переходе к обобщённым допустимым правилам вывода (с несколькими формулами в заключении), от которых потом можно перейти к обычным.
В своём докладе я расскажу про модальные логики K, K4, S4, GL, разберу примеры допустимых правил в них, определю обобщенные допустимые правила и их AR-системы, предложенные Э. Ержабеком, изложу результаты теории унификации для модальных логик, полученные С. Гилярди, и расскажу идею доказательства Э. Ержабека построения явного базиса допустимых правил в логиках K4, S4, GL.
Jeřábek E. Admissible rules of modal logics //Journal of Logic and Computation. – 2005. – Т. 15. – №. 4. – С. 411-431.
Докладчик: Никита Лукашов
Название: Допустимые правила вывода в IPC
YouTube
Дата: 16.02.2024
СЛАЙДЫ
Аннотация:
Правило вывода в логике L называется допустимым, если множество теорем логики L не изменяется при добавлении к ней этого правила. Хорошо известно, что в интуиционистской логике высказываний IPC, в отличие от классической, существуют допустимые, но не выводимые правила вывода. В 1975 году Х. Фридман сформулировал проблему, является ли множество допустимых правил вывода IPC разрешимым или нет.
В 1984 В.В. Рыбаков дал на этот вопрос положительный ответ, и более того доказал, что для допустимых правил IPC не существует конечного базиса. Однако, это не исключало существования бесконечного базиса. Немного лет спустя, де Йонг и А. Виссер нашли красивое бесконечное множество правил, допустимых в IPC, и выдвинули гипотезу, что оно образуют базис. Независимо друг от друга, П. Розье (1991 г.) и Р. Имхофф (1999 г., опираясь на недавние результаты С. Гилярди в области теории унификации для IPC), доказали эту гипотезу, и таким образом был получен счётный базис допустимых правил вывода в интуиционистской логике высказываний.
В своём докладе я расскажу об интуиционистской логике высказываний, о разных интересных свойствах, касающихся допустимости правил вывода, сформулирую понятие их базиса, изложу результаты теории унификации для IPC, полученные С. Гилярди, и дам набросок доказательства Р. Имхофф.
Докладчик: Абдуламин Исмаилов
Название: Роль аксиомы выбора в игре о шляпах
YouTube
Дата: 09.02.2024
Аннотация:
Вечный вопрос о поиске идеальных оснований математики приводит нас к теориям типов -- аналогам теорий множеств (именно так -- теории), но с другими базовыми объектами. В докладе мы будем разбирать, каким образом такие теории строятся, а также на каких соображениях основаны те или иные аксиомы/правила, которые на первый взгляд могут показаться странными. В моём понимании, здесь, как и с теориями множеств, эти вопросы являются главными.
Докладчик: Надежда Хорошавкина
Название: Роль аксиомы выбора в игре о шляпах
YouTube
Дата: 26.01.2024
Аннотация:
Классическая задача о шляпах звучит так: N игроков стоят в ряд, на каждого надета шляпа одного из двух цветов. Каждый игрок видит цвета шляп всех следующих за ним игроков, но не видит ни своего цвета шляпы, ни цветов шляп предыдущих игроков. По очереди, начиная с первого, каждый игрок должен назвать цвет своей шляпы. Какое минимальное количество ошибок могут обеспечить игроки, если им разрешено заранее договориться о стратегии? Задачу можно обобщить на счётное число игроков. Оказывается, что в этом случае ответ не меняется, и существование выигрышной стратегии может быть показано с помощью разных версий аксиомы выбора. Об этом, а также о том, можно ли обойтись без аксиомы выбора и что нам придётся потребовать взамен — будет рассказано в докладе.
Доклад основан на статьях "Choice and the Hat Game", S. Geschke, R. Lubarsky, M. Rahn и "Ultrafilters, Transversals, and the Hat Game", L. Serafin, 2023. Для понимания доклада можно почитать про разные версии аксиомы выбора, а также про ультрафильтры на натуральных числах. Однако все необходимые определения будут даны.
Докладчик: Александр Запрягаев
Название: Категорный подход к интерпретациям теорий
YouTube
Дата: 19.01.2024
Аннотация:
Метод интерпретаций является мощным инструментом для исследования теорий первого порядка и сопоставления их сравнительной силы. Мы познакомимся с главными методами, приложениями и примерами интерпретаций и изучим различные категории, который можно ввести на классе всех теорий с интерпретациями в качестве морфизмов. Мы установим их основные свойства и укажем теории и интерпретации, соответствующие классическим теоретико-категорным понятиям в них.
Доклад основан на статье А. Виссера "Categories of Theories and Interpretations." In Logic in Tehran, edited by Ali Enayat, Iraj Kalantari, and Mojtaba Moniri, 284-341. Lecture Notes in Logic.
Cambridge: Cambridge University Press, 2006.
2023 год
Докладчик: Андрей Минаев
Название: Релевантные логики
YouTube
Дата: 08.12.2023
Аннотация:
Релевантные логики - это неклассические логики, в которых посылка и вывод должны быть значимо взаимосвязаны. Актуальность исследований релевантных логик заключается в их способности разрешать парадоксы импликации. Более того, такие логики являются паранепротиворечивыми, то есть устойчивыми к принципу, что из противоречия может быть доказано любое утверждение. В докладе будет проведен обзор некоторых наиболее значимых релевантных логик и семантики Рутли-Мейера.
Докладчик: Александр Грефенштейн
Название: Интерполяция в классической логике первого порядка
YouTube
Дата: 24.11.2023
Аннотация:
Интерполяционные свойства относятся к числу фундаментальных свойств логических систем. Изучению вопросов о наличии или отсутствии интерполяционных свойств у различных систем посвящена обширная литература. В частности, для ряда известных систем были развиты абстрактные алгебраические методы, позволяющие решать такого рода вопросы для целых решёток расширений. Однако, как это часто бывает, ситуация оказывается намного сложнее в кванторном случае, где изучение даже одной конкретной системы нередко представляет собой сложную задачу.
На докладе будет разобрано решение вопроса об интерполяции для классической логики первого порядка, QCL. А именно, мы установим, что QCL обладает аналогом интерполяционного свойства Крейга, а также получим некоторые другие метаматематические свойства QCL в качестве следствий.
Докладчик: Раджаб Агамов
Название: Линейные динамические системы с непрерывными весовыми функциями
YouTube
Дата: 17.11.2023
Аннотация:
In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This presentation addresses the problems to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions and polynomial weight functions as a special case. Besides general LDSs, the special cases of stochastic LDSs and of LDSs with bounded orbits are considered. Furthermore, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.
Докладчик: Владислав Слюсарев
Название: Модальные логики случайных шкал в определимых классах. Часть 2
YouTube
Дата: 10.11.2023
Аннотация:
Мы рассматриваем последовательность шкал Крипке конечного размера n со случайным отношением. Формула называется истинной асимптотически почти наверное (а.п.н.), если вероятность её общезначимости в случайной шкале размера n стремится к 1 при n -> ∞. В. Горанко исследовал случайные шкалы Крипке с равномерным распределением среди всех n^2 отношений в статье [1]. Множество всех а.п.н. истинных формул образует нормальную модальную логику. Горанко представил некоторые аксиомы этой логики, однако неизвестно, существует ли её разрешимая аксиоматизация.
Модель Горанко можно обобщить, рассматривая равномерное распределение на множестве всех шкал размера n, в которых общезначима заданная логика L. Множество а.п.н.
истинных формул в этой модели случайной шкалы является нормальным расширением L. Для некоторых логик комбинаторные методы позволяют получить полную аксиоматизацию.
Доклад состоит из двух частей. В первой части мы ввели основные определения и рассмотрели примеры логик T, KB, TB. Вторая часть доклада посвящена комбинаторным методам, которые позволяют свести общую задачу к логикам свзных шкал и конусов. Мы используем эти методы для исследования структуры случайных шкал логик SL, GL.3, Grz.3 и расширений K5 и построим полные аксиоматизации логик а.п.н. истинных формул в перечисленных классах.
[1] Goranko, Valentin. “The Modal Logic of Almost Sure Frame Validities in the Finite.” Advances in Modal Logic (2020).
Докладчик: Владислав Слюсарев
Название: Модальные логики случайных шкал в определимых классах. Часть 1
YouTube
Дата: 03.11.2023
Аннотация:
Мы рассматриваем последовательность шкал Крипке конечного размера n со случайным отношением. Формула называется истинной асимптотически почти наверное (а.п.н.), если вероятность её общезначимости в случайной шкале размера n стремится к 1 при n -> ∞. В. Горанко исследовал случайные шкалы Крипке с
равномерным распределением среди всех n^2 отношений в статье [1]. Множество всех а.п.н. истинных формул образует нормальную модальную логику. Горанко представил некоторые аксиомы этой логики, однако неизвестно, существует ли её разрешимая аксиоматизация.
Модель Горанко можно обобщить, рассматривая равномерное распределение на множестве всех шкал размера n, в которых общезначима заданная логика L. Множество а.п.н. истинных формул в этой модели случайной шкалы является нормальным расширением L. Для некоторых логик комбинаторные методы позволяют получить полную аксиоматизацию.
Доклад состоит из двух частей. В первой части мы введём определения случайных шкал Крипке и а.п.н. истинных формул в модально определимом классе и рассмотрим логики случайных шкал в классах шкал логик T, KB, TB. Вторая часть доклада будет посвящена комбинаторным методам, которые позволяют получать полные аксиоматизации для логик случайных шкал в некоторых классах, таких как шкалы логики K5 и её расширений.
[1] Goranko, Valentin. “The Modal Logic of Almost Sure Frame Validities in the Finite.” Advances in Modal Logic (2020).
Докладчик: Анастасия Оноприенко
Название: Иерархия семантик интуиционистской логики
YouTube
Дата: 20.10.2023
Аннотация:
Взгляды Брауэра на основания математики привели к изучению интуиционистской логики и её расширений. Со временем это превратилось в самостоятельную отрасль логики, связанную с теорией решёток, топологией, модальной логикой и другими областями. В докладе я расскажу про различные типы семантик интуиционистской логики. Основной идеей является иерархия семантик, организованная по принципу возрастающей общности. Наименее общая - семантика Крипке, далее семантика Бета, топологическая семантика, семантика Драгалина и, наконец, самая общая - алгебраическая семантика.
Докладчик: Кудинов Андрей
Название: Топологическая семантика модальной логики
YouTube
Дата: 06.10.2023
Аннотация:
Основной семантикой для модальной логики сейчас является семантика Крипке. Но исторически раньше семантики Крипке появилась топологическая семантика, интерпретирующая модальный оператор, как оператор взятия внутренности. Маккинси и Тарский в своей работе 1944 года доказали полноту логики S4 относительно топологических пространств, и, более того, относильно любого метрического, плотного в себе, сепарабельного пространства. Я дам определение топологической семантики, докажу теорему о полноте. Теорема Маккинси и Тарского технически довольно сложная, поэтому мы не будем ее доказывать полностью, а обсудим только идею. Вместо этого мы подробно докажем частный случай теоремы: полноту относительно рациональных чисел. В конце мы обсудим в каком направлении развивалось исследование топологичеких модальных логик после работы Маккинси и Тарского.
Докладчик: Кокин Владислав
Название: Введение в субструктурные логики
YouTube
Дата: 29.09.2023
Аннотация:
Субструктурные логики — семейство неклассических логик, в которых отсутствуют какие-то из структурных правил ослабления, сокращения или обмена. На семинаре я сформулирую секвенциальные и гильбертовские исчисления для основных субструктурных логик и расскажу про их синтаксические свойства, обращая внимание на отличия от классического исчисления предикатов.
Докладчик: Александр Гагарин
Название: Введение в модальную логику
Дата: 22.09.2023
САЙДЫ
Аннотация:
Модальная логика получается из классической логики высказываний добавлением к логическим связкам операций "необходимо" и "возможно", разная интерпретация которых ведет к разным множествам тавтологий. В докладе будет дано по два определения модальной логики K и примеров ее расширений - через семантику Крипке и в виде исчисления. Введем понятие канонической модели, необходимое для доказательства эквивалентности этих определений, и обсудим границы применимости канонических моделей к доказательству полноты по Крипке различных логик. На примерах разберем метод фильтраций для доказательства разрешимости модальных логик, и обсудим вычислительную сложность.
Докладчик: Серова Дарья
Название: Использование алгебраических моделей программ для обнаружения метаморфного вредоносного кода
YouTube
Дата: 09.06.2023
Аннотация:
В докладе рассмотрятся новая теоретико-автоматная модель, которая может послужить основой для разработки антивирусов. Эту модель создали Р.И. Подловченко, Н. Н. Кузюрин, В. С. Щербина и В. А. Захаровa в своих научных работах и привели методы решений проверки эквивалентности программ. В докладе проведу обзор методов решения проблемы проверки эквивалентности для различных алгебраических моделей программ и оценка устойчивости некоторых обфусцирующих преобразований, которые обычно используются метаморфными вирусами.
Докладчик: Ирина Агаджанян
Название: Алгоритмическая сложность монадических полимодальных предикатных логик с равенством на конечных шкалах Крипке
YouTube
Дата: 02.06.2023
Аннотация:
Для монадических модальных логик зачастую достаточно одной монадической предикатной буквы и нескольких переменных, чтобы уже иметь возможность доказать неразрешимость. В то же время монадический фрагмент с равенством классической логики предикатов является разрешимым. Отсюда возникает вопрос: при достижении каких условий можно говорить про разрешимость? В данном докладе будут рассмотрены монадические предикатные логики с равенством над конечными шкалами Крипке, в работе с которыми не работает обычный способ доказательства неразрешимости, будут доказаны их разрешимости и получены оценки сложности для некоторых из них. Доклад является расширением моего доклада от 9.12.2022 на случай логик с равенством.
Докладчик: Александр Грефенштейн
Название: О \Pi^1_1-трудности вероятностной логики Кейслера–Хувера
YouTube
Дата: 28.04.2023
Аннотация:
В 1977 году Джером Кейслер в ходе работы над гиперконечной теорией моделей, основная цель которой состояла в изучении и классификации моделей из прикладных разделов математики, определил инфинитарную вероятностную логику, похожую на широко известную логику L_{\omega_1, \omega}. В языке этой логической системы также присутствуют счётные конъюнкции и дизъюнкции, однако вместо обычных кванторов по элементам носителя вводятся вероятностные кванторы вида (Px >= r), где r — вещественное число. При этом запись (Px >= r) \Phi читается следующим образом: «вероятность того, что x удовлетворяет условию \Phi, больше или равна r». Более того, им было показано, что значительная часть теории вероятностей может быть промоделирована внутри этой системы и её естественных обогащений.
На докладе мы посмотрим на данную систему с алгоритмической точки зрения. Следуя статье Дугласа Хувера «Probability logic» (1978), мы покажем, что проблема общезначимости для относительно слабого, но весьма естественного финитарного фрагмента такой системы является \Pi^1_1-трудной, т.е. к ней сводится проблема истинности для \Pi^1_1-предложений в стандартной модели арифметики. Здесь основная сложность проистекает из возможности строить цепочки вложенных друг в друга вероятностей, а не из инфинитарности языка или использования вещественных чисел внутри вероятностных кванторов. Аналогичная верхняя оценка была ранее установлена Кейслером; поэтому «\Pi^1_1-трудной» можно заменить на «\Pi^1_1-полной».
Докладчик: Елена Попова
Название: Подходы к решению проблемы логического всеведения в эпистемической логике
YouTube
Дата: 21.04.2023
Аннотация:
Проблема логического всеведения заключается в замкнутости знания относительно логического следования, поэтому связана с чрезмерной идеализацией познавательных способностей агентов - знание аксиом автоматически гарантирует знание всех следствий. В докладе будут представлены возможные пути решения проблемы логического всеведения в эпистемической логике, в частности, мы рассмотрим логики с оператором осведомленности (Fagin R., Halpern J., 1988; van Benthem J., Velazquez-Quesada F., 2010) и их возможные модификации с темпоральным расширением эпистемической логики.
Докладчик: Никита Лукашов
Название: Проблема унификации в бимодальной логике доказуемости GLB
YouTube
Дата: 14.04.2023
СЛАЙДЫ
Аннотация:
Бимодальная логика доказуемости GLB возникла, как расширение логики доказуемости Гёделя-Лёба GL с модальностью $\square$ (она же $[0]$), интерпретируемой как доказуемость в арифметике Пеано, добавлением новой модальности $[1]$, которая понимается как $\omega$-доказуемость в PA.
Про логику GLB было установлено много интересных свойств, таких как интерполяция Крейга, теорема о неподвиной точке, теорема о нормальной форме, и т.д. Однако вопрос об унификационном типе GLB до последнего времени оставался открытым. Аналогичные результаты были получены С. Гилярди для логики GL в статье [Ghilardi, 2000]. Он показал, что в GL существование проективного унификатора для формулы эквивалентно наличию для класса её моделей некоторого свойства расширения.
В своём докладе я расскажу о проблеме унификации в GLB и о своих продвижениях в ней. Я обобщу результаты Гильярди и докажу аналогичную теорему для логики J (подсистемы GLB). Все необходимые определения будут даны по ходу доклада.
[Ghilardi, 2000] Ghilardi, S. (2000). Best solving modal equations. Annals of Pure and Applied Logic, 102(3):183–198.
Докладчик: Иван Пыльцын
Название: Игровая семантика Межирова для интуиционистской логики (продолжение)
YouTube
Дата: 07.04.2023
СЛАЙДЫ
Аннотация:
Этот доклад будет продолжением доклада от 24 марта. В этом докладе мы продолжим рассматривать игровую семантику для интуиционистской логики, но уже рассмотрим предикатный случай, какие проблемы возникают при попытке непосредственного обобщения со случая высказываний, а также затронем проблему сильной полноты.
Докладчик: Иван Пыльцын
Название: Игровая семантика Межирова для интуиционистской логики
YouTube
Дата: 24.03.2023
СЛАЙДЫ
Аннотация:
В этом докладе мы рассмотрим игровую семантику для интуиционистской логики, рассмотрим примеры и докажем соответствующие теоремы о полноте и корректности. Если останется время, то посмотрим, как обстоит дело с интуиционистской логикой предикатов.
Докладчики: Дмитрий Шкатов и Михаил Рыбаков
Название: Алгоритмическая сложность неклассических логик унарного предиката
Дата: 17.03.2023
СЛАЙДЫ
Аннотация:
В докладе будут изложены результаты о рекурсивной неперечислимости модальных и суперинтуиционистских предикатных логик классов шкал Крипке с конечным числом возможных миров в языках с одной унарной предикатной буквой и тремя индивидными переменными.
Докладчик: Николай Поляков
Название: О канонической рамсеевской теореме Эрдёша и Радо и рамсеевских ультрафильтрах
Youtube
Дата: 03.03.2023
СЛАЙДЫ
Аннотация:
В докладе представлен комбинаторный результат, имеющий отношение к канонической рамсеевской теореме Эрдёша и Радо. Доказано, что для каждого разбиения $P$ множества $[\omega]^n$ существует такое конечное разбиение $Q$ множества $[\omega]^{2n}$, что каждое однородное для разбиения $Q$ множество $X\subseteq \omega$ есть конечное объединение множеств канонических для разбиения $P$. Результат использован для получения характеризации рамсеевских ультрафильтров в терминах функций произвольной конечной арности и их ультрарасширений. Подробнее см. https://doi.org/10.48550/arXiv
Докладчик: Надежда Хорошавкина
Название: Неперечислимая гипотеза Хадвигера и характеризация деревьев с помощью графов
Youtube
Дата: 17.02.2023
Аннотация:
Гипотеза Хадвигера утверждает, что в графе с хроматическим числом χ найдется в качестве минора полный подграф на χ вершинах. В гипотезе участвуют только конечные графы без петель. В докладе мы рассмотрим обобщение этой гипотезы на графы с бесконечным множеством вершин: в качестве множества вершин будут выступать бесконечные кардиналы. Мы покажем на примерах, что во многих случаях расширенная гипотеза Хадвигера не верна. Также, мы расскажем о том, как известные результаты о гипотезе Хадвигера помогают классифицировать неособенные деревья. Доклад основан на статье Dávid Uhrik, arxiv:2212.02169.
Докладчик: Екатерина Малюгина
Название: Топобулевы алгебры
Youtube
Дата: 10.02.2023
Аннотация:
Топобулевой алгеброй называется булева алгебра с оператором замыкания, для которого верны аксиомы Куратовского. Точное определение будет дано в докладе. Также будет рассказано о пополнениях Маккинси-Тарского и Йонссона-Тарского и рассмотрена связь топобулевых алгебр с модальной логикой S4. Кроме того, будут доказаны некоторые свойства категории топобулевых алгебр и полугомоморфизмов.
Докладчик: Владислав Слюсарев
Название: Модальные логики хорновых замыканий случайной шкалы Крипке
Youtube
Дата: 03.02.2023
СЛАЙДЫ
Аннотация:
Мы рассматриваем последовательность шкал Крипке конечного размера n со случайным отношением. Формула называется истинной асимптотически почти наверное (а.п.н.), если вероятность её общезначимости в случайной шкале размера n стремится к 1 при n -> ∞. В. Горанко исследовал случайные шкалы Крипке с равномерным распределением среди всех n^2 отношений в статье [1]. Множество всех а.п.н. истинных формул образует нормальную модальную логику. Горанко представил некоторые аксиомы этой логики, однако неизвестно, существует ли её разрешимая аксиоматизация. Мы рассматриваем замыкания случайной шкалы Крипке относительно хорновых классов шкал, таких как многообразия логик K4, K5, S4, S5 и др. Эта модель позволяет исследовать "вероятностные" варианты этих логик. Мы доказываем в общем случае, что а.п.н. истинные формулы в этой модели образуют нормальное расширение исходной логики. Мы также показываем, что для логик, содержащих K4 или K5, это расширение совпадает с S5.
[1] Goranko, Valentin. “The Modal Logic of Almost Sure Frame
Validities in the Finite.” Advances in Modal Logic (2020).
Докладчик: Глеб Красилич
Название: Зависимые типы и автоматическая проверка доказательств
Youtube
Дата: 27.01.2023
Аннотация:
Данный доклад (а точнее серия из двух докладов) продолжает тему доклада Лямбда-исчисление и Соответствие Карри-Говарда от 23.09.2022. В прошлый раз мы обсудили, как типизированное лямбда-исчисления связано с логикой. Сейчас же мы рассмотрим Гомотопическую теорию типов (а точнее ее "негомотопический" фрагмент, похожий на классическую теорию типов Мартин-Лёфа): очень выразительное типизированное исчисление, пригодное для формализации содержательной математики. Будут даны
основные определения, мотивировки, показано как мы можем формализовать математические рассуждения пользуясь парадигмой "типы как утверждения", и, пожалуй самое главное, мы будем "программировать" математические доказательства на языке Agda, используя его в качестве системы автоматической проверки доказательств.
Докладчик: Глеб Красилич
Название: Зависимые типы и автоматическая проверка доказательств
Youtube
Дата: 20.01.2023
Аннотация:
Данный доклад (а точнее серия из двух докладов) продолжает тему доклада Лямбда-исчисление и Соответствие Карри-Говарда от 23.09.2022. В прошлый раз мы обсудили, как типизированное лямбда-исчисления связано с логикой. Сейчас же мы рассмотрим Гомотопическую теорию типов (а точнее ее "негомотопический" фрагмент, похожий на классическую теорию типов Мартин-Лёфа): очень выразительное типизированное исчисление, пригодное для формализации содержательной математики. Будут даны
основные определения, мотивировки, показано как мы можем формализовать математические рассуждения пользуясь парадигмой "типы как утверждения", и, пожалуй самое главное, мы будем "программировать" математические доказательства на языке Agda, используя его в качестве системы автоматической проверки доказательств.
АРХИВ СЕМИНАРОВ ПРОШЛЫХ ЛЕТ
Нашли опечатку?
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!
Сервис предназначен только для отправки сообщений об орфографических и пунктуационных ошибках.