Все семинары можно посмотреть на нашем Youtube канале.

 

Докладчик: Виталий Гулевский

Название: Двойственность в интуиционистской логике высказываний

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/~snburris/htdocs/UALG/univ-algebra2012.pdf

 

Докладчик: Владимир Шейн

Название: Внутренняя логика топосов и её приложения в алгебраической геометрии

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.03685) (Приложения в алгебраической геометрии)

 

Докладчик: Александр Колпащиков

Название: Неразрешимые суперинтуиционистские исчисления и закон исключённого третьего

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.2203.10293

 

Докладчик: Надежда Хорошавкина

Название: Неперечислимая гипотеза Хадвигера и характеризация деревьев с помощью графов

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, используя его в качестве системы автоматической проверки доказательств.

 

АРХИВ СЕМИНАРОВ ПРОШЛЫХ ЛЕТ