Кафедра математической логики и теории алгоритмов

Логические проблемы информатики
& Модальная и алгебраическая логика

Объединенный семинар
«Логические проблемы информатики»
(руководители: проф. С.Н.Артёмов, акад. РАН Л.Д.Беклемишев,
доц. В.Н.Крупский, проф. М.Р.Пентус, доц. Т.Л.Яворская)
и  «Модальная и алгебраическая логика»
(руководители: проф. М.Р.Пентус,
проф. В.Б.Шехтман, к.ф.-м.н. И.Б.Шапировский)
Видеозаписи докладов на YouTube
Семинар проходит по четвергам 18:30–20:05.
Временно заседания проходят через Zoom.
Для получения ссылки (включения в рассылку) напишите
<!--ученому секретарю кафедры / семинара Е. Золину--> секретарю семинара А. Запрягаеву по электронной почте aleksandr.zapryagaev@yandex.ru.
<!-- ПОДСКАЗКА: Математические символы окружать sin x -->
    <!-- ШАБЛОН:
  1. 2021.03.XX:
    Докладчик:
    Аннотация.
  2. -->
    весна 2024
  3. 2024.02.15: Сравнение исчислений для бесконечнозначной логики Лукасевича первого порядка и рациональной логики Павелки первого порядка
    Докладчик: А.С.Герасимов (Санкт-Петербург, СПбПУ)
    Аннотация. Бесконечнозначная логика Лукасевича первого порядка и её расширение истинностными константами - рациональная логика Павелки первого порядка - являются многозначными (точнее, нечёткими) логиками, которые формализуют приближённые рассуждения. Множества всех общезначимых формул этих двух логик неперечислимы. Для данных логик известны гильбертовские и аналитические генценовские исчисления, в том числе бесповторное гиперсеквенциальное исчисление, ориентированное на поиск вывода. В докладе будет рассказано о том, как с точки зрения выводимости сравнить несколько таких исчислений друг с другом. <p Доклад основан на статье:

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

  4. осень 2023
  5. 2023.10.24: Формальные грамматики с линейным ограничением на длину вывода
    Докладчик: Тихон Пшеницын (МИАН)
    Аннотация. Порождающие грамматики Хомского задаются следующим образом: фиксируются стартовая строка S и конечное множество P правил вида α→β, где α и β — строки. Язык, задаваемый такой грамматикой, состоит из строк, которые можно получить из S в результате последовательности применений правил из P (применение правила α→β заключается в замене подстроки α на β). Известно, что задача принадлежности строки языку, задаваемому такой грамматикой, алгоритмически неразрешима, что делает такие грамматики неинтересными с практической точки зрения. Один из способов добиться разрешимости — ограничить вид используемых правил. Скажем, если потребовать, что все правила в порождающей грамматике Хомского имеют вид A→β, где A — один нетерминальный символ, то получится класс контекстно-свободных грамматик, для которых известны полиномиальные алгоритмы. Другой, значительно менее популярный, способ — ограничить длину выводов в грамматике. А именно, будем говорить, что строка w задаётся f-ограниченной грамматикой, если существует цепочка преобразований вида S ⇒ w1 ⇒ … ⇒ wk = w, где k<f(|w|), для некоторой вычислимой функции f(x); тогда проверка выводимости становится разрешимой.

    Доклад посвящён частному случаю такого ограничения, когда f(x)=Cx — линейная функция. Оно интересно, с одной стороны, тем, что является минимальным возможным, при котором грамматики могут порождать бесконечные языки; с другой стороны, формальные грамматики с линейным ограничением на длины выводов оказываются тесно связанными с категориальными грамматиками, основанными на субструктурных логиках с операциями мультипликативного типа. Результаты, которые будут обсуждаться в докладе, получены для модификаций порождающих грамматик Хомского с линейным ограничением. В частности, будет доказано, что системы сложения векторов с ветвящимися правилами (BVASS) и с линейным ограничением на размеры выводов эквивалентны грамматикам над коммутативным исчислением Ламбека. Также будет рассказано о линейно ограниченных графовых грамматиках и их связи с гиперграфовыми категориальными грамматиками Ламбека.

  6. 2023.10.03: О логиках доказуемости арифметики Нибергалля
    Докладчик: Лев Дворкин (МГУ)
    Аннотация. К.-Г. Нибергалль привел известный пример неперечислимой непротиворечивой теории, расширяющей арифметику Пеано PA, в которой доказуема естественная формализация утверждения о собственной непротиворечивости. В докладе будут рассмотрены логики доказуемости этой теории относительно PA, истинностной арифметики и самой арифметики Нибергалля. Для каждой из данных логик представлена полная семантика Крипке и описан её замкнутый фрагмент. Вопрос об их конечной аксиоматизируемости остаётся открытым. Мы рассмотрим попытки получить явное синтаксическое описание данных логик и возникающие на этом пути трудности.
  7. весна 2023
  8. 2023.03.30: Алгоритмическая сложность неклассических логик унарного предиката / Computational complexity of non-classical logics of an unary predicate
    Докладчик: Михаил Рыбаков (Mikhail Rybakov, ИППИ РАН) и Дмитрий Шкатов (Dmitry Shkatov, Университет Йоганнесбурга)
    Аннотация. Планируется обсудить алгоритмическую сложность неклассических предикатных логик при ограничениях на средства языка. В 1962г. С.Крипке предложил простой способ, позволяющий моделировать в модальном языке бинарную предикатную букву с помощью двух унарных. Будет показано, как можно моделировать бинарную букву с помощью одной унарной в модальном языке и с помощью двух унарных в интуиционистском языке. Это сразу даёт неразрешимость многих логик в языке с одной-двумя унарными буквами и тремя переменными, поскольку классическая логика бинарного предиката неразрешима при трёх переменных в языке. Кроме того, будет показано, как можно промоделировать все унарные буквы с помощью одной унарной (как в модальном, так и в интуиционистском языке). С учётом известных результатов о неразрешимости многих неклассических логик в языке с двумя переменными (Д.Габбай, В.Шехтман (1993), Р.Кончаков, А.Куруш, М.Захарьящев (2005)), это даёт возможность доказать неразрешимость многих модальных и суперинтуиционистских предикатных логик в языке с одной унарной предикатной буквой и двумя переменными. Предлагаемое моделирование позволяет получить неперечислимость и даже неарифметичность соответствующих фрагментов некоторых логик, определяемых семантически. Мы подробно разберём доказательство неперечислимости модальных предикатных логик естественных классов конечных (по числу миров) шкал Крипке и доказательство неперечислимости позитивного фрагмента интуиционистской предикатной логики конечных шкал Крипке, когда языки этих логик содержат одну унарную предикатную букву и три предметные переменные.

    We consider the issues concernign algorithmic complexity of non-classical predicate logics in restricted languages. In 1962, S.Kripke suggested how to simulate a binary predicate letter of a classical first-order formula with a modal first-order formula containing two unary letters. Building on Kripke's idea, we simulate a binary precidate letter with a single unary letter in modal formulas and with two unary letters in superintuitionistic formulas. This immediately gives us the undecidability of numerous modal logics in languages with one unary letter, and superintuitionistic logics with two unary letters, and three variables, since the classical logic of a binary predicate is undecidable with three variables. In addition, we show how to simulate any number of unary letters with a single unary letter (both in modal and intuitionistic languages). Due to the well-known results on the undecidability of many non-classical logics in languages with two variables (D.Gabbay, V.Shehtman (1993), R.Konchakov, A.Kurucz, M.Zakharyaschev (2005)), we obtain the undecidability of many modal and superintuitionistic predicate logics in languages with a single unary predicate letter and two variables. The proposed encoding enables us to obtain the non-enumerability and even non-arithmeticity of the corresponding fragments of a number of logics of Kripke frames. We shall prove in detail that the following logics are not recursively enumerable in languages with a single unary predicate letter and three individual variables: modal predicate logics of natural classes of finite (in terms of the number of worlds) Kripke frames and the positive fragment of intuitionistic predicate logic of finite Kripke frames.

  9. 2023.03.16: Локально конечные полимодальные логики и критерий Сегерберга-Максимовой
    Докладчик: И.Б. Шапировский (ИППИ РАН и Университет Нью-Мексико)
    Аннотация. Логика L локально конечна (в другой терминологии - локально таблична), если каждый её фрагмент с конечным числом переменных содержит лишь конечное число неэквивалентных формул. В алгебраических терминах, это значит что локально конечно многообразие алгебр логики L. Для одномодальных транзитивных логик критерий локальной конечности был получен в 1970х годах К. Сегербергом [2] и Л.Л. Максимовой [1]: в этом случае локальная конечность L равносильна тому, что L содержит формулу B_n конечной глубины. Это замечательная теорема в нескольких отношениях. Помимо того, что она даёт естественный семантический критерий через свойства бинарных отношений, она также даёт синтаксическое описание: локальная конечность выражается формулой из некоторого явно описанного множества формул {B_n: n<ω}. В работе [4] критерий Сегерберга-Максимовой был обобщен на некоторые семейства нетранзитивных одномодальных логик. Я расскажу об обобщениях этого критерия на полимодальный случай. Часть результатов основана на недавней работе [3].

    [1] L. Maksimova, Modal logics of finite slices, Algebra and Logic, vol. 14 (1975), no. 3, pp. 304–319.

    [2] K. Segerberg, An essay in classical modal logic, Filosofska Studier, vol.13, Uppsala Universitet, 1971.

    [3] I. Shapirovsky, Sufficient conditions for local tabularity of a polymodal logic, Preprint, 2022. arxiv.2212.07213

    [4] I. Shapirovsky and V. Shehtman, Local tabularity without transitivity, Advances in Modal Logic, volume 8, College Publications, 2016, pp. 520–534.

  10. 2023.02.16: Kuznetsov's Theorem Done Algebraically: δ-Extensions of Heyting Algebras
    Докладчик: Alexei Muravitsky (Northwestern State University, USA)
    Аннотация. The talk is devoted to an algebraic interpretation of Kuznetsov's theorem which establishes the assertoric equipollence of intuitionistic calculus and calculus KM. Given a Heyting algebra, we define an enrichable Heyting algebra, into which the former algebra is embedded. Moreover, we show that both algebras generate one and the same variety of Heyting algebras. This algebraic result is equivalent to the Kuznetsov theorem. The proposed construction of the enrichable ``counterpart'' of a given Heyting algebra allows one to observe that some properties of the original algebra are preserved by this embedding in the counterpart algebra. The embedding technique, being called in the talk a "δ-embedding", can be used for proving other properties of KM, namely separation property, interpolation property and fixed-point property. In addition, the role of KM in the lattices of normal extensions of some other calculi will be discussed.
  11. весна 2022
  12. 2022.05.19: О финитной аппроксимируемости модальных логик декартовых степеней линейных порядков
    Докладчик: И.Б. Шапировский (ИППИ РАН; New Mexico University)
    Аннотация. Финитная аппроксимируемость логики означает её полноту относительно некоторого класса конечных структур. С 1960-х годов известно, что модальные логики стандартных числовых линейных порядков финитно аппроксимируемы. Куда более нетривиальными оказываются результаты о финитной аппроксимируемости модальных логик их декартовых степеней. Для действительных чисел с нестрогим порядком финитная аппроксимируемость была установлена независимо Голдблаттом (1980) и Шехтманом (1983), со строгим порядком -- Шехтманом и Шапировским (2003). Финитная аппроксимируемость логик конечных степеней натуральных чисел с отношениями и ≥ немедленно следует из того, что в таких структурах всякий порожденный точкой конус конечен. С использованием техники селективных фильтраций, этот результат обобщается на случай конечных произведений любых ординалов, рассматриваемых с обратным порядком; кроме того, логика всех таких произведений, взятых без наибольшего элемента, совпадает с модальной логикой Медведева (Савельев и Шапировский, 2022).

    Goldblatt, R. (1980): Diodorean modality in Minkowski spacetime. Stud. Logica 39(2/3), 219–236.

    Shehtman, V. (1983) Modal logics of domains on the real plane. Stud. Logica 42, 63–80.

    Shapirovsky, I. and Shehtman, V. (2003) Chronological future modality in Minkowski spacetime. In Advances in Modal Logic, v.4, 437–459, College Publications.

    Shapirovsky, I. (2019) Modal logics of finite direct powers of ω have the finite model property. In WoLLIC 2019, pp. 610–618.

    Saveliev, D. and Shapirovsky, I. (2022) Medvedev's logic and products of converse well orders. Accepted to Advances in Modal Logic-2022.

  13. 2022.05.12: Свойства лесных модальных логик
    Докладчик: Алексей Алексеев
    Аннотация. Ознакомившись с результатами Я. М. Другуша, изложенными в статье "Финитная аппроксимируемость лесных суперинтуиционистских логик" (1984) , мы рассматриваем аналогичное утверждение в модальной логике. В докладе опровергается аналогичное утверждение и приводится два контрпримера: для расширений минимальной модальной логики K и расширений логики Гёделя-Лёба GL.
  14. 2022.05.12: Модальная глубина и бисимуляционные игры на примере расширений логики Гжегорчика
    Докладчик: Илья Мароченков
    Аннотация. При исследовании модальной глубины логики можно применять такой инструмент, как бисимуляционные игры. В докладе будет описана связь бисимуляционных игр и модальной глубины. В частности, будет доказана точность верхней оценки (полученной В.Б. Шехтманом) модальной глубины логики Grz+bd_n (логики Гжегорчика с дополнительной аксиомой).
  15. 2022.04.14: Топологическое произведение S4.1xS4
    Докладчик: А.В. Кудинов (ИППИ РАН)
    Аннотация. Под произведением модальных логик L1 и L2 обычно понимается логика произведений L1-шкал и L2-шкал Крипке. В частности, такое произведение S4 на S4 равно коммутатору, т.е. соединению логик S4*S4 плюс аксиома коммутативности и аксиома Черча-Россера. Если вместо шкал Крипке рассматривать окрестностные шкалы, то в результате произведений мы будем получать другие логики. Окрестностные шкалы являются обобщением шкал Крипке, и получатся более слабые логики. Для расширений логики S4 окрестностная семантика эквивалентна топологической. В работе [1] доказано, что логика произведений топологических пространств равно соединению S4*S4 без дополнительных аксиом. Топологическое произведение S4 на S5 равно полукоммутатору, т.е. S4*S5 плюс коммутативность в одну сторону и аксиома Черча-Россера, а для S5 на S5 совпадает с коммутатором. После этого, в работе [2] было доказано, что логика произведения RxR (R - пространства действительных чисел) отлична от S4*S4, но точная ee аксиоматизация остается неизвестной. Аксиома A1 = \Box\Diamond p \to \Diamond \Box p называется аксиомой Маккинси. Логика S4.1 = S4 + A1 хорошо известна и полна относительно слабо разреженных пространств (см. [3]). Мы докажем, что топологическое произведение S4.1 на S4 равно S4.1*S4 + логик, \Diamond_1\Box_2(\Diamond_1 p \to \Box_1 p). Это первый пример произведения логик, которое отличается от соединения, коммутатора и полукоммутатора и для которого аксиоматика известна.

    [1] Benthem, J. V., Bezhanishvili, G., Cate, B. T., & Sarenac, D. (2006). Multimodal logics of products of topologies. Studia Logica, 84(3), 369-392.

    [2] Kremer, P. (2015). The Incompleteness of S4 \oplus S4 for the Product Space RxR. Studia Logica, 103(1), 219-226.

    [3] Bezhanishvili, G., Esakia, L., & Gabelaia, D. (2005). Some results on modal axiomatization and definability for topological spaces. Studia Logica, 81(3), 325-355.

  16. 2022.04.07: Аксиома транзитивности в окрестностной семантике: полнота и разрешимость
    Докладчик: Кирилл Копнев (Университет Амстердама)
    Аннотация. Окрестностная семантика - один из видов пространственной семантики для модальных логик. В окрестностной шкале каждой точке сопоставляется множество окрестностей, которые эта точка 'видит'. Эта семантика обобщает семантику Крипке, а логика Е всех окрестностных шкал оказывается слабее логики К. С математической точки зрения окрестностная семантика интересна как минимум по двум причинам:

    (1) Она позволяет изучать большее количество логик, нежели семантика Крипке;

    (2) Она является частным случаем топологической семантики.

    В докладе мы дадим определение окрестностной семантики, рассмотрим некоторые важные классы окрестностных шкал, а также рассмотрим вопрос окрестностной полноты и разрешимости некоторых модальных логик с аксиомой транзитивности.

  17. осень 2021
  18. 2021.12.16: Taming the 'elsewhere': On the expressivity of topological languages
    Докладчик: David Fernández Duque (Ghent University, Belgium)
    Аннотация. In topological modal logic, it is well known that the Cantor derivative is more expressive than the topological closure, and the 'elsewhere,' or'difference,' operator is more expressive than the `somewhere' operator. In 2014, Kudinov and Shehtman asked whether the combination of closure and elsewhere becomes strictly more expressive when adding the Cantor derivative. In this paper we give an affirmative answer: in fact, the Cantor derivative alone can define properties of topological spaces not expressible with closure and elsewhere. In this talk we review the state of the art and the morphisms used to establish the new result.
  19. 2021.12.02: Модель безопасности RSS или логика безопасного дорожного движения
    Докладчик: С.П. Кикоть (ИППИ РАН)
    Аннотация. В докладе речь пойдет о попытке построить формальную теорию, которой могли бы руководствоваться водители и автономные автомобили, чтобы избегать столкновений на дорогах. Утверждается, что вождение происходит не столько по официальным ПДД, сколько по неофициальным "народным" правилам, которые можно попытаться формализовать. Другие компоненты теории - понятия ответственности (отсюда название модели RSS - responsibility-sensitive safety), приоритета, опасной ситуации и правильной реакции. В докладе также будет рассмотрена задача проезда через нерегулируемые перекрестки и определения очередности проезда в трудных ситуациях.
  20. 2021.10.28: Система доказательств Аренд
    Докладчик: Валерий Исаев (JetBrains, Санкт-Петербург)
    Аннотация. Аренд -- это система доказательств, основанная на вариации гомотопической теории типов, разрабатываемая в JetBrains Research. Мы обсудим различные особенности языка, включая его гибкую систему классов, поддержку высших индуктивных типов, включая фактор-множества, и возможности по автоматизации доказательств.

    Основная цель Аренда -- это формализация результатов как в гомотопической теории типов, так и в обычной математике. Для достижения этой цели Аренд предоставляет систему вселенных с подтипизацией, которая позволяет работать на каждом из этих уровней однообразно.

    Система классов с подтипизацией и вывод экземпляров классов позволяет удобным образом формализовывать стандартные структуры, которые встречаются в различных областях математики.

    Система мета-определений позволяет реализовывать расширения языка, в частности, различные EDSL и тактики.

  21. 2021.10.21: Введение в гомотопическую теорию типов
    Докладчик: Валерий Исаев (JetBrains, Санкт-Петербург)
    Аннотация. Гомотопическая теория типов -- это новая область математики, которая объединяет логику, теория гомотопий и теорию языков программирования. В этом докладе я расскажу про все базовые компоненты этой теории, включая необходимые теоретико-типовые конструкции. Я приведу сравнение этой теории с более традиционными теориями множеств и покажу как гомотопические конструкции являются естественным обобщением теоретико-множественных определений. Например, мы обсудим определение надстройки и сфер, которые получаются из обобщения фактор-множеств. Также я продемонстрирую как эти конструкции выражаются формально на языке Аренд.
  22. 2021.10.14: Неперечислимость суперинтуиционистской логики конечных шкал Крипке в языке с тремя предметными переменными и одной унарной предикатной буквой
    Докладчики: Михаил Рыбаков (ИППИ РАН; ВШЭ; ТвГУ), Дмитрий Шкатов (University of the Witwatersrand, Johannesburg)
    Аннотация. Рассматривается суперинтуиционистская предикатная логика, определяемая классом шкал Крипке с конечным числом миров. Доказывается, что эта логика не является рекурсивно перечислимой (является Пи-0-1-трудной) в языке, содержащем три предметные переменные и одну одноместную предикатную букву.

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

    Используемая техника позволяет получить аналогичные результаты для всех предикатных логик, лежащих между логикой конечных шкал и логикой конечных шкал логики слабого закона исключённого третьего. При добавлении условия постоянства предметных областей результат сохраняется. Аналогичные результаты можно получить для модальных логик.

  23. 2021.10.07: Soundness and completeness results for LEA and probability semantics
    Докладчик: Eoin Moore, CUNY Graduate Center, New York
    Abstract. The goal of the logic of evidence aggregation (LEA) was to describe probabilistic evidence aggregation in the setting of formal logic. However, as noted in that paper, LEA is not complete with respect to probability semantics. This leaves open the tasks to find sound and complete semantics for LEA and a proper axiomatization for probability semantics. We do both. We define a class of basic models called deductive basic models, and show LEA is sound and complete with respect to this class. We also define an axiomatic system LEA+ extending LEA and show it is sound and complete with respect to probability semantics.
  24. 2021.09.30: Вероятностый анализ логического следования
    Докладчик: С.Н.Артемов, Нью Йорк
    Slides
    Аннотация. Представьте себе множество пропозициональных формул Gamma = {F_1,...,F_n}, возможно противоречивое, и пусть Х логически следует из Gamma. Допустим также что допущения из Gamma носят вероятностный характер и для каждого F_i известно достаточное условие его выполнения, событие e_i. Каково совокупное свидетельство (aggregated evidence) AE(X) для Х как функция от e_1,...,e_n?

    Известно решение, когда e_i заданы числами - нижними оценками вероятности для F_i. Такая совокупная нижняя оценка в числовом выражении применима при "технологических" высоких вероятностях близких к 1. Однако, в силу привязки к худшему случаю, такие нижние числовые оценки быстро вырождаются в 0 и бесполезны при средних "социальных" вероятностях.

    Мы предлагаем находить совокупное свидетельство AE(X) для Х в символической форме в виде функции t(e_1,...,e_n) перед вычислением числовых оценок. Таким образом появляется возможность отойти от анализа худшего случая и использовать дополнительную информацию о событиях e_i для получения более тонких нижних оценок. Доказано, что AE(X) является теоретически наилучшим совокупным свидетельством для Х при данном Gamma.

  25. весна 2021
  26. 2021.05.27: PSpace-трудность в модальной логике: следствия из конструкции Ладнера
    Докладчик: Шапировский Илья Борисович, ИППИ РАН, New Mexico State University.
    Видеозапись доклада: YouTube
    Аннотация. Согласно теореме Ладнера, всякая модальная логика, содержащаяся в S4, является PSpace-трудной [Ladner77]. На самом деле, доказательство Ладнера даёт PSpace-трудность для более широкого класса модальных логик, например, для всех логик, содержащихся в логике Гёделя – Лёба GL или в логике Гжегорчика Grz. С некоторыми модификациями доказательство работает для логик, содержащихся в S4.1, S4.2 и многих других [Spaan 1993]. В докладе будут обсуждаться конструкции Ладнера и Спаан, а также их следствия.

    [1] R. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing, 6(3):467-480, 1977.
    [2] E. Spaan. Complexity of Modal Logics, PhD thesis. University of Amsterdam, Institute for Logic, Language and Computation, 1993.

  27. 2021.05.20: Nuclear implicative semilattices: a finitarity result
    Speaker: Silvio Ghilardi (University of Milan)
    (joint work with Guram & Nick Bezhanishvili, L. Carai, David Gabelaia, M. Jibladze.
    Video: YouTube | Slides
    Abstract. Diego's theorem says that the implication-conjunction fragment of intuitionistic logic is locally finite. We show that the result persists if we enrich the language with a nucleus, that is with a modality j satisfying the conditions x & j(x) = x,
    j(j(x)) = j(x),
    j(x & y) = j(x) & j(y).
    Nuclei arise from the study of locales and topoi and they were also more recently motivated by some computer science applications. In order to prove the result, we employ, adapt and revisit well-known universal model constructions in non-classical logics.
  28. 2021.04.29: Модальные формулы Янкова – Файна и их применения
    Докладчик: Золин Е.Е.
    Видеозапись доклада: YouTube | Слайды
    Аннотация. В докладе речь пойдет о модальных «характеристических» формулах Янкова – Файна. Будет рассказано об их основных свойствах и применениях к таким вопросам, как характеризация конечной порожденной точкой шкалы Крипке, алгоритмическая разрешимость проблемы равенства (и включения) логик двух конечных шкал, критерий модальной определимости класса конечных транзитивных шкал, эффективное построение аксиоматики табличной логики, характеризация Блока конечных шкал, чьи логики дают расщепление решетки всех логик.
  29. 2021.04.15: Игры Эренфойхта и представления цилиндрических алгебр (продолжение)
    Докладчик: Рогозин Даниил (ИППИ РАН)
    Видеозапись доклада: YouTube | Слайды
  30. 2021.04.08: Представимые цилиндрические алгебры, ver.2 (абстракт ниже)
    Докладчик: Рогозин Даниил (ИППИ РАН)
    Видеозапись доклада: YouTube | Слайды
  31. 2021.03.25: Игровая семантика логических формул при наличии ограничений на вычислительную сложность стратегий
    Докладчик: Соловьев Сергей (Институт информатики Университета Тулузы-3)
    Видеозапись доклада: YouTube | Слайды
    Аннотация.Игровая семантика логических формул разрабатывалась с целью показать возможность игровой интерпретации (игры между «утвердителем» и «опровергателем», Verifier and Falsifier), которая приводит к стандартной семантике, полученной более традиционным путем. Было показано, что Verifier имеет выигрышную стратегию в игре, построенной по формуле А, в том и только том случае, когда А выводима в соответствующей дедуктивной системе или истинна в модельно-теоретическом смысле.

    Хорошо известно, что ограничения на классы стратегий противников могут вести к тому, что этот результат больше не будет иметь места. В связи с этим изучался вопрос о «допустимых» ограничениях: например, возможно ли получить аналогичный результат, рассматривая только вычислимые стратегии. В работе ограничения рассматриваются с другой точки зрения: насколько семантика может быть «искажена» в результате некоторой естественной асимметрии между игроками. С учетом различных типов игр, рассматривавшихся в литературе, в работе рассматриваются, например, игры, в которых один из противников может «брать ход назад». Выясняется, что при наличии ограничений на вычислительную сложность возможны ситуации, когда Verifier имеет выигрышную стратегию для некоторых формул, ложных в обычном смысле. Эти ситуации не выглядят искусственными — например, преимущество Verifier'a может состоять в том, что он способен вычислять универсальную функцию для стратегий Falsifier'a.

    Цель работы лежит скорее в практической области, чем в области оснований математики — привлечь внимание к тенденции в современной науке, когда «научным» считается подтверждение, основанное на тестах, а не доказательствах, и «игроки», имеющие доступ к превосходящим вычислительным ресурсам, могут получать неоправданное преимущество.

  32. 2021.03.18: Представимые цилиндрические алгебры, ver.1
    Докладчик: Рогозин Даниил (ИППИ РАН)
    Видеозапись доклада: YouTube | Слайды
    Аннотация. Доклад основан на работах Робина Хирша и Иена Ходкинсона [1], [2].

    Цилиндрические алгебры — это разновидность булевых алгебр с операторами, которая была введена и изучена школой Тарского в 50-60-е годы. Изначальной мотивацией для исследования цилиндрических алгебр была алгебраизация логики предикатов первого порядка с равенством. Цилиндрические алгебры также могут быть использованы в изучении многомерных модальных логик и реляционных баз данных.

    Представлением цилиндрической алгебры A размерности α (где α — ординал) является вложение A в некоторую цилиндрическую алгебру множеств, то есть алгебру α-мерных отношений с оператором цилиндрификации, который служит своего рода алгебраическим 'аналогом' квантора существования.

    Представление цилиндрических алгебр — это довольно сложный и тонкий вопрос, в отличие от просто булевых алгебр, которые представимы как подалгебры алгебр подмножеств по теореме Стоуна. Сложность этого вопроса заключается в существовании непредставимых цилиндрических алгебр, поскольку в таком случае мы не располагаем теоремой о представлении для всех алгебр. <!--

    В докладе мы обсудим то, как можно проводить характеризацию представимых цилиндрических алгебр с использованием игр Эренфойхта.-->

    [1] Robin Hirsch and Ian Hodkinson. “Complete Representations in Algebraic Logic”, 1997. Статья
    [2] Robin Hirsch and Ian Hodkinson. “Completions and Complete Representations”, 2013. Статья

  33. 2021.03.04: Отрицание как модальный оператор в рамках логики предикатов
    Докладчик: Сперанский Станислав Олегович (МИАН им. В.А.Стеклова)
    Видеозапись доклада: YouTube | Слайды
    Аннотация. Идея интерпретации отрицания как (негативной) модальности используется в немалом числе логических систем; особого упоминания здесь заслуживает предложенная Дошеном пропозициональная логика N, в которой отрицание слабее, чем в «минимальной» логике Йохансона. Среди интересных расширений N можно выделить пропозициональные логики N* и Hype. Первая из них была предложена Кабаларом, Одинцовым и Пирсом в качестве базы для изучения оснований фундированной семантики логических программ с отрицанием; вторая же в последнее время рекламировалась Ляйтгебом как основная система для работы с «гиперинтенциональными контекстами», однако впервые она была описана Мойсилом ещё в 1942.

    В моей недавней работе были изучены предикатные версии N и N*, а также описана простая семантика типа Раутли (где отрицание определяется посредством антимонотонной функции на возможных мирах) для предикатной версии Hype из статьи Ляйтгеба. В докладе будут приведены соответствующие результаты о сильной полноте. Кроме того, Ляйтгеб ошибочно утверждал, что Hype, подобно интуиционистской логике, обладает дизъюнктивным свойством. Однако это не так. Поэтому мы бегло обсудим дизъюнктивное и экзистенциальное свойства в контексте изучения кванторных расширений N. В целом исследования в данной области можно рассматривать как часть общей программы по изучению кванторных интуиционистских модальных логик.

  34. 2021.02.25: Гиперграфовые грамматики Ламбека, часть 2
    Докладчик: Пшеницын Тихон Григорьевич, 4 курс (науч. рук. М. Р. Пентус)
    Видеозапись доклада: YouTube | Слайды (те же)
    Аннотация. Гиперграфовое исчисление Ламбека возникло из желания совместить принципы обычного исчисления Ламбека с принципами грамматик замещения гиперребер. В частности, по аналогии с обычными грамматиками Ламбека, можно определить гиперграфовые грамматики Ламбека (ГГЛ). Эти грамматики представляют собой альтернативный грамматикам замещения гиперребер формализм для порождения гиперграфовых языков.

    В докладе дается необходимая для понимания основных определений интуиция, в том числе, под новым углом рассмотрены аксиомы и правила гиперграфового исчисление Ламбека. На примерах мы показываем, что гиперграфовые грамматики Ламбека обладают возможностью описывать более сложные (но при этом часто возникающие в приложениях) структуры, чем просто строки. Доказана NP-полнота проверки принадлежности гиперграфа языку, распознаваемому ГГЛ.

    Ключевой вопрос, на который дается ответ в данном докладе — выполняется ли для ГГЛ теорема Пентуса: верно ли, что всякий язык, порождаемый ГГЛ, является контекстно-свободным? Несколько неожиданный ответ — нет. Так, данные грамматики могут порождать язык всех графов без изолированных вершин. Кульминационный результат, кратко обсуждаемый к концу доклада, заключается в том, что ГГЛ порождают конечные пересечения контекстно-свободных гиперграфовых языков. Из этого следует в том числе, что ГГЛ могут порождать строковые языки, которые не порождаются грамматиками замещения гиперребер, а также то, что для них не выполняется теорема Парика.

  35. 2021.02.18: Гиперграфовые грамматики Ламбека, часть 1
    Докладчик: Пшеницын Тихон Григорьевич, 4 курс (науч. рук. М. Р. Пентус)
    Видеозапись доклада: YouTube | Слайды
    Аннотация. В докладе были введены определения грамматик замещения гиперребер и гиперграфового исчисления Ламбека. В формате дискуссии были обсуждены принципы, лежащие в основе вводимого автором доклада исчисления, в том числе, его языковая семантика.
  36. осень 2020
  37. 2020.12.17: Кобордизмы и коммутативные категориальные грамматики
    Докладчик: Славнов Сергей Андреевич, НИУ ВШЭ.
    Видеозапись доклада: YouTube | Слайды
    Аннотация. Под категориальными грамматиками обычно понимают логические грамматики, основанные на вариациях некоммутативной линейной логики, в первую очередь — на исчислении Ламбека. Менее известны так называемые абстрактные категориальные грамматики (АКГ), в которых в качестве системы типов используется обычная импликативная линейная логика. Их можно назвать коммутативными.

    С одной стороны, АКГ привлекают замечательной простотой базовой логики, к тому же они гибче и выразительней некоммутативных вариантов. С другой стороны, это системы с довольно неудобным интерфейсом. Основные объекты в АКГ — линейные лямбда-термы; чтобы распознать в такой кодировке конкретные элементы языка, требуются усилия.

    Мы показываем, что АКГ имеют простое интуитивное представление в очень естественной геометрической структуре, которую мы называем категорией словесных кобордизмов. Категория словесных кобордизмов кажется вполне замечательной и сама по себе. Кроме того, основываясь на этом представлении, можно развивать и другие варианты коммутативных грамматик, например, использующие классическую (а не интуиционистскую) линейную логику.

    Будет много красивых картинок и, среди прочего, простая геометрическая демонстрация того, как коммутативная грамматика может порождать NP-полный язык.

  38. 2020.03.10: Эпистемические модели как обозреваемые фрагменты моделей Крипке
    Epistemic models as the observable fragments of Kripke models
    Докладчик: Артёмов Сергей Николаевич (Sergei Artemov), Graduate Center CUNY, New York
    Доступны слайды.
    Аннотация. Эпистемическая интерпретация моделей Крипке скрытно предполагает общее знание модели, что существенно ограничивает возможности их применения в эпистемологии. Мы исследуем эпистемические модели возможных миров в самом общем случае, без предположения общего знания модели, и показываем, что каждая такая эпистемическая модель является «обозреваемым фрагментом» некоторой модели Крипке. Мы обсудим начала соответствующей теории и покажем, что они приводят к новому уровню ясности в эпистемическом моделировании. Подобный анализ применим и к интуиционистским моделям.

    Abstract. Epistemic reading of Kripke models relies on a hidden assumption of common knowledge of the model which is too restrictive in epistemic contexts. We explore possible worlds epistemic models in their full generality without common knowledge of the model assumptions and show that an epistemic model can be identified as an “observable fragment” of some Kripke model. We sketch a corresponding theory and argue that it offers a new level of conceptual clarity in epistemic modeling. Similar analysis applies to intuitionistic models.

  39. 2020.12.03: Гиперграфовое исчисление Ламбека
    Докладчик: Пшеницын Тихон Григорьевич, 4 курс (науч. рук. М. Р. Пентус)
    Видеозапись доклада: YouTube | Слайды
    Аннотация. Исчисление Ламбека — это логический формализм, введенный в 1958 году И. Ламбеком для описания синтаксиса естественных языков. Для математиков интересны как собственно логические свойства этого исчисления (устранимость сечения, логические эквивалентности, модели и др.), так и свойства категориальных грамматик, в основу которых оно положено (один из основных результатов в данной области — эквивалентность контекстно-свободным грамматикам).

    Помимо этого, известно, что контекстно-свободные грамматики можно обобщить на гиперграфы — получатся так называемые гиперграфовые грамматики (им был посвящен доклад 19 ноября). Возникает вопрос: возможно ли аналогичным способом обобщить на гиперграфы исчисление Ламбека? Оказывается, возможно.

    В данном докладе мы представим такое обобщение (введенное докладчиком), называемое гиперграфовым исчислением Ламбека. Будет показано, что в него вкладывается исчисление Ламбека, а также многие его разновидности: исчисление Ламбека с единицей, с модальностями, с правилом перестановки, с операцией обращения (reversal operation). Будет представлена теорема об устранимости сечения в данном гиперграфовом исчислении и дана сложностная характеристика проблемы выводимости секвенции.

    В будущих докладах мы надеемся осветить и другие аспекты гиперграфового исчисления Ламбека: структурные свойства, категориальные грамматики и их распознающую силу, модели.

  40. 2020.11.26: Сложность произведений модальных логик с логикой K в языке с одной переменной
    Докладчик: Рыбаков М.Н. (Тверской государственный университет),
    Соавтор: Шкатов Д.П. (Йоханнесбург).
    Видеозапись доклада: YouTube | Слайды
    Аннотация. Произведения модальных логик введены в 1970-х годах независимо К.Сегербергом и В.Б.Шехтманом. С тех пор они активно изучались и нашли приложения в разных областях знания. Известно, что произведения логик могут иметь очень высокую алгоритмическую сложность, значительно превосходящую сложность каждой из перемножаемых логик (в том числе могут быть неразрешимыми и даже «сильно» неразрешимыми). Возникает вопрос о сложности их фрагментов, получающихся в результате ограничений на использование средств языка.

    В рамках семинара предполагается обсудить вопрос о сложности произведений пропозициональных модальных логик при наличии в языке лишь конечного числа переменных. Авторами будет представлен следующий результат: если в произведении модальных логик один из сомножителей равен K, то всё это произведение полиномиально погружается в свой фрагмент с одной переменной.

    Используемая в доказательстве техника переносится на произведения с полимодальными логиками с K-модальностью, а также на полупроизведения логик, где имеется K-модальность, что тоже предполагается обсудить.

  41. 2020.11.19: Позвольте представить: грамматики замещения гиперрёбер
    Докладчик: Пшеницын Тихон Григорьевич, 4 курс (науч. рук. М. Р. Пентус)
    Видеозапись доклада: YouTube | Слайды
    Аннотация. Название доклада является отсылкой к названию статьи 1986 года “May we introduce to you: Hyperedge replacement” авторов Annegret Habel и Hans-Jorg Kreowski. По материалам данной статьи и учебника 1997 года “Handbook on Graph Grammars and Computing by Graph Transformation” под редакцией Гжегожа Розенберга нами будет сделан обзор теории графовых грамматик, а точнее, их специального вида — грамматик замещения гиперрёбер. Данные грамматики были разработаны в 1970-х годах; они естественным образом обобщают контекстно-свободные грамматики и, в частности, наследуют их свойства.

    В первой части доклада будут даны определения и примеры, связанные с грамматиками замещения гиперрёбер; будут сформулированы фундаментальные результаты: лемма-насос, факты о порождающей силе грамматик, NP-полнота. Во второй части будет представлен доказанный нами результат о существовании для грамматик замещения гиперрёбер (за исключением незначительного класса случаев) слабой нормальной формы Грейбах. Данный результат является стартовой точкой для последующих исследований о возможности обобщить на гиперграфы категориальные грамматики Ламбека и само исчисление Ламбека. Об этом мы надеемся сделать серию докладов в будущем.

  42. 2020.11.12: The modal logic of almost sure frame validities in the finite
    Talk by: Valentin Goranko (University of Stockholm)
    Video of the talk: YouTube | Slides
    Abstract. A modal formula is almost surely valid in the finite if the probability that it is valid in a randomly chosen finite frame with n states is asymptotically 1 as n grows unboundedly. In this talk I will discuss the normal modal logic MLas of all modal formulae that are almost surely valid in the finite. Because of the failure of the zero-one law for frame validity in modal logic, the logic MLas extends properly the modal logic of the countable random frame MLr, which was completely axiomatized in a 2003 paper by Goranko and Kapron.

    In a recent work, I have studied the logic MLas, provided a certain model-theoretic characterisation of its additional validities beyond those in MLr, and raised some open problems and conjectures regarding the missing additional axioms over MLr and the explicit description of the complete axiomatisation of MLas, which may turn out to hinge on difficult combinatorial-probabilistic arguments and calculations.

    The talk is based on the paper [1]. At the end of the talk a listener (S. Kikot) mentioned the paper [2].

    [1] Goranko V. The modal logic of almost sure frame validity in the finite. Advances in Modal Logic, 2020, to appear in Proceedings.
    [2] Popova S., Zhukovskii M. Existential monadic second order logic of undirected graphs: The Le Bars conjecture is false. Annals of Pure and Applied Logic, 2019, vol. 170, num. 4, pp. 505-514. DOI 10.1016/j.apal.2018.12.001

  43. 2020.11.05: О канонической окрестностной шкале модальной логики транзитивного замыкания K+
    Докладчик: Шамканов Д. С.
    Видеозапись доклада: YouTube
    Аннотация. Хотя для многих модальных логик конструкция канонической шкалы Крипке позволяет элегантно получить результат о реляционной полноте, существуют интересные и важные логики, для которых данная конструкция не работает. В частности, для модальных логик GL, GLP и K+ конструкция канонической шкалы Крипке не дает результат о реляционной полноте.

    Однако для каждой из этих логик можно построить каноническую окрестностную шкалу, наличие которой влечет окрестностную полноту соответствующей логики. В нашем докладе мы детально обсудим конструкцию канонической окрестностной шкалы для случая модальной логики транзитивного замыкания K+.

  44. 2020.10.29: Свойство конечного представления для редуктов представимых алгебр отношений
    Докладчик: Даниил Рогозин (ИППИ РАН)
    Видеозапись доклада: YouTube | Слайды
    Аннотация. Алгебры отношений (RA) — это разновидность булевых алгебр с операторами, предлагающая алгебраизацию бинарных отношений [Tarski 1944]. Представление алгебры отношений — это изоморфизм между алгеброй отношений и алгеброй подмножеств бинарного отношения. Представимые алгебры отношений (RRA) — это замыкание таких алгебр подмножеств над бинарными отношениями относительно изоморфных копий.

    Как известно, существуют непредставимые алгебры отношений [Lyndon 1950], и, таким образом, первопорядковые теории RA и RRA не совпадают. Более того, представимость для конечных алгебр отношений — это алгоритмически неразрешимая проблема [Hirsch, Hodkinson 2001].

    В связи с этим, естественным направлением является изучение редуктов алгебр отношений, то есть алгебр отношений, сигнатура которых — это некоторая подсигнатура сигнатуры алгебры отношений. В частности, такие редукты изучаются на предмет наличия конечной аксиоматизации и свойства конечного представления (когда каждая представимая конечная структура изоморфна представимой алгебре на конечной базе).

    В этом докладе мы обсудим текущие результаты в изучении редуктов алгебр отношений, такие как конечная (не)аксиоматизируемость и конечная (не)представимость. В частности, мы покажем, что представимые полугруппы с делениями обладают свойством конечного представления (что было открытой проблемой в [Hirsch, Hodkinson 2002]).

    Мы покажем что всякая полугруппа с делениями представима как подалгебра представимый полугруппы, упорядоченной в полной решетке, с использованием соответствия Галуа и пополнений по Дедекинду-Макнейлу.

    Наконец, мы предъявим контрпример, нарушающий свойство конечного представления для полугрупп, упорядоченных в верхней полурешетке, используя недавний результат из [Maddux 2016].

  45. 2020.10.22: О тетрахотомии сложности по данным для дизъюнктивных логических программ одного типа
    Докладчик: Станислав Кикоть, Оксфордский университет.
    Видеозапись доклада: YouTube | Слайды
    Аннотация. Доклад посвящен простейшим дизъюнктивным логическим программам, которые проверяют, следует ли из набора фактов и аксиомы покрытия (для всех х, A(x) влечет F(x) или T(x)) данный булев конъюнктивный запрос, состоящий из предикатов арности 1 и 2. Рассматривается задача о классификации конъюнктивных запросов в зависимости от сложности по данным проблемы нахождения ответа для такой программы; обсуждается ее место в более общем контексте.

    Будет предъявлено полное решение этой задачи для запросов, бинарные атомы которых организованы в форме направленной линии. Доклад основан на совместной работе с Ольгой Герасимовой, Аги Куруш, Михаилом Захарьящевым и Владимиром Подольским, недавно представленной на конференции "Knowledge Representation and Reasoning".

  46. 2020.10.15: Топологические модальные логики метрических пространств
    Докладчик: Кудинов Андрей Валерьевич, ИППИ, ВШЭ.
    Видеозапись доклада: YouTube
    Аннотация. Доклад по статье [1].

    В начале я коротко напомню определение топологической семантики модальной логики. Дам определение разреженного и слабо разреженного топологического пространства. Также для разреженного пространства я определю ранг Кантора-Бендиксона. В докладе мы ответим на вопрос: какие модальные логики могут возникать, как топологические модальные логики метрических пространств.

    Авторы показывают, что при этом могут возникнуть только следующие логики: S4, S4.1, Grz, Grz + bdn (где n — любое натуральное число). Здесь bdn — аксиома глубины n, ее общезначимость на транзитивных рефлексивных шкалах Крипке эквивалентна тому, что глубина шкалы не превышает n.

    Кратко результаты можно сформулировать следующим образом:

    1. Если метрическое пространство имеет открытое плотное в себе подмножество, то его логика равна S4.
    2. Если метрическое пространство слабо разреженное, но не является разреженным, то его логика равна S4.1.
    3. Если метрическое пространство разреженное, то логика зависит от его ранга Кантора-Бендиксона.
      • Если ранг конечен и равен n, логика равна Grz + bdn,
      • Если ранг бесконечен, то логика равна Grz.

    [1] Bezhanishvili, G., Gabelaia, D. and Lucero-Bryan, J., 2015. Modal logics of metric spaces. The Review of Symbolic Logic, 8(1), pp. 178-191. DOI: 10.1017/S1755020314000446.

  47. весна 2020
  48. 2020.03.12: Доксастический аналог логики SSL
    Докладчик: Кудинов Андрей Валерьевич, ИППИ, ВШЭ.
    Аннотация. Логика пространства подмножеств (Subset space logic, или коротко SSL) была введена в 1994 Добровским, Моссом и Парихом как логика ресурсов. Язык этой логики содержит две модальности: K для знания и &square; для ресурсов (или усилий). В качестве шкал для этой логики рассматриваются пары (X, O), где O — множество подмножеств X. Формулы оцениваются на парах (x,U), где x&in;U и U&in;O. Формула KA верна на (x,U), если формула A верна на всех парах вида (y, U). Формула &square;A верна на (x,U), если A верна на всех парах вида (x, V), где V — из O и подмножество U. Интуитивно формула &lozenge;A означает: A станет верно после некоторого усилия или после некоторой траты ресурсов. Аксиоматика для логики SSL состоит из аксиом логики S5 для модальности K, аксиом логики S4 для модальности &square;, а также «кросс-аксиомы» K &square; A → &square; K A.

    Мы рассмотрим доксастический аналог логики SSL, а именно логику, в которой модальность знания K заменена на модальность веры (belief) B. Если для моделирования знания обычно рассматривают логику S5, то для моделирования веры рассматривают логику KD45. Я расскажу, как можно изменить семантику, чтобы логика по первой модальности была KD45, докажу корректность и расскажу идею доказательства полноты.

  49. 2020.03.05: Логика дистрибутивных решеток с делениями и модальными операторами: канонические расширения и топологическая двойственность
    Докладчик: Рогозин Даниил Дмитриевич, МГУ.
    Аннотация. В докладе будет рассмотрена логика дистрибутивных решеток с делениями, расширенных модальными операторами, являющимися некоммутативными обобщениями &square; и &lozenge;. Далее мы определим шкалы Крипке для таких логик и покажем, что всякая каноническая логика полна по Крипке алгебраическим способом. Каноничность логики будет рассматриваться как замкнутость соответствующей логики относительно канонических расширений, которые также будут определены в докладе.

    Мы построим дискретную двойственность между шкалами Крипке и модальными совершенными дистрибутивными решетками. В таком случае полнота по Крипке всякой канонической логики будет следовать из замкнутости относительно канонических расширений соответствующего многообразия и дискретной двойственности.

    Далее мы усилим результат о дискретной двойственности — введем топологические шкалы Крипке для интересующих нас логик и установим топологическую двойственность (основанную на двойственности Пристли для ограниченных дистрибутивных решеток) между введенными топологическими шкалами Крипке и дистрибутивными решетками с делениями, расширенными модальными операторами.

  50. осень 2019
  51. 2019.12.05: Базовые категориальные грамматики с однозначным присвоением типов
    Докладчик: Вишникин Максим Евгеньевич, 5 курс, науч. рук. С. Л. Кузнецов
    Аннотация. Понятие базовой категориальной грамматики (БКГ) восходит к работам Айдукевича (1934) и Бар-Хиллела (1953). В БКГ каждая буква алфавита сопоставляется нескольким типам (категориям), а слово принадлежит языку, если хотя бы для одного выбора этих типов выводима соответствующая секвенция. Известно, что для любой контекстно-свободной грамматики существует БКГ, задающая тот же язык (возможно, за вычетом пустого слова). Верно и обратное.

    Доклад будет посвящен рассмотрению контекстно-свободных языков, которые могут быть заданы БКГ, где каждой букве присвоен ровно один тип. В ходе доклада планируется детально рассмотреть случай одно/двухбуквенных языков и вопрос, какие БКГ с однозначным присвоением типов задают автоматные языки, а какие нет (неавтоматными будут почти все). Также планируется доказать несуществование алгоритма, который по произвольной контекстно-свободной грамматике определит, существует ли эквивалентная ей БКГ с однозначным присвоением типов.

  52. 2019.11.28: Топологическая двойственность и модальная логика (продолжение)
    Докладчик: Рогозин Даниил Дмитриевич, МГУ.
  53. 2019.11.21: Топологическая двойственность и модальная логика
    Докладчик: Рогозин Даниил Дмитриевич, МГУ.
    Аннотация. Доклад является вводным рассказом о том, как применяется теория двойственности к модальным логикам. Модальные алгебры — это булевы алгебры с операторами. Данные алгебры выполняют роль алгебр модальных логик. Довольно естественно расширить двойственность Стоуна для булевых алгебр на модальные алгебры. Мы рассмотрим две двойственности.

    Для начала мы рассмотрим более простую двойственность между шкалами Крипке и совершенными модальными алгебрами, то есть полными атомными булевыми алгебрами, в которых модальный оператор обладает свойством полной аддитивности. После чего мы обобщим конструкцию для шкал Крипке и установим топологическую двойственность между топологическими шкалами Крипке (шкалами Крипке над пространствами Стоуна) и произвольными (не обязательно совершенными) модальными алгебрами. Такая двойственность расширяет двойственность Стоуна между булевыми алгебрами и вполне несвязными компактными хаусдорфовыми топологическими пространствами, то есть пространствами Стоуна.

    Если останется время, то мы обсудим связь топологической двойственности для модальных алгебр с обобщёнными шкалами Крипке.

  54. 2019.11.14: О грамматиках исчисления Ламбека с факультативными делениями (продолжение)
    Докладчик: Пшеницын Тихон Григорьевич, студ. 3 курса, науч. рук. М. Р. Пентус
  55. 2019.11.07: О грамматиках исчисления Ламбека с факультативными делениями
    Докладчик: Пшеницын Тихон Григорьевич, студ. 3 курса, науч. рук. М. Р. Пентус
    Аннотация. Исчисление Ламбека — логический формализм, который может быть использован для описания естественных языков. Один из простых примеров его применения — описание аргументов глагола. К примеру, предложению “Tim loves Helen” соответствует секвенция n (n\s)/n n → s в исчислении Ламбека; тип (n\s)/n отражает тот факт, что глагол “loves” имеет 2 обязательных аргумента — подлежащее (Tim) и дополнение (Helen).

    В лингвистике, однако, рассматривают примеры так называемых необязательных аргументов глагола: к примеру, в предложении “Tim bet Helen 5$ that they hired Alex” («Тим поспорил с Хелен на 5 долларов, что они наняли Алекса») можно опустить и дополнение Helen, и дополнение 5$, и зависимое придаточное “that they hired Alex”; к примеру, можно сказать “Tim bet Helen” («Тим поспорил с Хелен”).

    Чтобы разумно описать данное явление с формальной точки зрения, нами рассматривается фрагмент исчисления Ламбека с конъюнкцией, а именно вводятся левое и правое факультативные деления. В рамках доклада мы дадим определение этих операций, рассмотрим примеры выводимых секвенций с их использованием. В основной части доклада будут сформулированы и доказаны теоремы, характеризующие класс языков, порождаемых грамматиками Ламбека с факультативными делениями; в частности, будет доказано, что всякое конечное пересечение контекстно-свободных языков задаётся одной из таких грамматик.

  56. 2019.10.31: Градуированная модальная логика: аксиоматика, разрешимость, определимость
    Докладчик: Золин Е.Е.
    Аннотация. В стандартном модальном языке имеется оператор возможности, означающий: формула верна в некотором последователе данного мира. Как с теоретической точки зрения, так и в некоторых приложениях естественно рассмотреть модальные логики с градуированными модальностями, означающими: формула верна в не менее (не более) n последователях данного мира. Первая аксиоматика градуированной модальной логики GrK класса всех шкал и соответствующая теорема о полноте появилась в работе Файна “In so many possible worlds” (1972). Далее последовала серия из 7 работ “Graded Modalities I, II, ..., VII” (1985–1999) итальянских исследователей (Fattorosi-Barnaba, de Caro, Cerrato и др.), причем первые 4 работы (то есть до 1994 года) они написали, не зная о существовании работы Файна; в частности, в 1988 году независимо от Файна нашли (другую) аксиоматику логики GrK.

    В докладе дается обзор основных результатов в этой области: «конечная» (в некотором расширенном смысле) аксиоматизируемость градуированных аналогов «традиционных» модальных логик, таких как K, K4, S4, S5, в частности, необычные аксиомы для градуированной логики S4; разрешимость и сложность этих логик (Казаков, Pratt-Hartmann, 2009); неразрешимость логики с градуированными прямыми и обратными модальностями (Золин, 2011), систематизация вычислительной сложности логик в языках, имеющих градуированные модальности и/или градуированные обратные модальности (Bednarczyk, Kieronski, Witkowski, 2018); характеризация градуированного модального языка (GrML) как фрагмента языка первого порядка, инвариантного относительно градуированных бисимуляций (van der Hoek 1992, de Rijke 2000); критерий GrML-определимости классов отмеченных моделей Крипке (de Rijke 2000); аналог теоремы Гольдблатта–Томасона, т.е. критерий GrML-определимости классов шкал Крипке (Katsuhiko Sano, Minghui Ma, AiML 2010). Упомянуты некоторые открытые вопросы в этой области.

    Дополнение. Недавно получен аналог теоремы Розена о характеризации: над классом конечных моделей градуированный модальный язык является в точности фрагментом языка первого порядка, инвариантным относительно градуированных бисимуляций (Martin Otto “Graded modal logic and counting bisimulation”, 2019). Там же приводится описание градуированных бисимуляционных игр.

    Многие из тем доклада освещены подробнее в лекциях докладчика «Модальная логика 2014-2015 года».

  57. 2019.10.24: Модальные интуиционистские логики: в поисках семантики
    Докладчик: Кудинов Андрей (НИУ ВШЭ), Агамов Раджаб (асп. ВШЭ, науч. рук. А.В.Кудинов)
    Аннотация. У многих авторов, начиная с работы Фитча (Fitch) 1948 года, возникала идея построить модальную интуиционистскую логику, с естественным желанием, чтобы ее безмодальный фрагмент совпадал с интуиционистской логикой. Это оказалось сделать не так просто, и за эту задачу за прошедшие 70 лет брались многие исследователи.

    Подобно тому, как в интуиционистской логике 1-го порядка кванторы и не выражаются друг через друга, в модальной интуиционистской логике модальности «необходимость» &square; и «возможность» &lozenge; тоже не выражаются друг через друга. Если рассматривать языки только с &square; или только с &lozenge;, все получается довольно хорошо. Проблемы начинаются, когда мы пытаемся построить «естественный» язык, содержащий обе модальности. Без хорошей семантики тут не обойтись, но все известные варианты имеют свои недостатки.

    Мы попробуем объяснить, в чем же заключаются сложности и какие есть достижения в этой области. В заключение мы немного скажем о нашем проекте: рассмотреть окрестностную семантику для модальной интуиционистской логики.

  58. 2019.10.17: Отсутствие рекурсивной перечислимости логики QK* в языке с двумя предметными переменными
    Докладчик: Рыбаков Михаил Николаевич (Тверской государственный университет)
    Аннотация. Будет обсуждаться доказательство результата Ф. Волтера и М. Захарьящева о рекурсивной неперечислимости логики QK* в языке с двумя предметными переменными. Логика QK* определяется как множество модальных предикатных формул с двумя модальностями, соответствующими на шкалах Крипке отношению достижимости и его рефлексивно-транзитивному замыканию, истинных во всех предикатных шкалах Крипке.

    Будет также обсуждаться распространение использованной техники на другие предикатные логики, определяемые семантически (например, предикатные логики шкал логик GL и Grz), и усиление результата для языка с одним одноместным предикатом.

    Если позволит время, то будет показано, как получать аналогичные результаты в интуиционистском случае.

  59. 2019.10.10: Алгебры доказуемости формальных теорий (продолжение)
    Докладчик: Колмаков Евгений Александрович, ВШЭ, факультет математики
  60. 2019.10.03: Алгебры доказуемости формальных теорий
    Докладчик: Колмаков Евгений Александрович, ВШЭ, факультет математики
    Аннотация. Как известно, алгебра Линденбаума формальной системы не отражает теоретико-доказательственную силу этой системы. Действительно, для любых двух достаточно сильных перечислимых непротиворечивых теорий соответствующие им алгебры Линденбаума являются счётными безатомными булевыми алгебрами и поэтому изоморфны.

    Обогащение алгебры Линденбаума унарным оператором доказуемости в данной формальной теории приводит к понятию алгебры доказуемости для этой теории. Такие структуры позволяют выразить многие факты о доказуемости и отличить разные по силе теории (в частности, алгебры доказуемости для теорий PA и ZF неизоморфны).

    В докладе будет дан обзор ряда основных результатов об алгебрах доказуемости формальных теорий: характеризация логики алгебры доказуемости для данной арифметической теории (теорема Соловея об арифметической полноте и её равномерный вариант), описание всех подалгебр данной алгебры (теоремы Шаврукова и Замбеллы), неразрешимость элементарной теории алгебры доказуемости (теорема Шаврукова), достаточные условия изоморфизма и неизоморфизма, существование нетривиальных автоморфизмов (теоремы Шаврукова и Адамссона). Планируется подробно изложить общую схему доказательства достаточных условий неизоморфизма двух алгебр, а также обсудить возможные усиления этого результата.

    На первом заседании семинара было рассказано доказательство теоремы Соловея (1976): Для любой арифметической перечислимой теории T бесконечной характеристики (то есть не доказывающей утверждение &square;n&bottom; ни для какого n) совокупность доказуемых в T принципов доказуемости в точности совпадает с логикой Гёделя–Лёба GL.

  61. весна 2019
  62. 2019.05.16: Пропозициональная динамическая логика PDL
    Докладчик: Золин Е.Е.
    Аннотация. Планируется рассказать о пропозициональной динамической логике PDL, ее синтаксисе, семантике, выразительных возможностях, аксиоматике. Будут изложены основные идеи относительно простого доказательства Козена и Париха (Kozen, Parikh, 1981) ее полноты относительно конечных шкал Крипке (финитной аппроксимируемости и, как следствие, разрешимости).

    Кроме того, будет дан обзор некоторых результатов о языках, тесно связанных с PDL (в частности, монадическом языке второго порядка, модальном мю-исчислении, инфинитарном модальном и первопорядковом языках), в частности, теорем о характеризации в терминах бисимуляционной эквивалентности (так называемых Invariance Theorems и Safety Theorems). Типичным результатом в этом ряду является теорема ван Бентема о том, что модальный язык в точности является бисимуляционно инвариантным фрагментом языка первого порядка (подходящей сигнатуры).

  63. 2019.04.11: Логика Гейтинга — Оккама и гиперинтенсиональность
    Докладчик: Одинцов Сергей Павлович (Новосибирский государственный университет)
    Аннотация. Поводом для доклада послужило выступление Ханнеса Ляйтгеба (Hannes Leitgeb) на конференции LP18 (Linguistics Prague 2018), где он ввел логику HYPE для рассуждений о гиперинтенсиональных контекстах. Оказалось, что эта логика близка к логике Гейтинга — Оккама, введенной в процессе исследования логических программ с отрицанием, т.е. с совершенно иной мотивацией. К тому же обе логики имеют примечательную характеризацию в рамках теории отрицания Вакарелова. Наконец, после представления упрощенной семантики Крипке и алгебраической семантики для HYPE станет ясно, что это типичный пример интенсиональной логики. В значительной степени это будет исторический доклад, включающий краткие обзоры теории отрицания Вакарелова и сведений о дедуктивных базах для немонотонных логик.
  64. 2019.04.04: Лексикографические произведения модальных логик
    Докладчик: Вахрушева Полина Викторовна (науч. рук. В.Б.Шехтман)
    Аннотация. В докладе будут рассмотрены лексикографические произведения — один из способов объединения модальных логик. Будут описаны основные свойства таких конструкций, а также доказаны результаты о полноте.

    Операция лексикографического произведения была предложена Филиппом Бальбиани (2009) и независимо C. Бабенышевым и В. Рыбаковым (2010). Обе эти операции могут быть определены в терминах операции упорядоченных сумм, рассмотренной Л. Беклемишевым в контексте логики GLP. Упорядоченная сумма также является частным случаем операции generalized sum of models (С. Шелах, 1975). И.Б. Шапировский (2008) использовал упорядоченные суммы для изучения вычислительной сложности модальных логик.

  65. 2019.03.28: Итерированные определения истинности и исчисление рефлексий
    Докладчик: Беклемишев Л.Д. (совместная работа с Е. Колмаковым и Ф. Пахомовым)
    Аннотация. Мы рассматриваем обогащение языка арифметики Пеано определениями истинности, удовлетворяющими эквивалентностям Тарского. Для полурешетки расширений элементарной арифметики в рассматриваемом языке изучаются операторы рефлексии. Формулируется строго позитивная модальная логика RCλ, описывающая тождества этой полурешетки, с которой связывается естественная система ординальных обозначений. Получающиеся теории на основе итерированных схем рефлексии позволяют интерпретировать некоторые известные предикативные фрагменты арифметики второго порядка и вычислить их ординалы и спектры консервативности.
  66. 2019.03.21: О точных моделях логики свидетельств
    Докладчик: Крупский В.Н.
    Аннотация. В моделях логики свидетельств операция произведения свидетельств означает извлечение логических следствий и удовлетворяет аксиомам аппликации: s:(F → G) → (t:F → [s*t]:G). Модель называется точной (относительно произведения), если для каждой истинной формулы вида [s*t]:G существует формула F («причина»), для которой посылки соответствующей аксиомы аппликации также истинны.

    Свойство точности моделей логики свидетельств играет существенную роль при формальном анализе эпистемических сценариев типа “Prime Minister Example” Б. Рассела. Вопрос об аксиоматизации этого свойства средствами логики свидетельств оставался открытым. Мы предлагаем полные аксиоматики для класса всех точных базисных моделей, а также для класса всех точных моделей в случае расширенного языка с дополнительной операцией + (объединение свидетельств).

  67. 2019.03.14: Модальные логики топологических пространств: две компактности и их связь (продолжение)
    Докладчик: Кудинов Андрей Валерьевич, к.ф.-м.н., ВШЭ.
  68. <!--
  69. 2019.03.14: Семинара не было.
  70. -->
  71. 2019.02.28: Модальные логики топологических пространств: две компактности и их связь
    Докладчик: Кудинов Андрей Валерьевич, к.ф.-м.н., ВШЭ.
    Аннотация. Доклад основан на недавней работе И. Ходкинсона и Р. Голдблатта, в которой авторы рассматривают различные модальные языки с топологической семантикой. Они рассматривают комбинации следующих модальностей: топологическая (основанная на операции взятия внутренности), деривационная (связанная с операцией взятия производного множества), универсальная модальность, модальность неравенства, модальность запутанности (tangled modality) и градуированная модальность (graded modality).

    Для всех этих языков можно задавать вопрос о полноте и сильной полноте относительно конкретного топологического пространства (класса пространств). Также авторы изучают вопрос, когда язык является компактным над некоторым топологическим пространством: когда для выполнимости множества формул достаточно выполнимости произвольного конечного подмножества? Кроме того, в топологии имеется своя компактность, говорящая, что в любом открытом покрытии найдётся конечное подпокрытие.

    Авторы доказали, что язык с деривационной модальностью и модальностью неравенства компактен относительно любого нульмерного некомпактного метрического пространства, но некомпактен относительно нульмерного компактного метрического пространства (с точностью до гомеоморфизма это Канторово пространство). Однако язык с топологической модальностью и градуированной модальностью компактен относительно Канторова пространства.

  72. осень 2018
  73. 2018.12.13: О пополнении модальных предикатных логик в семантике Крипке
    Докладчик: Шехтман В.Б.
    Аннотация. Для модальных логик предикатов проблема полноты в семантике Крипке очень нетривиальна. Многие из них оказываются неполными. Возникает естественный вопрос: каким образом исправить неполноту? В некоторых случаях это удается сделать, добавив недостающие аксиомы простого вида. В докладе будут доказаны несколько результатов на эту тему.
  74. 2018.12.06: О глобальной окрестностной полоноте логики GL и об алгебрах открытых множеств окрестностных GL-шкал
    Докладчик: Шамканов Д. С.
    Аннотация. Я напомню результат о глобальной окрестностной полноте логики GL с отношением выводимости, определенным с помощью нефундированных выводов, и расскажу о некоторых усилениях данной теоремы. Я также расскажу о решеточной характеризации алгебр открытых множеств окрестностных GL-шкал (или, другими словами, разреженных топологических простанств).
  75. 2018.11.29: Как спрятать дистрибутивность, или два контрпримера к полноте расширений исчисления Ламбека
    Докладчик: Кузнецов Степан Львович
    Аннотация. Известно, что закон дистрибутивности недоказуем в исчислении Ламбека, расширенном аддитивными конъюнкцией и дизъюнкцией, однако истинен при интерпретациях этого исчисления на формальных языках и на алгебре бинарных отношений (где конъюнкция и дизъюнкция интерпретируются теоретико-множественными операциями). Таким образом, дистрибутивность является препятствием к теореме о полноте. С другой стороны, для расширения одной конъюнкцией имеются теоремы о полноте. Вопрос об исчислении с одной дизъюнкцией оставался открыт.

    В докладе будут показаны два контрпримера, показывающие неполноту. Первый: формула в расширении исчисления Ламбека одной дизъюнкцией, истинная во всех дистрибутивных интерпретациях, но не выводимая: ослабленную форму закона дистрибутивности, оказывается, можно записать без конъюнкции. Второй: такая же формула в расширении исчисления Ламбека конъюнкцией и звёздочкой Клини. Здесь мы пользуемся скрытой внутри звёздочки Клини бесконечной дизъюнкцией.

  76. <!--
  77. 2018.11.22: Семинара не было.
  78. -->
  79. 2018.11.08: Коммутативная линейная логика как множественно контекстно-свободная грамматика
    Докладчик: Славнов Сергей Андреевич, к.ф.-м.н., ВШЭ.
    Аннотация. Множественно контекстно-свободные грамматики (multiple context-free grammars) — это нетривиальное обобщение контекстно-свободных грамматик, в котором правила оперируют сразу с конечными последовательностями слов, а не с отдельными словами. Они были предложены в 1990 годах, как один из более адекватных формализмов для моделирования естественного языка. Подобно контекстно-свободным грамматикам (КСГ), множественно контекстно-свободные грамматики (МКСГ) допускают эффективные алгоритмы синтаксического разбора («парсинга»), но при этом обладают строго большей выразительной силой.

    Хорошо известно, что КСГ порождают тот же класс формальных языков, что и категориальные грамматики, построенные на исчислении Ламбека, которое представляет собой вариант некоммутативной линейной логики. Мы предлагаем вариант категориальной грамматики на основе обычной коммутативной линейной логики и показываем, что получается система, эквивалентная МКСГ. Иными словами, получается, что исчисление Ламбека относится к КСГ так же, как линейная логика относится к МКСГ.

    Ключевой шаг состоит в наблюдении, что последовательности слов, с которыми оперируют МКСГ, можно оформить в симметрическую моноидальную категорию, которая оказывается моделью линейной логики.

  80. 2018.11.01: Квазинормальные модальные логики в расширениях логик GL и S, не имеющие независимой аксиоматизации
    Докладчик: Горбунов Игорь Анатольевич (Тверской государственный университет)
    Аннотация. Вопрос о существовании логик без независимой аксиоматизации тесно связан с вопросом о существовании аксиоматического базиса для эквациональных и квазиэквациональных теорий модальных алгебр. В 1995 г. А.В.Чагров и М.В.Захарьящев построили суперинтуиционистские и нормальные модальные логики (в расширениях логик K4 и S4) без независимой аксиоматизации. Тогда же был поставлен вопрос о существовании квазинормальных логик без независимой аксиоматизации. В докладе будет рассказано о способе построения таких логик и теорий, в частности, в расширениях логики Гёделя – Лёба GL и логики Соловея S.
  81. 2018.10.25: Топологическая модальная логика с модальностью неравенства
    Докладчик: Агамов Раджаб, аспирант ВШЭ, науч. рук. А.В.Кудинов
    Аннотация. Доклад посвящен топологической модальной логике T0-пространств с модальностью неравенства (для Tn-пространств, где n &geq;1, соответствующие логики были известны). Мы рассматриваем пропозициональную модальную логику с двумя модальными операторами: &Square; и [≠]. Модальность &Square; интерпретируется как оператор взятия внутренности, а модальность [≠] соответствует отношению неравенства. Мы определим логику S4DT0 и покажем, что она является логикой всех T0-пространств и финитно аппроксимируема (в смысле семантики Крипке).
  82. 2018.10.18: Примеры полных по Крипке перечислимых модальных предикатных логик, которые не полны относительно первопорядково определимых классов шкал Крипке
    Докладчик: Рыбаков Михаил Николаевич (Тверской государственный университет)
    Аннотация. Несложно показать, что если логика задаётся классом шкал Крипке, который определяется формулой первого порядка, то она имеет рекурсивную аксиоматику. В то же время известно много примеров модальных предикатных логик, которые определяются классами шкал Крипке, не описываемыми первопорядковыми формулами, и при этом неперечислимых. Такие логики не могут быть заданы в виде исчислений, а «естественные» модальные предикатные исчисления оказываются неполными по Крипке.

    Возникает вопрос о существовании полных по Крипке и перечислимых модальных предикатных логик, которые не полны относительно первопорядково определимых классов шкал. Примерно в 2001 году докладчику удалось показать, что такие логики существуют в классе квазинормальных логик. Этот результат не был нигде опубликован, он лишь докладывался на семинаре в Тулузе. Недавно мне удалось найти аналогичные примеры сначала в классе предикатных логик с двумя модальностями (причём вторая модальность была «обратной» к первой), а чуть позже — и в классе мономодальных нормальных предикатных логик. В обоих примерах существенно использовалось отсутствие транзитивности. В докладе предполагается показать эти примеры и обсудить возможности обобщения.

  83. 2018.10.11: Inquisitive semantics: an informational approach to the logic of questions
    Докладчик: Gianluca Griletti (Institute for Logic, Language and Computation, Amsterdam)
    Abstract. Through logic we are able to represent and study relations between a certain class of sentences, namely statements. Several different formalisms have been proposed to capture and analyze fragments of natural language, the most well-known example being the classical logic. Most of them are based on truth-conditional semantics – specifying when a sentence is true in a given context – and so they are not suitable to capture logical relations between questions. The aim of inquisitive semantics is to extend these formalisms to also encompass questions.

    This can be done by extending the truth-based account to an information-based one, and by defining an appropriate semantics, in which states of partial information play the role of the contexts. This allows us to represent statements and questions in a uniform way, and thus to also represent more complex kinds of sentences such as conditional questions.

    In this talk I will introduce the main ideas behind inquisitive semantics. Then I will describe in more detail two logics stemming from this approach: inqB, which corresponds to the classical propositional logic, and inqBQ, which corresponds to the classical predicate logic.

  84. 2018.10.04: О консервативности схем ограниченности (продолжение)
    Докладчик: Пахомов Ф.Н., к.ф.-м.н., МИАН.
  85. 2018.09.27: О консервативности схем ограниченности
    Докладчик: Пахомов Ф.Н., к.ф.-м.н., МИАН.
    Аннотация. Классы формул Π0n и Σ0n в арифметике первого порядка можно понимать в стандартном (узком) смысле, как состоящие из формул начинающиеся из подходящей кванторной приставки из неограниченных кванторов (∀x) после которой идет формула только с ограниченными кванторами (∀x≤t). Но также их можно понимать и в широком смысле, как классы формул, в которых ограничивается число альтернаций неограниченных кванторов, а ограниченные кванторы могут использоваться произвольным образом.

    Каждая Π0n- (Σ0n-) формула в широком может быть преобразована в Π0n- (Σ0n-) формулу в стандартном смысле. Естественный способ такого преобразования — это пронесение неограниченных кванторов сквозь ограниченные, что позволяет делать схема Σ0n-ограниченности 0n: (∀x≤y)   ∃z   φ(x,y,z)   →   ∃z0   (∀x≤y)   (∃z≤z0)   φ(x,y,z),    где   φ&in;Σ0n.

    Схемы 0n и их взаимоотношение с другими арифметическими аксиомами были предметом подробного изучения. В частности, еще в 1970-х независимо Х. Фридманом и Д. Парисом была доказана Π0n+1-консервативность схемы 0n+1 над теорией Σ0n-индукции 0n. Позднее этот результат был обобщен Л.Д. Беклемишевым, который дал простое необходимое и достаточное условие на Π0n+1 аксиоматизируемые теории T для достижения Π0n+1 консервативности схемы 0n над T.

    Описанная выше ситуация с пониманием иерархий Π0n и Σ0n в широком и узком смысле и наличием принципа нужного для проноса кванторов имеет свои аналоги для других теорий.

    В теории множеств ограниченными считаются кванторы вида ∀x&in;y, а принципы, дающие возможность проносить неограниченные кванторы сквозь ограниченные, — это схемы Σn-Coll (отмечу, что схема Σ1-Coll известна в качестве одной из аксиом теории множеств Крипке — Платека).

    В арифметике второго порядка роль неограниченных кванторов играют кванторы по множествам натуральных чисел, роль ограниченных кванторов — кванторы по натуральным числам, а для проноса кванторов используются схемы выбора Σ1n-AC.

    Для систем ограниченной арифметики естественные иерархии формул — это иерархии Σbn (фактически являющиеся уровнями полиномиальной иерархии из теории сложности); вместо неограниченных кванторов используются ограниченные кванторы ∀x≤t, a вместо ограниченных кванторов — строго ограниченные кванторы ∀x≤log2(t); соответствующие принципы ограниченности обозначаются BBΣbn.

    В настоящем докладе я расскажу об аналогах теоремы Беклемишева для теорий множеств, арифметик второго порядка и систем ограниченной арифметики (все они будут получены в качестве следствия из общего результата). Также я расскажу о том, как из этих общих теорем получается ряд конкретных результатов о частичной консервативности схем ограниченности и выбора над естественными формальными теориями.

  86. весна 2018
  87. 2018.05.10: Семантика типа Крипке для пропозициональной логики задач и высказываний
    Докладчик: Оноприенко Анастасия Александровна, студ. 6 курса, науч. рук. Л.Д.Беклемишев
    Аннотация. Предикатная логика QHC, введённая С.А. Мелиховым, объединяет в себе классическую логику высказываний и интуиционистскую логику задач, соединённых двумя модальностями ? и !. В докладе будет описан пропозициональный фрагмент HC этой логики, рассмотрена её семантика типа Крипке и доказана полнота логики HC относительно конечных шкал Крипке.
  88. <!--
  89. 2018.05.03: Семинара не было
  90. -->
  91. 2018.04.26: Полнота некоторых предикатных хорновых модальных логик относительно окрестностных шкал с постоянной предметной областью
    Докладчик: Кудинов Андрей Валерьевич, к.ф.-м.н., ВШЭ.
    Аннотация. В предикатной модальной логике для ряда логик доказана полнота относительно шкал Крипке с расширяющейся предметной областью. В частности, это доказано для так называемых односторонних хорновых логик (one-way Horn logics) (в книге Gabbay, Shehtman, Skvortsov “Quantification in Nonclassical Logic", 2009).

    Шкал Крипке с постоянной областью для полноты недостаточно, т.к. в них общезначима формула Баркан В отличие от шкал Крипке, в окрестностных шкалах формула Баркан не обязательно общезначима. Более того, оказывается, что для любой односторонней хорновой логики L ее предикатный вариант QL полон относительно окрестностных шкал с постоянной областью. Доказательство последней полноты мы и расскажем.

  92. 2018.04.19: Интервальные модальные логики с отношениями касания. Неразрешимые расширения
    Докладчик: Чижов Алексей Сергеевич, ИППИ, науч. рук. В.Б.Шехтман
    Аннотация. Модальная логика интервалов Халперна-Шохама (HS) содержит 8 основных отношений: «касаться», «содержать», «быть началом» и пр. Логика HS неразрешима, но многие её 1- и 2-модальные фрагменты финитно аппроксимируемы и имеют сложность от NP до NЕxpTime. Граница, отделяющая разрешимые фрагменты от неразрешимых, неочевидна.

    В докладе рассматриваются интервальные логики над линейными порядками, содержащие модальности для правого и левого касания, а также дополнительные модальности, добавление которых выводит логику из «области разрешимости». Приводится детальное построение редукции проблемы замощения плитками (tiling problem), что дает неразрешимость этих логик.

    Доклад основан на работе D. Brensolin, V. Goranko, A.Montanari, G.Sciavicco “Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions” (Annals of Pure and Applied Logic, 2009).

  93. 2018.04.12: Новая старая семантика линейной логики: линейные операторы и аналитические функции
    Докладчик: Славнов Сергей Андреевич, НИУ ВШЭ.
    Аннотация. Линейная логика появилась из анализа структуры и семантики интуиционистских доказательств; конкретно, из выделения «линейных» и «нелинейных» логических конструкций. С самого начала было предложено неформально интерпретировать доказательства линейной логики как линейные операторы над векторными пространствами. Тем не менее, несмотря на многие попытки, построить корректную семантику, основываясь на этой интуиции, не удавалось.

    Прогресс был достигнут в недавние годы, когда стало понятно, что необходимо рассматривать категории частично упорядоченных векторных пространств. Т.Эрар и Л.Ренье, наконец, построили корректную невырожденную модель всей пропозициональной линейной логики (а не какого-то отдельного фрагмента), в принципе допускающую описание в терминах некоторых, довольно специфических, частично упорядоченных векторных пространств и положительных линейных операторов.

    Развивая это направление, мы предлагаем существенно более богатую и, возможно, более прозрачную модель линейной логики, построенную непосредственно из естественных конструкций над частично упорядоченными векторными пространствами достаточно общего вида.

  94. 2018.03.29: Симплициальная семантика предикатных модальных логик (продолжение)
    Докладчик: Шехтман В.Б.
  95. 2018.03.22: Симплициальная семантика предикатных модальных логик
    Докладчик: Шехтман В.Б.
    Аннотация. Симплициальная семантика была введена Д.П.Скворцовым в начале 1990-х гг. как обобщение семантики Крипке (которая во многих случаях оказывается неадекватной). В докладе будет дан краткий обзор определений и основных теорем и доказан недавний результат о неполноте. Материал частично совпадает с докладом в МИАН осенью 2017 г., но часть о неполноте будет новой.
  96. 2018.03.15: Циклические выводы для эквациональной теории алгебр Клини (продолжение)
    Докладчик: Кузнецов С.Л.
  97. <!--
  98. 2018.03.08: Семинара не было.
  99. -->
  100. 2018.03.01: Циклические выводы для эквациональной теории алгебр Клини
    Докладчик: Кузнецов С.Л.
    Аннотация. Будет рассказано об исчислении в гиперсеквенциальном формате с нефундированными выводами, задающем эквациональную теорию алгебр Клини (в сигнатуре, содержащей операции умножения, аддитивной дизъюнкции и итерации Клини). Для этой системы доказано, что её фрагмент с циклическими (регулярными) выводами, не содержащими правило сечения, задаёт ту же самую теорию.

    По статье:
    A. Das, D. Pous. A cut-free cyclic proof system for Kleene algebra. Proc. TABLEAUX '17, LNCS/LNAI vol. 10501.

  101. 2018.02.22: О некоторых свойствах моделей эпистемической логики свидетельств
    Докладчик: Крупский В.Н.
    Аннотация. Аксиоматизируются свойства таких моделей — функциональность (свидетель подтверждает не более одной формулы) и строгость (произведение свидетелей в точности соответствует применению Modus Ponens).
  102. <!--
  103. 2018.02.15: Семинара не было, Планировал С.Одинцов, но не смог выступить из-за болезни. Планировавшаяся тема: О конструктивных версиях теоретико-игровой семантики: логика первого порядка и логика Хинтикки
  104. -->
    осень 2017
  105. 2017.12.14: Временные логики с топологической модальностью (продолжение)
    Докладчик: Шехтман В.Б.
  106. 2017.12.07: Временные логики с топологической модальностью
    Докладчик: Шехтман В.Б.
    Аннотация. Мы рассмотрим логики линейного времени со стандартными связками «всегда будет» и «всегда было», к которым добавляется топологическая S4-модальность «локальной истинности». Будет построена аксиоматика и доказана финитная аппроксимируемость таких логик для класса всех линейных порядков и для рациональной прямой. Будет дан краткий обзор дальнейших результатов и проблем в этой области.
  107. 2017.11.30: Предтранзитивные логики конечной глубины (продолжение)
    Докладчик: Кудинов Андрей Валерьевич
  108. 2017.11.23: Предтранзитивные логики конечной глубины
    Докладчик: Кудинов Андрей Валерьевич
    Аннотация. Одной из самых известных нерешенных проблем модальной логики является следующая: является ли разрешимой логика, задаваемая аксиомой &Square;&Square;p → &Square;&Square;&Square;p. Эта аксиома задает понятное первопорядковое свойство R3 &subseteq; R2. В общем случае можно рассматривать формулы вида &Square;mp → &Square;np для m < n. Такие формулы задают логики, которые часто называют предтранзитивными, т.к. в них выразимо транзитивное замыкание, т.е. существует формула A(p) такая, что для любой формулы B, любой модели M и ее точки x имеем: M,x&models;A(B) ⇔ формула B истинна во всех точках, достижимых из x по отношению R за конечное число шагов. Каноничность таких формул легко проверяется, а вот стандартные способы доказательства финитной аппроксимируемости (и, как следствие, разрешимости) проходят только для случая, когда m = 1; для случая же m > 1 ни финитная аппроксимируемость, ни разрешимость до сих пор не известна. В нашей совместной работе с И. Шапировским мы сделали небольшой шаг в направлении решения этой проблемы. Мы доказали, что если взять любую из упомянутых аксиом и добавить аксиомы, соответствующие тому, что глубина транзитивного замыкания отношения не превосходит данного k (для логики S4 такие формулы давно известны из работ Сегерберга и Максимовой; мы берем те же формулы, но для транзитивного замыкания), то полученная логика будет финитно аппроксимируемой и разрешимой.

    Я расскажу про постановку задачи, известные результаты и изложу метод фильтрации с помощью последовательных разбиений, который мы развили. Этот метод может оказаться полезным и для других логик.

  109. <!--
  110. 2017.11.16: Семинара не было. Вместо него был доклад Silvio Ghilardi "Interpolation, Amalgamation and Combination" в среду 15.11.2017 на кафедральном семинаре
  111. -->
  112. 2017.11.09: Реконструкция модального аргумента Гёделя (продолжение)
    Докладчик: Красненкова Анастасия Владимировна (канд. филос. наук; бакалавриат мехмата, науч. рук. В.Н.Крупский)
  113. 2017.11.02: Реконструкция модального аргумента Гёделя
    Докладчик: Красненкова Анастасия Владимировна (канд. филос. наук; бакалавриат мехмата, науч. рук. В.Н.Крупский)
    Аннотация. В докладе будет проанализирована реконструкция так называемого онтологического аргумента Геделя, проведенная в системе интерактивных доказательств Coq К.Бенцмюллером и Б.Палео. Будут также рассмотрены тактики Coq, позволяющие работать в системе модальной логики.
  114. 2017.10.26: О сложности аналитических функций нескольких переменных
    Докладчик: Белошапка Валерий Константинович, профессор, кафедра ТФФА.
    Аннотация. В математическом анализе, как и в дискретной математике, есть круг вопросов, связанных с оценками сложности объектов. Или, другими словами, вопросы о возможности выразить функции некоторого класса с суперпозициями функций другого, более узкого класса. В анализе этот круг вопросов связан с именами Э. Галуа, Ж. Лиувилля, Д. Гильберта, А. Островского, А. Н. Колмогорова, В. И. Арнольда, А. Г. Витушкина. Докладчик планирует рассказать о своем подходе к задаче оценки сложности аналитических функций нескольких переменных, о недавно полученных результатах, о связях и аналогиях с другими областями математики, о возникающих в этой задаче конструкциях и о стоящих на этом пути проблемах.
  115. <!--
  116. 2017.10.19: Семинара не было в связи с проведением Wormshop 2017 в МИАН.
  117. -->
  118. 2017.10.12: Неразрешимость интуиционистской логики предикатов в языке с одной одноместной предикатной буквой и двумя предметными переменными
    Докладчик: Рыбаков Михаил Николаевич (Тверской государственный университет)
    Аннотация.
    1. Техническая часть доклада.
    Известно, что интуиционистская логика в языке с двумя предметными переменными неразрешима. Будет показано, что этот результат можно получить при дополнительных ограничениях на язык: когда используются только позитивные формулы от одноместных предикатных букв. Далее будет показано, как все одноместные буквы позитивных формул промоделировать одной одноместной буквой (тоже с использованием лишь позитивных формул). Таким образом, будет представлен результат о неразрешимости позитивного фрагмента интуиционистской логики предикатов в языке с одной одноместной предикатной буквой и двумя предметными переменными.

    2. Дискуссия.
    Предполагается обсудить возможность перенесения результата на бесконечные классы модальных и суперинтуиционистских логик, а также суперинтуиционистских фрагментов расширений логики QK4. Кроме того, предполагается обсудить возможность получения аналогичных результатов для логик классов конечных моделей (но уже связанных с неперечислимостью).

  119. 2017.10.05: Насыщенность и компактность в модальной логике (продолжение)
    Докладчик: Золин Е.Е.
    Аннотация. Данный доклад является продолжением предыдущего, тем не менее докладчик постарается сделать его максимально независимым от уже рассказанного. В новом докладе речь пойдёт о применениях понятий насыщенной модели и компактного класса моделей для получения некоторых классических результатов, среди которых — теорема ван Бентема о бисимуляции, теорема о критерии определимости.
  120. 2017.09.28: Насыщенность и компактность в модальной логике
    Докладчик: Золин Е.Е.
    Аннотация. Будет рассказываться, как понятия насыщенности и компактности позволяют получать различные результаты в модальной логике, в частности, критерии определимости классов структур.
  121. весна 2017
  122. 2017.05.25: Критерии определимости в модальной логике
    Докладчик: Золин Е.Е.
    Аннотация. В математической логике фундаментальную роль играют результаты, характеризующие выразительные возможности того или иного языка. Выразимость бывает «внутренней» (какие отношения выразимы формулами данного языка через имеющиеся отношения в конкретной структуре) или «внешней», для которой чаще используется термин «определимость» (какие классы структур можно задать средствами изучаемого языка). В докладе пойдет речь о внешней выразимости, причем мы будем трактовать слова «задать средствами» несколькими способами (среди них: задать одной формулой, задать множеством формул, а также другие трактовки, выстраивающиеся вместе с указанными двумя в естественную — и довольно простую — иерархию). Классическими результатами этого типа являются теорема Биркгофа, характеризующая классы алгебр, задаваемых множеством тождеств; теорема Кейслера, характеризующая классы моделей первого порядка, задаваемых множеством предложений элементарного языка; теорема Голдблатта – Томасона, характеризующая (элементарные) классы шкал Крипке, задаваемые множеством модальных формул. Будет дан обзор критериев определимости (включая полученные недавно докладчиком) для различных языков (первого порядка и модальных, акцентом на последних) и структур (моделей первого порядка, моделей Крипке, шкал Крипке).
  123. 2017.05.18: О двух типах ультрарасширений моделей первого порядка и их обобщения
    Докладчик: Савельев Денис Игоревич, ИППИ РАН.
    Аннотация. Известны два типа расширения моделей первого порядка ультрафильтрами, короче, ультрарасширения моделей, оба в определённом смысле канонические. Один из них [1] происходит из модальной логики и универсальной алгебры и фактически восходит к классической работе [2]. Другой [3, 4] происходит из теории моделей и алгебры ультрафильтров с ультрарасширениями полугрупп [5] в качестве главного предшественника.

    Классическим в общей топологии является тот факт, что пространство ультрафильтров над дискретным пространством есть его наибольшая компактификция. Основной результат работ [3, 4], подтверждающий каноничность данного типа расширения, обобщает этот факт на дискретные пространства, снабжённые структурой первого порядка. Аналогичный результат для первого типа ультрарасширения был получен в [6].

    В настоящем докладе предлагается однородный подход к обоим типам расширений. Он основан на идее расширить саму операцию расширения. Далее предлагается обобщение стандартного понятия модели первого порядка, в котором функциональные и предикатные символы интерпретируются как ультрафильтры над множествами функций и отношений, а не индивидуальные функции и отношения. Построены две операции специального вида, превращающие обобщённые модели с носителями, состоящими из ультрафильтров, в обычные модели с теми же носителями, и установлены необходимые и достаточные условия для того, чтобы эти последние модели оказались ультрарасширениями двух канонических типов каких-то моделей. Доклад основан на недавней совместной работе с Н.Л. Поляковым.

    Литература

    [1] V. Goranko. Filter and ultrafilter extensions of structures: universal-algebraic aspects. Preprint, 2007.
    [2] B. Jonsson, A. Tarski. Boolean algebras with operators. Part I: Amer. J. Math., 73:4 (1951), 891-939. Part II: ibid., 74:1 (1952), 127-162.
    [3] D.I. Saveliev. Ultrafilter extensions of models. Lecture Notes in AICS 6521 (2011), 162-177.
    [4] D.I. Saveliev. On ultrafilter extensions of models. In: S.-D. Friedman et al. (eds.). The Infinity Project Proc. CRM Documents 11, Barcelona, 2012, 599-616.
    [5] N. Hindman, D. Strauss. Algebra in the Stone-Cech compactification. 2nd ed., revised and expanded, W. de Gruyter, Berlin-N.Y., 2012.
    [6] D.I. Saveliev. On canonicity of the larger ultrafilter extension. Preprint, 2014.

  124. 2017.05.11: Вторая теорема Гёделя о неполноте для теорий с функцией пары
    Докладчик: Пахомов Фёдор Николаевич, к.ф.-м.н., МИАН, науч. рук. Л.Д.Беклемишев.
    Аннотация. Для доказательства своих знаменитых теорем о неполноте Курт Гёдель разработал формализацию в арифметических терминах понятий формального языка и доказуемости. Дальнейшие исследования показали, что вместо использования явной формализации понятия доказуемости, как это делал Гёдель, можно доказать теорему для всех формализаций, удовлетворяющих небольшому набор условий (условия Гильберта – Бернайса – Лёба на предикат доказуемости), которому, фактически, удовлетворяют все «адекватные» формализации понятия доказуемости.

    В этом докладе будет рассказано о похожем подходе к замене явно сформулированной гёделевой нумерации на любую формализацию понятия формального языка данной теории, удовлетворяющую небольшому набору естественных условий. Обычно первопорядковый язык данной сигнатуры задается естественным индуктивным определением, определяемым набором правил образования новых формул из уже имеющихся. Для каждой теории T мы формулируем первопорядковую теорию Syn(T), объектами которой являются формулы языка теории T и аксиомы которой отражают индуктивное определение множества всех формул языка теории T. Мы доказываем лемму о неподвижной точке для всех теорий T, которые интерпретируют теорию Syn(T). Тем самым, во всех таких теориях T проходит стандартное доказательство второй теоремы Гёделя для любых предикатов, удовлетворяющих условиям Гильберта – Бернайса – Лёба.

    Отметим, что наш подход оказывается применим к теориям менее выразительным, чем арифметические теории со сложением и умножением, в которых представимы все вычислимые функции. В частности, лемма о неподвижной точке доказуема для полной и разрешимой элементарной теории Th(ℕ,C) натуральных чисел с канторовской функцией пары C(m,n)=(m+n)/(m+n+1)/2+m. Кроме того будет рассказано о связи между наличием в теории адекватных формализаций понятия доказуемости и её неразрешимостью.

  125. <!--
  126. 2017.05.04: Семинара не было.
  127. -->
  128. 2017.04.27: Некоторые теоремы полноты для модальных логик предикатов (продолжение)
    Докладчик: Шехтман В.Б.
  129. 2017.04.20: Некоторые теоремы полноты для модальных логик предикатов
    Докладчик: Шехтман В.Б.
    Аннотация. Будет доказана полнота в семантике Крипке для предикатной модальной логики с аксиомами транзитивности и плотности. При этом для построения нужной контрмодели используется игровой метод. Тем же методом можно упростить доказательства результатов Корси (1993) о полноте модальных предикатных логик плотных линейных порядков с переменными областями. Вкратце будет сказано и о других применениях.
  130. <!--
  131. 2017.04.13: Семинара не было.
  132. --> <!--
  133. 2017.04.06: Обзорная лекция о теории доказательств, модальной логике и матлингвистике. Дополнение ко (второй?) встрече со студентами 2-го курса.
  134. -->
  135. 2017.03.30: О временных модальных логиках интервалов над ℚ и ℝ. Финитная аппроксимируемость, сложность и описание класса конечных шкал
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
    Аннотация. За последние 10 лет были получены результаты о (не)разрешимости более 90% модальных интервальных логик над линейными порядками. Значительная часть результатов относится к работам В.Горанко, А.Монтанари, В.Б.Шехтмана и др. Однако, вопрос о прочих свойствах логик, таких как финитная аппроксимируемость, алгоритмическая сложность, описание класса конечных шкал и т.д. для многих интервальных логик остается открытым.

    В настоящей работе рассматриваются временные шкалы интервалов над рациональным и вещественным числами с отношением «ранее». Методом фильтрации канонической модели и построением p-морфизмов на конечные шкалы получена финитная аппроксимируемость соответствующих модальных логик. Также в работе явно описаны классы конечных шкал, соответствующих этим логикам, откуда следует NP-сложность задачи выполнимости.

  136. 2017.03.23: Перевод традиционной негативной силлогистики в модальную логику
    Докладчик: Красненкова Анастасия Владимировна (канд. филос. наук; бакалавриат мехмата, науч. рук. В.Н.Крупский)
    Аннотация. Рассматривается формальная система традиционной негативной силлогистики NTS. Предложена ее точная модальная формулировка и установлено, что проблема выводимости в NTS является NP-полной.
  137. <!--
  138. 2017.03.16: Семинара не было. Готовились ко встрече со студентами 17 марта.
  139. -->
  140. 2017.03.09: Некоммутативные расширения линейной логики (продолжение)
    Докладчик: Славнов Сергей Андреевич, к.ф.-м.н., ВШЭ.
  141. 2017.03.02: Некоммутативные расширения линейной логики
    Докладчик: Славнов Сергей Андреевич, к.ф.-м.н., ВШЭ.
    Аннотация. Еще в конце прошлого века было известно, что мультипликативную линейную логику можно расширить добавлением некоммутативной самодвойственной двуместной связки. Первую такую систему, Pomset logic, определил Кристиан Реторе, написав для нее денотационную семантику и синтаксис proof-nets. Через некоторое время для этой же связки была придумана система глубокого вывода BV. Предполагается, что системы эквивалентны, но это так и не доказано. Также, для этой связки до сих пор не удавалось построить исчисления секвенций с устранением сечения.

    Мы вводим новое расширение, в котором некоммутативных связок две, и они двойственны друг другу. Мы затем исследуем вариации этой системы, и получаем еще два «вырожденных» расширения, одно из которых идентифицируется как Pomset logic Реторе. Для всех трех получившихся систем пишется синтаксис proof-nets и исчисление секвенций с устранением сечения.

  142. <!--
  143. 2017.02.23: Праздничный день.
  144. -->
    осень 2016
  145. 2016.12.15: Biabduction (and related problems) in Array Separation Logic
    Докладчик: Max Kanovich (Канович Макс Иосифович), Professor of Computer Science, University College London
    Abstract. In the last 15 years, separation logic has evolved from a novel way to reason about memory pointers to a mainstream technique for scalable program verification.

    We investigate Array Separation Logic, a variant of symbolic-heap separation logic, in which the primary data structures are not lists, but similarly ubiquitous data structures for imperative programming, namely pointers and arrays, i.e., contiguously allocated blocks of memory. This logic can be seen as a language for compositional proof of memory safety for array-manipulating imperative programs.

    We focus on the biabduction problem for this logic, which has been established as the key to automatic specification inference at the industrial scale in the setting of standard separation logic, in particular, by digging information out of bare code.

    Specifically, we show that the problem of finding a consistent solution is NP-complete, and we present a concrete NP algorithm for biabduction that produces solutions of reasonable quality.

    Along the way, we show that satisfiability in our logic is NP-complete, and that entailment is decidable with high complexity. The somewhat surprising fact that biabduction is computationally simpler than entailment is explained by the fact that, as we show, the element of choice over biabduction solutions enables us to drastically reduce the search space.

    This is joint work with James Brotherston and Nikos Gorogiannis.

    No programming knowledge is required.

  146. <!--
  147. 2016.12.08: Семинара не было.
  148. -->
  149. 2016.12.01: О связи IF-логики Хинтикки и реализуемости по Нельсону (по совместной работе с С.П.Одинцовым и И.Ю.Шевченко)
    Докладчик: Сперанский Станислав Олегович, к.ф.-м.н., доцент, СПбГУ.
    Аннотация. В своей книге “The Principles of Mathematics Revisited” Хинтикка обсуждает одну логику с обобщёнными кванторами, так называемую IF-FOL (сокр. от англ. independence-friendly first-order logic), и то, как сильно изменилась бы ситуация в философии математики, если классическую FOL заменить на IF-FOL. Отчасти вдохновляясь идеями Хинтикки, связанными с конструктивизмом, мы собираемся «эффективизировать» теоретико-игровую семантику (сокр. GTS) для IF-FOL, однако наш подход будет несколько отличаться от того, что предлагал Хинтикка в своей книге. План таков:

    • Сначала будет показано, что реализуемость по Нельсону (которая расширяет хорошо известную реализуемость по Клини посредством добавления «сильного отрицания»), ограниченная на формулы без импликаций, может рассматриваться как эффективная версия GTS для FOL.

    • Затем мы определим некоторый вариант реализуемости для IF-FOL, вдохновляясь так называемой «трамп-семантикой» (которая была открыта Ходжесом), и покажем, что получающаяся «трамп-реализуемость» может рассматриваться как эффективная версия GTS для IF-FOL.

    • Наконец, будет показано, что наша трамп-реализуемость для IF-FOL подходящим образом обобщает ограниченную реализуемость по Нельсону для первопорядковых формул без импликаций.

    Мы также бегло коснёмся проблемы добавления импликации к IF-FOL.

  150. 2016.11.24: Закон «нуля или единицы» для случайных графов
    Докладчик: Кузнецов С.Л.
    Аннотация. Доклад будет посвящён одному результату (независимо полученному Глебским и др. (1969) и Фейгиным (1976)) на стыке теории вероятностей, математической логики и теории игр — закону «нуля и единицы». Формулируется он, в простейшем случае, так: для случайного графа в модели Эрдёша – Реньи с постоянной вероятностью ребра всякое утверждение о графе, выразимое на языке первого порядка, либо асимптотически почти наверное истинно, либо асимптотически почти наверное ложно. Ключевой момент в доказательстве — переход от истинности формул первого порядка к стратегиям в играх Эренфойхта на графах. Если останется время и энтузиазм слушателей, также будут намечены вариации этой теоремы, полученные Спенсером, Шелахом и недавно М. Жуковским.
  151. 2016.11.17: Инфинитарный оператор слабой необходимости
    Докладчик: Золин Е.Е.
    Аннотация. Модальные логики с оператором неслучайности (non-contingency; другое название — оператор разрешимости), означающим «необходимо A или необходимо не-А», изучались с конца 1960-х годов, однако лишь в 1995 году L.Humberstone и S.Kuhn построили первую полную аксиоматику логики этого оператора. Использованная ими для доказательства полноты модификация конструкции канонической модели мотивировала докладчика к введению так называемого «инфинитарного оператора слабой необходимости», выполняющего в данном доказательстве роль, близкую к роли оператора необходимости в обычной канонической модели. Таким образом, через оператор неслучайности был выражен некоторый оператор, по свойствам близкий (но не совпадающий) с исходным оператором необходимости.

    В докладе будет рассказано об обнаруженных свойствах этого оператора, о выразительных возможностях модального языка с данным оператором, а также об открытых вопросах в данной области, в частности, о проблеме построения полной аксиоматики логики инфинитарного оператора. Кроме того, будет обсуждаться и другой оператор, введенный Claudio Pizzi в 1999 году, также выраженный через оператор неслучайности, но уже не с помощью инфинитарного языка, а с помощью кванторов по пропозициональным переменным (модальной логики второго порядка).

  152. <!--
  153. 2016.11.03: Праздник.
  154. -->
  155. 2016.11.10: О моделировании знания в социальных сетях
    Докладчик: Крупский В.Н.
    Аннотация. Предлагается математическая модель формирования знания в социальных сетях. Соответствующие математические структуры оказываются моделями интуиционистской эпистемической логики IEL (С.Артемов, Т.Протопопеску, 2014), причем последняя оказывается полной в этом классе моделей. Это обстоятельство мотивирует более детальное исследования логики IEL.

    Мы устанавливаем ее PSpace-полноту и предлагаем для IEL эквивалентную секвенциальную формулировку без правила сечения. Поиск вывода в этом исчислении дает верхнюю оценку сложности, а соответствующая нижняя оценка следует из аналогичной оценки для интуиционистской логики высказываний.

  156. 2016.10.27: Intuitionistic Epistemic Logic
    Докладчик: Tudor Protopopescu (HSE, Moscow)
    Аннотация. Intuitionistic Epistemic Logic is the logic of constructive knowledge based on the Brouwer-Heyting-Kolmogorov (BHK) semantics for intuitionistic logic. Constructive knowledge is understood as the product of verification which is not necessarily strict proof. In contrast to classical logics of knowledge co-reflection, A → KA, is valid, while reflection, KA → A, is not. The former expresses the constructivity of truth; the latter claims that verifications yield strict proofs and is too strong as an expression of the truth condition for knowledge.

    We will consider the motivations for such an approach to knowledge and present the resulting system of Intuitionistic Epistemic Logic, IEL, as well as both Kripke models and provability models, via extensions of S4 and the Logic of Proofs with a verification modality. We will also look at how IEL gives natural intuitionistic responses to some epistemic puzzles, namely the Knowability Paradox and the Lottery Paradox.

  157. 2016.10.20: О расширении исчисления Ламбека с субструктурной модальностью и управляемой неассоциативностью
    Докладчик: Кузнецов С.Л. (по совместной работе с М.Кановичем и А.Щедровым)
    Аннотация. Доклад посвящён одному расширению исчисления Ламбека с тремя модальностями. Одна из них разрешает для помеченных ей формул некоторые структурные правила (сокращение и перестановку, но не ослабление); две другие позволяют расставлять в секвенции скобки, локально отменяющие правило ассоциативности. Этот вариант исчисления Ламбека мотивирован лингвистическими приложениями [Моррилл и Валентин 2015]. К сожалению, оказалось, что проблема выводимости для этого исчисления алгоритмически неразрешима. Будет рассказана схема доказательства неразрешимости, а также приведены разрешимые фрагменты этого исчисления, используемые на практике. Точная оценка алгоритмической сложности для наиболее интересных из этих фрагментов остаётся открытой задачей.
  158. 2016.10.13: О бесконечных выводах для логики Гжегорчика
    Докладчик: Саватеев Юрий Вячеславович, к.ф.-м.н., науч. рук. М.Р.Пентус.
    Аннотация. Известно, что для логики Гёделя – Лёба GL существует исчисление секвенций с циклическими выводами. В докладе мы предложим аналогичную конструкцию для логики Гжегорчика Grz.
  159. 2016.10.06: О сильной топологической полноте логики GL
    Докладчик: Шамканов Д. С., к.ф.-м.н., науч. рук. Л.Д.Беклемишев и В.Н.Крупский
    Аннотация. Известно, что логика Гёделя – Лёба GL является сильно полной относительно топологической семантики в случае локального отношения следования. В докладе мы обсудим связь между глобальным отношением семантического следования на классе разреженных топологических пространств и бесконечными выводами в логике GL.
  160. весна 2016
  161. 2016.05.19: Окрестностносные и топологические произведения модальных логик
    Докладчик: Кудинов Андрей Валерьевич
    Аннотация. В отличие от того, как это делается в классической топологии, произведение двух топологических пространств можно определить как битопологическое пространство с носителем — декартовым произведением носителей, «горизонтальной» топологией, в которой открытыми будут множества, у которых все горизонтальные сечения открыты в смысле первого пространства, и «вертикальной» топологией (определяется аналогично). Мы рассмотрим, какие получаются модальные логики произведений топологических пространств, если логики компонент произведений известны.

    Топологическую семантику возможно определить только для расширений модальной логики S4 (если мы интерпретируем модальность как оператор внутренности) или для расширений wK4 (если модальность интерпретируется как оператор взятия производного множества), тогда как аналогом топологической семантики для более слабых логик является окрестностная семантика. Мы рассмотрим описанную выше конструкцию и для окрестностной семантики и покажем, какие логики получается в этом, более общем, случае.

    Будет сделан обзор как известных, так и и новых, полученных докладчиком, результатов.

  162. 2016.05.12: Неразрешимое суперинтуиционистское исчисление с аксиомами от 3 переменных
    Докладчик: Боков Григорий Владимирович, к.ф.-м.н., кафедра МаТИС.
    Аннотация. Доказывается существование неразрешимого суперинтуиционистского исчисления с аксиомами от трех переменных. Это решает открытую проблему, поставленную А.В.Чагровым в 1994 году.
  163. <!--
  164. 2016.04.28: Семинара не было.
  165. -->
  166. 2016.04.21: Логика свидетельств для логики с модальностью транзитивного замыкания
    Докладчик: Шамканов Д. С.
    Аннотация. В этот раз планируется обсудить логику свидетельств, соответствующую модальной логике с модальностью транзитивного замыкания K+.
  167. 2016.04.14: Теорема о реализации для логики доказуемости Гёделя-Лёба (продолжение)
    Докладчик: Шамканов Д. С.
  168. 2016.04.07: Теорема о реализации для логики доказуемости Гёделя-Лёба
    Докладчик: Шамканов Д. С.
    Аннотация. Мы рассматриваем новую логику свидетельств, связанную с логикой доказуемости Гёделя-Лёба GL, и устанавливаем теорему о реализации логики GL в нашей системе, привлекая исчисление секвенций с так называемыми циклическими выводами.
  169. 2016.03.31: Алгоритмическая статистика и её приложения
    Докладчик: Милованов Алексей Сергеевич, асп. 2-го года, науч. рук. Н.К.Верещагин.
    Аннотация. В 1974 году Колмогоров предложил использовать алгоритмическую теорию информацию для измерения качества статистических гипотез. Эта идея превратилась в науку, которая сейчас называется «Алгоритмическая статистика». Важным понятием алгоритмической статистики являются нестохастические слова, т.е. такие объекты, для которых не существует «хорошего» объяснения в смысле Колмогорова. Они изучались в работах А.Шеня, П.Витании, Н.К.Верещагина и других.

    Докладчик попытается рассказать о чужих и своих результатах по данной теме. В частности будут затронуты темы приложения алгоритмической статистики в теории кодирования и задаче предсказания.

  170. 2016.03.24: О клоновом подходе к математическим проблемам теории коллективного выбора
    Докладчик: Поляков Николай Львович (Финансовый университет при Правительстве РФ)
    Аннотация. Наиболее известные результаты теории коллективного выбора (social choice theory) — это так называемые теоремы о невозможности, первой из которых была хорошо известная теорема (парадокс) Эрроу. Эти теоремы утверждают, что не существует правил агрегирования, которые сохраняют некоторые множества систем индивидуальных предпочтений и удовлетворяют некоторым естественным условиям. С.Шелах показал (2005), что при некоторых ограничениях каждое симметричное множество систем предпочтений обладает свойством Эрроу. Под системой предпочтений в работе Шелаха понимается произвольная r-функция выбора, т.е. функция выбора, определенная на множестве всех r-элементных подмножеств конечного множества альтернатив для некоторого натурального числа r.

    Нам удалось снять эти ограничения и построить полную классификацию симметричных множеств r-функций выбора, обладающих свойством Эрроу. Оказывается, рассматриваемая задача хорошо формулируется на языке соответствий Галуа для классов дискретных функций, что позволяет воспринимать теорему Шелаха и полученное нами усиление как новые результаты теории функционально замкнутых классов. Промежуточным результатом в доказательстве усиленной версии теоремы Шелаха о свойстве Эрроу явилась простая теорема о классификации симметричных квазитривиальных (консервативных) клонов с конечным носителем.

  171. 2016.03.10: Доказательство гипотезы Виссера-Зутхаута об интерпретациях арифметики Пресбургера в себя (продолжение)
    Докладчик: Запрягаев Александр Александрович, студ. 4-го курса, научный руководитель Л. Д. Беклемишев
  172. 2016.03.10: Доказательство гипотезы Виссера-Зутхаута об интерпретациях арифметики Пресбургера в себя
    Докладчик: Запрягаев Александр Александрович, студ. 4-го курса, научный руководитель Л. Д. Беклемишев
    Аннотация. Альберт Виссер предложил рассмотреть вопрос описания всех одномерных интерпретаций без параметров арифметики Пресбургера в себя и выдвинул гипотезу о том, что все такие интерпретации доказуемо изоморфны тождественной, что влечёт также невозможность интерпретировать арифметику Пресбургера ни в одной из своих конечно аксиоматизируемых подтеорий. Будет представлено полученное автором доказательство гипотезы Виссера–Зутхаута. Функция, осуществляющая изоморфизм интерпретации арифметики Пресбургера в себя тождественной, будет построена, согласно идее к.ф.-м.н. Ф.Н.Пахомова, на основе анализа интерпретированного отношения порядка. Также будет продемонстрирована неожиданная связь с задачей Улама — Коллатца о последовательности «3n+1».
  173. 2016.03.03: Абстрактные варианты второй теоремы Гёделя о неполноте для логик слабее классической (продолжение)
    Докладчики: Беклемишев Л.Д., Шамканов Д.С.
  174. 2016.02.25: Абстрактные варианты второй теоремы Гёделя о неполноте для логик слабее классической
    Докладчики: Беклемишев Л.Д., Шамканов Д.С.
    Аннотация. В докладе приводятся варианты условий Гильберта–Бернайса–Леба, работающие в очень общих предположениях относительно рассматриваемой логики. Также исследуется роль правил сокращения и ослабления для вывода второй теоремы Гёделя и строится игрушечный пример формальной системы, основанный на модальной логике типа K4 без правила сокращения, опровергающий формализованный вариант этой теоремы.
  175. осень 2015
  176. 2015.12.10: О полноте модальных логик, расширенных модальностью транзитивного замыкания
    Докладчик: Золин Е.Е., к.ф.-м.н., с.н.с.
    Аннотация. Доклад по совместной работе с И.Б.Шапировским. Известны аксиомы Сегерберга, которые при добавлении к модальной логике K дают полную по Крипке логику K+ с двумя модальностями: одной &Square;, отвечающей произвольному отношению R, и другой &boxplus;, отвечающей ее транзитивному замыканию R+. Возникает естественный вопрос: если аксиомы Сегерберга добавлять к произвольной (полной) модальной логике L, то в каких случаях получится полная по Крипке бимодальная логика L+? В докладе будут приведены найденные недавно (2015) достаточные условия на логику L, гарантирующие полноту логики L+. Данные условия являются довольно сильными (что сужает их область применимости) и гарантируют не только полноту, но и разрешимость, и финитную аппроксимируемость логики L+. Будет рассказано также о новом результате о достаточном условии полноты логики вида PDL(Φ), где Φ — некоторое множество полимодальных формул. Будут обсуждаться открытые вопросы в этой области.
  177. 2015.12.03: Полиномиальный алгоритм для формул ограниченной глубины в мультипликативной некоммутативной линейной логике (продолжение)
    Докладчик: Пентус М.Р.
  178. 2015.11.26: Полиномиальный алгоритм для формул ограниченной глубины в мультипликативной некоммутативной линейной логике
    Докладчик: Пентус М.Р.
    Аннотация. По статье: Pentus M. A polynomial-time algorithm for Lambek grammars of bounded order // Linguistic Analysis. — 2010. — Vol. 36, no. 1-4. — P. 441-471.
  179. 2015.11.19: Гибридные модальные логики
    Докладчик: Вахрушева Полина Викторовна, аспирантка, научный руководитель В.Б.Шехтман
    Аннотация. Краткий обзор–введение по гибридным логикам. Доклад основан на главе “Hybrid Logics” авторов Carlos Areces, Balder ten Cate из книги “Handbook of Modal Logic”. Будет приведена аксиоматика основных гибридных логик и доказаны некоторые теоремы о полноте.
  180. 2015.11.12: Итерации медленной непротиворечивости
    Докладчик: Пахомов Ф.Н., к.ф.-м.н., МИАН
    Аннотация. Рекурсивно аксиоматизируемые теории можно сравнивать по силе утверждения о их непротиворечивости Con(T). Хотя имеется ряд контрпримеров, но в случае «естественных» теорий T и U почти всегда оказывается, что либо примитивно рекурсивная арифметика PRA доказывает, что Con(T) влечет Con(U), либо PRA доказывает, что Con(U) влечет Con(T), либо PRA доказывает эквивалентность этих утверждений. Тем самым такое сравнение для «естественных» теорий оказывается линейным.

    С точки зрения этого линейного порядка, над арифметикой Пеано PA имеется «естественная» «немного более сильная» теория PA+Con(PA). Но, как оказывается, между этими двумя теориями имеются промежуточные по силе теории.

    Так, С. Фридманом, М. Ратьеном и А. Вайерманом был предложен следующий, относительно «естественный», пример теории в этом промежутке. Как известно, теория PA является объединением конечно аксиоматизируемых теорий n (PA со схемой индукции для Σn-формул) по всем натуральным n. Кроме того, хорошо известен ряд примеров быстрорастущих общерекурсивных функций, чья всюду определенность недоказуема в PA. Рассмотрим одну из них — функцию Fε0. Теперь рассмотрим альтернативный метод перечисления аксиом PA, а именно метод, при котором аксиомы теории n появляются на шаге Fε0(n). Как оказывается, PA не может доказать эквивалентность этой аксиоматизации и стандартной, а утверждение Con(PAs) о «медленной» непротиворечивости PA (то есть непротиворечивости теории, задаваемой этим альтернативным методом перечисления аксиом) оказывается слабее обычного Con(PA).

    Таким образом, теория PA+Con(PAs) оказывается промежуточной по силе между PA и PA+Con(PA). Более того, С. Фридманом, М. Ратьеном и А. Вайерманом было показано, что PA доказывает, что для всех формул φ имеет место эквивалентность &lozenge;&lozenge;sφ ↔ &lozenge;φ, где &lozenge;φ означает Con(PA+φ), а &lozenge;sφ означает Con(PAs+φ). Из этого, в частности, следует, что PA доказывает, что для всех φ и натуральных n имеет место импликация (&lozenge;s)nφ → &lozenge;φ. Тем самым, все конечные итерации добавления к PA утверждений о «медленной» непротиворечивости дают более слабые теории, чем PA+Con(PA).

    В докладе рассказывается о следующем результате: PA доказывает, что для всех φ имеет место эквивалентность (&lozenge;s)ε0φ ↔ &lozenge;φ. Отметим, что отсюда непосредственно следует, что трансфинитные итерации добавления к PA утверждений о «медленной» непротиворечивости дают в зазоре между PA и PA+Con(PA) цепь теорий возрастающей силы длины в точности ε0.

    Кроме того, будет рассказано о том, что при замене в определении оператора ε0 функции Fε0 на другие подходящие функции можно получать эквивалентности (&lozenge;s)αφ ↔ &lozenge;φ для α=2 и α=ω.

  181. 2015.11.05: О канонических ультрарасширениях отношений и их топологических характеристиках (продолжение)
    Докладчик: Савельев Денис Игоревич, ИППИ РАН.
  182. 2015.10.29: О канонических ультрарасширениях отношений и их топологических характеристиках
    Докладчик: Савельев Денис Игоревич, ИППИ РАН.
    Аннотация. Известны два способа расширить данное двухместное отношение на множестве X до двухместного отношения на множестве βX, состоящем из ультрафильтров над X. Один способ появился в 70-е гг. в работе Леммона и Скотта по модальной логике, другой — несколько лет назад в работе докладчика по теории моделей. Оба способа являются в определённом смысле каноническими. В докладе будет обсуждаться их соотношение, их взаимодействие с операциями алгебры отношений, а также будут сформулированы их топологические характеристики. Один тип характеристик будет дан в терминах стандартной бикомпактной топологии на множестве βX ультрафильтров над X, другой — в терминах топологии Вьеториса на множестве замкнутых подмножеств в βX, которое можно отождествить с множеством фильтров над X.
  183. 2015.10.22: О некоторых интервальных временных модальных логиках. Разрешимость, финитная аппроксимируемость (продолжение)
  184. 2015.10.15: О некоторых интервальных временных модальных логиках. Разрешимость, финитная аппроксимируемость
    Докладчик: Чижов Алексей Сергеевич, аспирант ИППИ, научный руководитель В.Б.Шехтман
  185. 2015.10.08: Исчисление Ламбека с (суб)экспоненциальными модальностями (по совместной работе с А. Щедровым и М. Кановичем)
    Докладчик: Кузнецов С.Л., к.ф.-м.н., асс.
    Аннотация Исчисление Ламбека можно рассматривать как вариант некоммутативной линейной логики. Линейная логика имеет также одноместную связку, называемую экспоненциальной, выделяющую формулы, для которых в исчисление добавлены структурные правила (перестановка, сокращение, ослабление), которые не разрешены для произвольных формул. В докладе рассматриваются способы расширения исчисления Ламбека экспоненциальной модальностью с сохранением (не формально, а по существу) «ламбекова ограничения»: левая часть любой секвенции должна быть непустой. Рассматривается также субэкспоненциальная модальность, для которой разрешены только перестановка и сокращение, но не ослабление. Для предлагаемых расширений строятся исчисления генценовского типа и доказывается неразрешимость проблемы выводимости.
  186. 2015.10.01: Исчисление Ламбека с дополнительными аксиомами (по статье В. Бушковского) (продолжение)
  187. 2015.09.24: Исчисление Ламбека с дополнительными аксиомами (по статье В. Бушковского)
    Докладчик: Кузнецов С.Л., к.ф.-м.н., асс.
    Аннотация. Будет изложено доказательство следующего факта: любое перечислимое множество слов, не содержащее пустого слова, порождается некоторой категориальной грамматикой, основанной на исчислении Ламбека с одной операцией деления, расширенном конечным набором дополнительных аксиом специального, весьма простого вида. Отсюда, в частности, следует существование такого расширения исчисления Ламбека с неразрешимой проблемой выводимости. Для сравнения, проблема выводимости в самом исчислении Ламбека с одной операцией деления разрешима за полиномиальное время [Саватеев 2008], а основанные на нём грамматики порождают только контекстно-свободные языки [Пентус 1992].

    Доклад основан на статье W. Buszkowski. Some decision problems in the theory of syntactic categories. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 28:539-548, 1982.

  188. весна 2015
  189. 2015.05.14: Interpretability Suprema for Interpretability Logic ILM
    Speaker: Paula Henk (ILLC, University of Amsterdam)
    Abstract. The relation of relative interpretability can be seen as a definition of what it means for one theory to be stronger than another one. A collection of finite extensions of Peano Arithmetic (PA) that are equally strong in this sense is called a degree. The collection of all degrees (together with the relation of interpretability) is a distributive lattice.

    We want to use modal logic to investigate what is provable in PA about the lattice of its interpretability degrees. Part of the answer is provided by the interpretability logic ILM. However, the existence of the supremum in the lattice of interpretability degrees is not expressible in ILM. In order to eliminate this deficiency, we want to add to ILM a new modality. As it turns out, a certain unary modality is sufficient for this purpose. The dual of this unary modality satisfies the axioms of the provability logic GL. It can be seen as a nonstandard provability predicate. We explore the bimodal logic that results when adding to GL a unary modality for such a nonstandard provability predicate.

  190. 2015.05.07: О неразрешимости проблем распознавания для пропозициональных исчислений
    Докладчик: Боков Григорий Владимирович, к.ф.-м.н., м.н.с. кафедры МаТИС.
    Аннотация. В докладе будут рассмотрены следующие проблемы распознавания для пропозициональных исчислений с правилами вывода modus ponens и подстановки: распознавание аксиоматизации, распознавание расширения и распознавание полноты. В частности, будет доказано, что проблема распознавания расширения алгоритмически неразрешима для любого непустого исчисления, а проблемы распознавания аксиоматизации и полноты алгоритмически неразрешимы для любого исчисления, в котором выводима формула x → ( y → x ). Кроме того, в докладе будет приведён исторический обзор известных результатов по данной тематике.
  191. 2015.04.23: О реализации модальности в системе Coq
    Докладчик: Крупский В.Н.
    Аннотация. По работе Christoph Benzmuller & Bruno Woltzenlogel Paleo "Interacting with Modal Logics in the Coq Proof Assistant" (CSR 2015).
  192. 2015.04.09: О категорных моделях квантовой механики, связанных с линейной логикой
    Докладчик: Запрягаев Александр Александрович, студ. 3-го курса, научный руководитель Л. Д. Беклемишев
    Аннотация. В настоящем докладе обсуждается возможность применения аксиоматического подхода к квантовым вычислениям и алгоритмам. Даётся обзор классического подхода в терминах гильбертовых пространств (по Дж. фон Нойману) и устанавливается его ключевой результат — протокол квантовой телепортации. После обсуждения недостатков подобной модели и предлагается новый подход (S. Abramsky / B. Coecke, 2003), базирующийся на идеях современной теории категорий. Рассматриваются как формально-аксиоматический подход, так и метод диаграмм, позволяющий изображать квантовые протоколы в виде наглядных рисунков и являющийся мощным средством нахождения новых протоколов и доказательства тождеств о квантовых системах.
  193. 2015.XX.XX: Несеквенциальное исчисление Ламбека с двумя делениями
    Докладчик: Луговая Валентина Николаевна, Рыжова Анастасия Александровна, студ. 4-го курса, науч. рук. С.Л.Кузнецов.
    Аннотация. Исчисление L было введено И. Ламбеком для описания синтаксиса естественных языков. Это исчисление существует в двух вариантах — секвенциальном (генценовском) и несеквенциальном (гильбертовском). В исчислении Ламбека используются три связки — умножение, левое и правое деления. Естественный интерес представляет фрагмент исчисления Ламбека без операции умножения. В докладе предъявляется гильбертовское исчисление для этого фрагмента и доказывается его эквивалентность генценовскому исчислению.
  194. 2015.03.26: Лексикографические произведения и суммы модальных логик (продолжение)
    Докладчик: Шапировский И.Б.
  195. 2015.03.19: Лексикографические произведения и суммы модальных логик
    Докладчик: Шапировский И.Б.
    Аннотация. Мы будем рассматривать две естественные операции на шкалах Крипке — лексикографическое (или порядковое) произведение и сумму, и соответствующие им операции на модальных логиках. Наша цель — построение аксиоматик возникающих логик. Один конкретный результат такого рода был известен в связи с исследованиями по теории доказательств: в 2007 г. Л. Д. Беклемишев описал аксиоматику суммы нескольких экземпляров логики Гёделя-Лёба GL. Недавно нам удалось доказать несколько общих теорем такого рода, в частности, найти аксиоматики сумм и произведений логик K, K4, S4, S5 и многих других. Доклад основан на совместной работе с Ф. Балбиани и В. Б. Шехтманом.
  196. 2015.03.12: О некоторых медленно терминируемых системах преобразований термов
    Докладчик: Оноприенко Анастасия Александровна, студ. 3-го курса, научный руководитель Л. Д. Беклемишев
    Аннотация. В этой работе мы формулируем простое комбинаторное утверждение, называемое принципом Червя. Это наглядный пример истинной, но недоказуемой в арифметике Пеано PA теоремы. Её доказательство основано на использовании только счётных ординалов, а потому может быть проведено в теории ZFC. На основе принципа Червя мы строим простые системы подстановок термов в логике первого порядка. Число шагов работы таких систем на произвольном входе конечно, но не ограничивается никакой вычислимой функцией от длины входа, доказуемо тотальной в арифметике Пеано PA. Тем самым утверждение о терминируемости этих систем недоказуемо в PA.
  197. 2015.03.05: Бисимуляционные игры и локально табличные модальные логики (продолжение)
    Докладчик: Шехтман В.Б.
  198. 2015.02.26: Логика с модальностью неравенства DL
    Докладчик: Кудинов Андрей Валерьевич, к.ф.-м.н.
  199. 2015.02.19: Бисимуляционные игры и локально табличные модальные логики
    Докладчик: Шехтман В.Б.
  200. осень 2014
  201. 2014.12.11: О некоторых разрешимых финитно неаксиоматизируемых бимодальных логиках (продолжение)
    Докладчик: Матузенко Виктор Сергеевич, аспирант ИППИ, научный руководитель В. Б. Шехтман
  202. 2014.12.04: О некоторых разрешимых финитно неаксиоматизируемых бимодальных логиках
    Докладчик: Матузенко Виктор Сергеевич, аспирант ИППИ, научный руководитель В. Б. Шехтман
    Аннотация. По работе А.Куруш и С.Марселино.
  203. 2014.11.25: Теорема о характеризации для класса конечных шкал логики K×K
    Докладчик: Осипов Илья Игоревич, аспирант ИППИ, научный руководитель В. Б. Шехтман
    Аннотация. В докладе будет изложено доказательство того, что формулы первого порядка, сохраняющие истинность в бимодально эквивалентных конечных моделях логики K×K, — это в точности формулы, семантически эквивалентные в классе конечных шкал логики K×K переводам бимодальных формул.
  204. 2014.11.20: Произведения модальных логик в окрестностной семантике (продолжение)
    Докладчик: Кудинов Андрей Валерьевич, к.ф.-м.н.
  205. 2014.11.13: Произведения модальных логик в окрестностной семантике
    Докладчик: Кудинов Андрей Валерьевич, к.ф.-м.н.
  206. 2014.11.06: Об интуиционистской логике знания
    Докладчик: Крупский В.Н.
  207. 2014.10.30: Об усилении теоремы Крахта
    Докладчик: Пахомов Ф.Н., аспирант МИАН, научный руководитель Л. Д. Беклемишев
    Аннотация. В докладе будет рассказано об усилении теоремы Крахта. Крахт показал, что если кардинал является наименьшей мощностью, в которой имеется модель некоторой счётной теории второго порядка, то существует некоторая модальная логика такая, что этот кардинал равен наименьшей мощности, в которой имеется шкала Крипке, чья логика в точности равна этой модальной логике. Мы усиливаем этот результат, находя искомую модальную логику уже среди расширений S4.
  208. 2014.10.23: О модальных логиках, которым нужны очень большие шкалы
    Докладчик: Пахомов Ф.Н., аспирант, научный руководитель Л. Д. Беклемишев
    Аннотация. Будет разобрана статья М. Крахта “Modal logics that need very large frames”. Будет обсуждаться вопрос о том, какие кардиналы могут быть описаны как наименьшие мощности шкал в классе шкал с некоторой фиксированной модальной логикой. Совокупность таких кардиналов известна как спектр Кузнецова. Как оказывается, спектр Кузнецова может содержать очень большие кардиналы. В частности, если существует недостижимый (слабо компактный, измеримый) кардинал, то в спектре Кузнецова есть кардинал, больший первого недостижимого (слабо компактного, измеримого) кардинала. Центральным результатом Крахта является то, что спектр Кузнецова совпадает с совокупностью всех кардиналов, являющихся наименьшими мощностями моделей фиксированных Π11 логик с конечными сигнатурами.
  209. 2014.10.16: Фильтруемость регулярных грамматических модальных логик
    Докладчик: Золин Е.Е., к.ф.-м.н.
    Аннотация. Данный доклад формально является продолжением предыдущего, но фактически от слушателей не будет требоваться знание содержания первой части. Мы расскажем, что такое грамматические модальные логики, в частности, регулярные. Мы покажем, что фильтруемость (определение будет дано) последних, а следовательно, их финитная аппроксимируемость и разрешимость легко получается из (рассказанных в прошлый раз) результатов о том, что операции транзитивного замыкания, объединения и композиции отношений в шкалах Крипке безопасны для фильтруемости. Наконец, мы приведем явные конструкции фильтрации для некоторых естественных семейств регулярных грамматических модальных логик (левосторонних, правосторонних и других). Данный доклад можно также считать дополнением к докладу (прошлого года) Станислава Кикотя о неразрешимых грамматических модальных логиках.
  210. 2014.10.09: Операции на шкалах, сохраняющие фильтруемость
    Докладчик: Золин Е.Е., к.ф.-м.н.
    Аннотация. Совместная работа с И. Шапировским и С. Кикотем. В модальной логике нередко изучается следующий вопрос: можно ли добавить в язык рассматриваемой логики новую модальность, расширив тем самым ее выразительные возможности, но не (сильно) испортив основные свойства логики, такие как полнота, разрешимость, финитная аппроксимируемость и т.п. Мы расскажем о таком свойстве логик, как фильтруемость (в общих чертах это — возможность устанавливать ее разрешимость методом фильтрации); приведем примеры фильтруемых и нефильтруемых (в данном смысле) логик; главное — рассмотрим вопрос о том, добавление каких модальностей (и сооответствующих им операций на отношениях достижимости, или более общо, на шкалах Крипке) сохраняет фильтруемость логики.
  211. 2014.10.02: О парадоксальных и непарадоксальных системах высказываний, ссылающихся друг на друга
    Докладчик: Савельев Денис Игоревич, ИППИ РАН.
    Аннотация. Как известно, все классические парадоксы содержат некоторый род самоссылающихся утверждений. Пример парадокса, не содержащего явной ссылки на себя, был предложен Ябло 20 лет назад. Этот новый парадокс можно рассматривать как развёртывание парадигматического парадокса лжеца: он состоит из высказываний, занумерованных натуральными числами так, что каждое высказывание утверждает «все высказывания со следующими номерами ложны». Нашей целью является исследование произвольных систем высказываний, некоторые из которых утверждают, что некоторые другие ложны, и установление критерия парадоксальности либо непарадоксальности такой системы. Для этого мы предлагаем теорию первого порядка в языке с одним одноместным и одним двуместным предикатами T и U, состоящую из двух аксиом:
    ∀x ( Tx → ∀y ( Uxy → ¬Ty ) ),
    ∀x ( ¬Tx ∧ ∃y Uxy → ∃y ( Uxy ∧ Ty ) ).
    Эвристическое значение этой теории таково: переменные понимаются как высказывания, Tx означает «x истинно», Uxy означает «x утверждает, что y ложно». Модель (X,U) называется непарадоксальной, если её можно обогатить до некоторой модели (X,T,U) данной теории, и парадоксальной иначе. Например, модель, соответствующая парадоксу лжеца, состоит из одной рефлексивной точки; модель парадокса Ябло изоморфна натуральным числам с их обычным упорядочением, и обе они являются парадоксальными. Обобщая эти два примера, мы замечаем, что любая модель с транзитивным отношением U без максимальных элементов парадоксальна. С другой стороны, любая модель с фундированным отношением U–1 непарадоксальна. Мы показываем, что свойство быть парадоксальным принадлежит классу Π11, но не классу Σ11, и предлагаем естественную классификацию непарадоксальных моделей.
  212. весна 2014
  213. 2014.05.15:
    Speaker: Meghyn Bienvenu (Paris, France)
    Abstract. The prime implicates of a formula are defined to be its strongest clausal consequences. Prime implicates have been extensively studied in propositional and first-order logic and have several applications in artificial intelligence. In this talk, I will give an overview of my work on prime implicates in the basic multi-modal logic Kn. First, I will discuss the problem of choosing an adequate definition of modal prime implicate and compare several alternative definitions. Then, for the selected definition, I will present some results on the two main computational tasks: generating and recognizing prime implicates.
  214. 2014.04.24: Финитная аппроксимируемость некоторых модальных логик, задаваемых хорновыми формулами
    Докладчик: Заплетин Андрей Максимович, студ. 5-го курса, научные руководители В.Б.Шехтман В.Б. и И.Б.Шапировский
  215. 2014.04.10: Канонические фильтрации и локально табличные модальные логики
    Докладчик: Шехтман В.Б.
  216. 2014.04.03: Алгоритмическая сложность проблемы выполнимости некоторых транзитивных плотных модальных логик
    Докладчик: Чижов Алексей Сергеевич, аспирант ИППИ, научный руководитель В.Б.Шехтман
  217. 2014.03.27: О неполноте в пучках Крипке квантифицированных версий некоторых S4-логик
    Докладчик: Маслов Николай Александрович, аспирант ИППИ, научный руководитель В.Б.Шехтман
    Аннотация. Будет рассказано обобщение результата Silvio Ghilardi, полученного в работе "Incompleteness results in Krilke semantics". Все результаты этой работы могут быть перенесены на случай пучков Крипке.
  218. 2014.03.20: Предикатные аналоги первичной логики Гуревича
    Докладчик: Подгайц Александра Ефремовна, аспирантка, научный руководитель Л.Д.Беклемишев
  219. 2014.03.13: О двух понятиях ультрарасширений бинарных отношений
    Докладчик: Савельев Денис Игоревич, ИППИ РАН.
    Аннотация. Существуют два различных понятия ультрарасширений бинарных отношений. Одно из них было обнаружено в модальной логике и использовано ван Бентемом для получения характеризации модальной определимости. Другое понятие ультрарасширений было недавно введено докладчиком в контексте общей теории моделей (некоторые близкие понятия были известны с 60-х гг. в двух разных областях: теории множеств и комбинаторных задачах алгебры). В докладе будет описано точное соотношение этих двух понятий, а также даны их топологические характеризации.
  220. 2014.03.06: О парадоксальных и непарадоксальных системах высказываний, ссылающихся друг на друга
    (On paradoxical and non-paradoxical systems of propositions referring to each other)
    Докладчик: Савельев Денис Игоревич, ИППИ РАН.
    Аннотация. As is well-known, all classical paradoxes involve a kind of self­reference. A paradox without any explicit self­reference was proposed by Yablo twenty years ago in [1] (for a subsequent discussion see [2]—[6]). This new paradox can be considered as an unfolding of the paradigmatic Liar Paradox: it consists of propositions indexed by natural numbers such that each of the propositions states “all propositions with greater indices are wrong”. Our purpose is to investigate arbitrary systems of propositions some of which state that some others are wrong, and to learn which of these systems are paradoxical and which are not. For this, we introduce a first-order theory in a language with one unary and one binary predicates, T and U, consisting of two axioms:
    ∀x ( Tx → ∀y ( Uxy → ¬Ty ) ),
    ∀x ( ¬Tx ∧ ∃y Uxy → ∃y ( Uxy ∧ Ty ) ).
    Heuristically, variables mean propositions, Tx means “x is true”, and Uxy means “x states that y is wrong”. A model (X,U) is called non­paradoxical if it can be enriched to some model (X,T,U) of this theory, and paradoxical otherwise. E.g. a model of the Liar Paradox consists of one reflexive point, a model of the Yablo Paradox is isomorphic to natural numbers with their usual ordering, and both are paradoxical. Generalizing these two instances, we note that any model with a transitive U without maximal elements is paradoxical. On the other hand, any model with a well­founded U–1 is non-paradoxical. We provide a classification of non-paradoxical models.

    Bibliography

    [1] S.Yablo, “Paradox without self-reference”, Analysis, 53:4 (1993), 251—251.
    [2] T.E.Forster, “The significance of Yablo's paradox without self­reference”, Manuscript, 1996.
    [3] G.Priest, “Yablo's paradox”, Analysis, 57:4 (1997), 236—242.
    [4] R.Sorensen, “Yablo's paradox and kindred infinite liars”, Mind, 107 (1998), 137—155.
    [5] Jc.Beall, “Is Yablo's paradox non­circular?”, Analysis, 61:3 (2001), 176—187.
    [6] T.E.Forster, “Yablo's paradox and the omitting types theorem for propositional languages”, Manuscript, 2012.
  221. 2014.02.27: Проблема распознаваемости аксиоматик модальной логики K
    Докладчик: Золин Е.Е., к.ф.-м.н.
    Аннотация. В докладе будет дан ответ на вопрос о том, существует ли алгоритм, который по произвольному конечному множеству модальных формул распознаёт, даёт ли оно, вместе с тремя правилами вывода: modus ponens, подстановки и усиления, полную аксиоматику модальной логики K. Данный результат получен в 2013 году Чагровым, доказательство упрощено докладчиком. Аналогичным вопросом — (не)распознаваемостью аксиоматик для различных пропозициональных (не модальных) исчислений: классического, интуиционистского, суперинтуиционистских, противоречивого — занимались многие исследователи, начиная с первых работ Поста и Линьяла (1949) и Кузнецова (1963) и заканчивая Боковым (2009), получившим сравнительно краткое и изящное доказательство для классической логики, впоследствии упрощенное и обобщенное докладчиком на суперинтуиционистские локики (2012), а позже усиленное Боковым на импликативные суперинтуиционистские локики (2014).
  222. <!-- Обсуждение плана на новый семестр
  223. 2014.02.20:
  224. --> <!--
-->

Семинар «Модальная и алгебраическая логика»

<!--
    -->
    осень 2013
  1. 2013.12.10: Полнота исчисления Ламбека–Гришина с унарными модальностями относительно реляциононных моделей (продолжение)
    Докладчик: Смуров Иван Михайлович, аспирант, научный руководитель М.Р.Пентус
  2. 2013.12.03: Модальная логика интервалов Халперна–Шохама: происхождение, вычислительная сложность
    Докладчик: Чижов Алексей Сергеевич, аспирант ИППИ, научный руководитель В.Б.Шехтман
    Аннотация. В докладе будет представлена оригинальная работа Халперна–Шохама 1996 года, где вводится логика интервалов на временных структурах. Получены результаты вычислительной сложности для логики с шестью естественными модальностями.
  3. 2013.11.26: Полнота исчисления Ламбека–Гришина с унарными модальностями относительно реляциононных моделей
    Докладчик: Смуров Иван Михайлович, аспирант, научный руководитель М.Р.Пентус
  4. 2013.11.19: Неразрешимость модальных логик, связанных с контекстно-свободными грамматиками
    Докладчик: Кикоть Станислав Павлович, к.ф.-м.н., научный руководитель В.Б.Шехтман
  5. 2013.11.12: Финитная аппроксимирумость некоторых модальных логик, «похожих» на K4
    Докладчик: Заплетин Андрей Максимович, студ. 4-го курса, науч. рук. В.Б.Шехтман и И.Б.Шапировский.
    Аннотация. Будет приведено доказательство финитной аппроксимируемости, а значит, и разрешимости расширения модальной логики K аксиомой &square; p → &square;&square;&square; p. (Результат Д.Габбая 70-х гг).
  6. 2013.11.05: Сети доказательства для исчисления Ламбека и линейной логики
    Докладчик: Кузнецов С.Л., к.ф.-м.н., научный руководитель М.Р.Пентус
  7. 2013.10.29: Каноничность модальной логики S4.1
    Докладчик: Журавлев Александр Алексеевич, студ. 4-го курса, научный руководитель В.Б.Шехтман
  8. 2013.10.22: Теоремы полноты для гибридных логик (продолжение)
    Докладчик: Вахрушева Полина Викторовна, аспирантка, научный руководитель В.Б.Шехтман
  9. 2013.10.15: Теоремы полноты для гибридных логик
    Докладчик: Вахрушева Полина Викторовна, аспирантка, научный руководитель В.Б.Шехтман
  10. 2013.10.08: Некоторые результаты о неразрешимости модальных и интуиционистких предикатных логик с использованием семантики категорий (продолжение)
    Докладчик: Маслов Николай Александрович, аспирант, научный руководитель В.Б.Шехтман
  11. 2013.10.01: Некоторые результаты о неразрешимости модальных и интуиционистких предикатных логик с использованием семантики категорий
    Докладчик: Маслов Николай Александрович, аспирант, научный руководитель В.Б.Шехтман
  12. 2013.09.24: Неразрешимость модальных логик между K×K×K и S5×S5×S5 (продолжение)
    Докладчик: Осипов Илья Игоревич, аспирант ИППИ, научный руководитель В.Б.Шехтман
  13. 2013.09.17: Неразрешимость модальных логик между K×K×K и S5×S5×S5
    Докладчик: Осипов Илья Игоревич, аспирант ИППИ, научный руководитель В.Б.Шехтман
  14. весна 2013
  15. 2013.05.14: Некоторые теоремы о неполноте модальных предикатных логик в семантике Крипке
    Докладчик: Маслов Николай, аспирант, научный руководитель В.Б.Шехтман
  16. 2013.05.07: Временные гибридные логики с модальностями «вчера» и «завтра»
    Докладчик: Вахрушева Полина Викторовна, науч. рук. В.Б.Шехтман.
  17. 2013.04.30: Финитная аппроксимируемость и другие свойства модальной логики K×K×K
    Докладчик: Осипов Илья Игоревич, аспирант ИППИ, научный руководитель В.Б.Шехтман
  18. 2013.04.23: О работах Якуба Михалишина в модальной логике
    Докладчик: Кикоть Станислав Павлович, к.ф.-м.н., научный руководитель В.Б.Шехтман
  19. 2013.04.16: О модальной логике конечноместных операций на топологическом пространстве и итерированной производной Кантора (продолжение)
    Докладчик: Савельев Д.И.
  20. 2013.04.09: Кванторная логика S4 с модальностями “de re” и “de dicto”
    Докладчик: Яворская Т.Л.
  21. 2013.04.02: О модальной логике конечноместных операций на топологическом пространстве и итерированной производной Кантора
    Докладчик: Савельев Д.И.
  22. 2013.03.26: О понятии выразимости модели Крипке в модальной логике (продолжение)
    Докладчик: Золин Е.Е.
    Аннотация. В первой половине доклада (на прошлом заседании семинара) было сформулировано определение понятия, указанного в заголовке доклада, и приведены простейшие примеры его применения. Во второй половине доклада будут рассказаны, с разной степенью подробности, два более серьёзных недавних результата, полученных с использованием данной техники.

    В первом, полученном докладчиком, утверждается неразрешимость некоторой (градуированной) модальной логики с одной модальностью (т.е. одним отношением в шкале Крипке).

    Второй результат касается нижней оценки сложности некоторой модальной логики (так же с одной модальностью); данный результат получен Ian Pratt-Hartmann в 2009 г, доказательство упрощено докладчиком.

  23. 2013.03.19: О понятии выразимости модели Крипке в модальной логике
    Докладчик: Золин Е.Е.
    Аннотация. Указанное в названии понятие, введенное докладчиком, оказалось удобным инструментом при доказательстве неразрешимости или получении нижних оценок вычислительной сложности различных модальных логик. Оно позволяет представить такое доказательство в виде двух частей, имеющих самостоятельный интерес, что делает доказательство более прозрачным. Будут сформулированы локальный и глобальный варианты данного понятия и приведены некоторые их применения.
  24. 2013.03.12: О логике регионов с булевыми связками
    Докладчик: Матвеева Екатерина Сергеевна, науч. рук. В.Б.Шехтман.
  25. 2013.03.05: Порядковые суммы шкал Крипке
    Докладчик: Шапировский И.Б.
    Аннотация. Всякая шкала (W,R), где отношение R транзитивно, может быть рассмотрена как частично упорядоченное множество своих сгустков (максимальных подмножеств W, в которых отношение универсально). Операция порядковой суммы шкал является обобщением этой несложной конструкции на случай, где вместо сгустков рассматриваются произвольные шкалы. Мы расскажем, как можно проверять выполнимость модальных формул на таких шкалах, и получим простое доказательство разрешимости в полиномиальной памяти для целого ряда расширений K4.
  26. 2013.02.26: Модальные интервальные логики с отношением «включение» (продолжение)
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
  27. 2013.02.19: Модальные интервальные логики с отношением «включение»
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
  28. осень 2012
  29. 2012.12.18: Графы Эрдёша и примеры канонических модальных логик, не определимых никаким элементарным классом шкал (продолжение)
    Докладчик: Маслов Николай Александрович, науч. рук. В.Б.Шехтман.
  30. 2012.12.11: Графы Эрдёша и примеры канонических модальных логик, не определимых никаким элементарным классом шкал
    Докладчик: Маслов Николай Александрович, науч. рук. В.Б.Шехтман.
    Аннотация. Доклад по статье [1]. Abstract из [1]:

    We show that there exist continuum-many equational classes of Boolean algebras with operators that are not generated by the complex algebras of any first-order definable class of relational structures. Using a variant of this construction, we resolve a long-standing question of Fine, by exhibiting a bimodal logic that is valid in its canonical frames, but is not sound and complete for any first-order definable class of Kripke frames (a monomodal example can then be obtained using simulation results of Thomason). The constructions use the result of Erd&odblac;s that there are finite graphs with arbitrarily large chromatic number and girth.

    [1] Robert Goldblatt, Ian Hodkinson, and Yde Venema "Erd&odblac;s graphs resolve Fine's canonicity problem", Bull. Symbolic Logic 10 no. 2 (June 2004), 186-208. [pdf]

  31. 2012.12.04: Простое бестиповое лямбда-исчисление
    Докладчик: Мухутдинова Татьяна
  32. 2012.11.27: Нижняя оценка длины совмещающего типа в исчислении Ламбека
    Докладчик: Сорокин Алексей
  33. 2012.11.20: Отсутствие равномерной интерполяции в исчислении Ламбека без умножения
    Докладчик: Смуров Иван Михайлович, науч. рук. М.Р.Пентус
  34. 2012.11.13: Критерий выводимости для исчисления Лабека без умножения
    Докладчик: Смуров Иван Михайлович, науч. рук. М.Р.Пентус
  35. 2012.11.06: О модальных логиках некоторых произведений окрестностных шкал (продолжение)
    Докладчик: Кудинов Андрей Валерьевич
  36. 2012.10.30: Теоремы о полноте и неполноте для тождеств в полурешетках
    Докладчик: Кикоть Станислав Павлович (Лондон)
  37. 2012.10.23: О модальных логиках некоторых произведений окрестностных шкал
    Докладчик: Кудинов Андрей Валерьевич
  38. <!-- Было ли заседание?
  39. 2012.10.16:
  40. -->
  41. 2012.10.09: О модальной логике топологической динамики: действия полугрупп
    Докладчик: Савельев Денис Игоревич
  42. <!-- Было ли заседание?
  43. 2012.10.02:
  44. -->
  45. 2012.09.25: О произведениях модальных логик с логикой неравенства
    Докладчик: Осипов Илья Игоревич, науч. рук. В.Б.Шехтман.
  46. 2012.09.18: Математическая морфология
    Докладчик: Кузнецов С.Л.
  47. весна 2012
  48. 2012.05.15: Дихотомия среди некоторых элементарно порождённых модальных логик
    Докладчик: Кикоть Станислав Павлович (Лондон)
  49. 2012.04.24: О неразрешимости модальных логик хэмминговых шкал фиксированной конечной размерности больше двух
    Докладчик: Шапировский И.Б.
  50. 2012.04.17: Равномерные оценки и допустимые правила вывода
    Докладчик: Шехтман В.Б.
  51. 2012.04.10: Примеры типов исчисления Ламбека, не имеющих равномерного постинтерполянта
    Докладчик: Смуров Иван Михайлович, науч. рук. М.Р.Пентус
  52. 2012.04.03: Теорема Гольдблатта–Томасона для модальных шкал Крипке
    Докладчик: Маслов Николай Александрович, науч. рук. В.Б.Шехтман.
  53. 2012.03.27: Некоторые обобщения теоремы ван Бентема
    Докладчик: Осипов Илья Игоревич, науч. рук. В.Б.Шехтман.
  54. 2012.03.20: Деривационные модальные логики с модальностью неравенства (продолжение)
    Докладчики: Кудинов А.В., Шехтман В.Б.
  55. 2012.03.13: Деривационные модальные логики с модальностью неравенства
    Докладчики: Кудинов А.В., Шехтман В.Б.
  56. 2012.03.06: Модальная логика с переменными модальностями
    Докладчик: Золин Е.Е.
  57. 2012.02.28: Модальные логики хэмминговых пространств
    Докладчик: Шапировский И.Б.
  58. 2012.02.21: Модальная логика и запросы к базам знаний
    Докладчик: Золин Е.Е.
  59. осень 2011
  60. 2011.12.13: Эволюция регуляторного сигнала экспрессии гена
    Докладчик: Куриленко Владислав Игоревич, науч. рук. В.А.Любецкий.
  61. <!-- Было ли заседание?
  62. 2011.12.06:
  63. -->
  64. 2011.11.29: Топологические модальные логики
    Докладчик: Шехтман В.Б.
  65. <!-- Было ли заседание?
  66. 2011.11.22:
  67. -->
  68. 2011.11.15: Разрешимые интервальные логики с модальностью «касается»
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
  69. 2011.11.08: L-полнота вариантов исчисления Ламбека
    Докладчик: Звонкин М.М.
  70. 2011.11.01: О числе расширений для соединений модальных логик над S4
    Докладчик: Измайлов Максим
  71. <!--
  72. 2011.10.25: Заседания не было.
  73. -->
  74. 2011.10.18: Модальная определимость формул первого порядка с несколькими свободными переменными (продолжение)
    Докладчик: Золин Е.Е. (по совместной работе с Кикотем С.П.)
  75. 2011.10.11: Модальная определимость формул первого порядка с несколькими свободными переменными
    Докладчик: Золин Е.Е. (по совместной работе с Кикотем С.П.)
  76. 2011.12.04: О логике доказательств первого порядка (продолжение)
    Докладчик: Яворская Т.Л.
  77. 2011.09.27: О логике доказательств первого порядка
    Докладчик: Яворская Т.Л.
  78. весна 2011
  79. 2011.05.17: Логика доказательств первого порядка
    Докладчик: Яворская Т.Л.
  80. 2011.05.10: Алгоритм построения супердерева по набору деревьев
    Докладчики: Котляров Никита, Куриленко Владислав
  81. 2011.05.03: Аналог теоремы Ван Бентема-Розена для шкал с бинарными предикатами (продолжение)
    Докладчик: Осипов Илья Игоревич, науч. рук. В.Б.Шехтман.
  82. 2011.04.26: Аналог теоремы Ван Бентема-Розена для шкал с бинарными предикатами
    Докладчик: Осипов Илья Игоревич, науч. рук. В.Б.Шехтман.
  83. 2011.04.19: Неразрешимость одной градуированной модальной логики
    Докладчик: Золин Е.Е.
  84. 2011.04.12: Гибридные модальные логики (продолжение)
    Докладчик: Вахрушева Полина Викторовна, науч. рук. В.Б.Шехтман.
  85. 2011.04.05: О предтранзитивных модальных логиках
    Докладчики: Шапировский Илья Борисович, Кудинов Андрей Валерьевич
  86. 2011.03.29: О логиках отрезков вещественной оси (продолжение)
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
  87. 2011.03.22: Гибридные модальные логики
    Докладчик: Вахрушева Полина Викторовна, науч. рук. В.Б.Шехтман.
  88. 2011.03.15: О логиках отрезков вещественной оси
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
  89. осень 2010
  90. 2010.11.25: О минимальной логике доказуемости, связанной со 2-й теоремой Геделя
    Докладчик: Беклемишев Л.Д.
  91. 2010.11.18: Позитивные фрагменты полимодальной логики доказуемости
    Докладчик: Дашков Евгений Владимирович, науч. рук. Л.Д.Беклемишев.
  92. 2010.11.11: О предтабличных расширениях логик S4 и K4
    Докладчик: Измайлов Максим, науч. рук. В.Б.Шехтман.
  93. 2010.09.16: Дескрипционные и модальные логики: сходства и различия (продолжение)
    Докладчик: Золин Е.Е.
  94. 2010.09.09: Дескрипционные и модальные логики: сходства и различия
    Докладчик: Золин Е.Е.
  95. <!--
-->

Семинар «Логические проблемы информатики»

<!--
    -->
    осень 2013
  1. 2013.12.12: Интернализация доказательств в обобщенных системах Фреге для классической логики
    Докладчик: Саватеев Ю.В., к.ф.-м.н., научный руководитель М.Р.Пентус
    Аннотация. Будет представлен общий метод интернализации доказательств для формальных систем описания классической логики и описана связь получающихся в результате систем с модальными логиками.
  2. 2013.12.11: О стратегических играх, имеющих определенное решение (online доклад)
    Докладчик: Артёмов С.Н., проф., Нью-Йорк
    Аннотация. В своей диссертации 1950 года Нэш обосновывал введение эквилибриума как решения игры предположением о том, что рациональное решение единственно и может быть выведено игроками из описания правил игры. Мы исследуем это предположение методами эпистемической модальной логики для класса стратегических игр с упорядоченными предпочтениями. Мы показываем, что предположение Нэша верно далеко не всегда, и что доля разрешимых игр стремится к нулю с ростом размера игры. Более того, критерием существования определенного решения является не единственность эквилибриума, а сходимость процесса устранения строго доминированных стратегий.
  3. <!-- Были ли?
  4. 2013.12.05:
  5. 2013.11.28:
  6. -->
  7. 2013.11.21: О длине переписывания конъюнктивных запросов относительно OWL 2 QL онтологий
    Докладчик: Кикоть Станислав Павлович, к.ф.-м.н., научный руководитель В.Б.Шехтман
    Аннотация. В докладе рассматривается следующая задача. Дана теория первого порядка T, которая может содержать аксиомы лишь двух видов:
    (1) ∀x ( C(x) → D(x) ), где C(x) и D(x) имеют вид A(x) или ∃y R(x,y);
    (2) ∀x ∀y (R(x,y) → S(y,x)),
    и экзистенциальная конъюнктивная формула q (запрос). Требуется построить такую позитивно экзистенциальную формулу первого порядка q' (переписывание запроса q), зависящую от q и T, чтобы для любого набора атомов I (данных), из I и T следовало бы q тогда и только тогда, когда из I следует q', и оценить сверху и снизу размер q' в зависимости от разных ограничений на T.
  8. <!-- Был ли?
  9. 2013.11.14:
  10. -->
  11. 2013.11.07: «Первичная» логика Гуревича–Неемана PL и правило замены подформулы на эквивалентную
    Докладчик: Прохоров И.В., бакалавриат ВШЭ
    Аннотация. Будет рассказан результат о разрешимости за полиномиальное время расширения логики PL слабым правилом замены.
  12. <!-- Были ли эти семинары?
  13. 2013.10.31:
  14. 2013.10.24:
  15. 2013.10.17:
  16. 2013.10.10:
  17. --> <!--
  18. 2013.10.03: Обсуждение открытых вопросов и тем для докладов
  19. -->
    весна 2013
  20. 2013.04.18: Конъюнктивные грамматики в нормальной форме Грейбах и исчисление Ламбека с аддитивными связками
    Докладчик: Кузнецов С.Л.
    Аннотация. Предложенные Охотиным конъюнктивные грамматики — это обобщение контекстно-свободных грамматик добавлением операции «конъюнкция»: если из u1, ..., uk выводится одно и то же слово w и в грамматике есть правило A → u1 & ... & uk, то считается, что слово w выводится из A. Для конъюнктивных грамматик определяется аналог нормальной формы Грейбах; теорема о приведении к этой нормальной форме пока доказана только для случая однобуквенного алфавита. С помощью конъюнктивных грамматик можно задать некоторые нетривиальные языки, например { a4n | n > 0 }. Мы докажем, что язык, порождённый конъюнктивной грамматикой в нормальной форме Грейбах, может быть порождён категориальной грамматикой, основанной на исчислении Ламбека, расширенном операцией пересечения (аддитивной конъюнкцией).
  21. 2013.04.11: Логика первого порядка со связывающим модальностями
    Докладчик: Яворская Т.Л.
  22. 2013.02.21: Автоматы, основанные на моноидах, и теорема Хомского–Шюгценберже
    Докладчик: Сорокин А.А.
  23. осень 2012
  24. 2012.12.02: Арифметическая полнота для позитивной логики равномерной схемы рефлексии
    Докладчик: Беклемишев Л.Д.
    Аннотация. Будет доказана арифметическая полнота позитивной логики для этой модальности (в стиле теоремы Соловея), что решает задачу, оставленную открытой в моём предыдущем докладе на эту тему.
  25. 2012.11.29: Верхняя оценка длины совмещающего типа в исчислении Ламбека
    Докладчик: Сорокин Алексей
  26. 2012.11.15: Об аксиоматизации позитивных логик доказуемости
    Докладчик: Беклемишев Л.Д.
    Аннотация. Позитивные логики доказуемости позволяют интерпретировать пропозициональные переменные не только как индивидуальные арифметические предложения, но и как схемы. Это позволяет рассматривать, в частности, равномерную схему рефлексии как модальность. Будет рассказано о текущих результатах по аксиоматизации позитивных логик доказуемости и вопросах, остающихся открытыми.
  27. осень 2011
  28. 2011.11.10: Интерполяционные свойства логик доказуемости и нормализация термов рефлексивной комбинаторной логики
    Докладчик: Шамканов Д.С.
  29. 2011.11.03: PSpace-полнота замкнутого фрагмента логики доказуемости GLP
    Докладчик: Пахомов Ф.Н.
  30. 2011.10.20: Σ1-предложения и рекурсивно перечислимые множества
    Докладчик: Шавруков В.Ю. (Амстердам)
  31. 2011.10.13: Исчисление Ламбека: открытые проблемы
    Докладчик: Пентус М.Р.
  32. 2011.09.28: Основные понятия теории процессов
    Докладчик: Миронов А.
    Аннотация. Теория процессов является одним из основных математических формализмов, предназначенных для моделирования и верификации вычислительных систем. Ее основы были заложены выдающимся английским математиком Р. Милнером. В докладе будут изложены основные понятия теории процессов, в том числе — алгебраические операции на процессах, понятие наблюдаемого бимоделирования. Кроме того, будет представлен один из вариантов обобщения понятия процесса — процесс с передачей сообщений, а также показано применение этого понятия для решения задач моделирования и верификации телекоммуникационных протоколов.