Объединенный семинар
«Логические проблемы информатики»
(руководители: проф. С.Н.Артёмов, чл.-корр. РАН Л.Д.Беклемишев,
доц. В.Н.Крупский, проф. М.Р.Пентус, доц. Т.Л.Яворская)

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

(руководители: проф. М.Р.Пентус,
проф. В.Б.Шехтман, к.ф.-м.н. И.Б.Шапировский)


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  16. 2018.10.04: О консервативности схем ограниченности (продолжение)
    Докладчик: Пахомов Ф.Н., к.ф.-м.н., МИАН.
  17. 2018.09.27: О консервативности схем ограниченности
    Докладчик: Пахомов Ф.Н., к.ф.-м.н., МИАН.
    Аннотация. (Не отформатировано.)

    Классы формул ??n и ??n в арифметике первого порядка можно понимать в стандартном (узком) смысле, как состоящие из формул начинающиеся из подходящей кванторной приставки из неограниченных кванторов (?x ) после которой идет формула только с ограниченными кванторами (?x?t). Но также их можно понимать и в широком смысле, как классы формул, в которых ограничивается число альтернаций неограниченных кванторов, а ограниченные кванторы могут использоваться произвольным образом. Каждая ??n( ??n) формула в широком может быть преобразована в ??n( ??n) формулу в стандартном смысле. Естественный способ такого преобразования - это пронесение неограниченных кванторов сквозь ограниченные, что позволяет делать схема ??n ограниченности B??n: (?x?y)?z ?(x,y,z)  ?z?(?x?y)(?z?z?) ?(x,y,z), где ????n. Схемы B??n и их взаимоотношение с другими арифметическими аксиомами были предметом подробного изучения. В частности, еще в 1970-х независимо Х. Фридманом и Д. Парисом была доказана ??_{n+1} консервативность схемы B??_{n+1} над теорией ??n индукции I??n. Позднее этот результат был обобщен Л.Д. Беклемишевым, который дал простое необходимое и достаточное условие на ??_{n+1} аксиоматизируемые теории T для достижения ??_{n+1} консервативности B??_{n+1} над T. Описанная выше ситуация с пониманием иерархии ??n (??n) в широком и узком смысле и наличием принципа нужного для проноса кванторов имеет свои аналоги для других теорий. В теории множеств ограниченными считаются кванторы вида ?x?y, а принципы дающие возможность проносить неограниченные кванторы сквозь ограниченные - это схемы ?_n-Coll (отмечу, что схема ??-Coll известна в качестве одной из аксиом теории множеств Крипке-Платека). В арифметике второго порядка роль неограниченных кванторов играют кванторы по множествам натуральных чисел, роль ограниченных кванторов играют кванторы по натуральным числам, а для проноса кванторов используются схемы выбора ??_n-AC. Для систем ограниченной арифметики естественные иерархии формул - это иерархии ?^b_n (фактически являющиеся уровнями полиномиальной иерархии из теории сложности); вместо неограниченных кванторов используются ограниченные кванторы?x?t, a вместо ограниченных кванторов используются строго ограниченные кванторы ?x?log?(t), соответствующие принципы ограниченности обозначаются BB?^b_n. В настоящем докладе я расскажу об аналогах теоремы Беклемишева для теорий множеств, арифметик второго порядка и систем ограниченной арифметики (все они будут получены в качестве следствия из общего результата). Также я расскажу о том, как из этих общих теорем получается ряд конкретных результатов о частичной консервативности схем ограниченности и выбора над естественными формальными теориями.

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

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

  21. 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).

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

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

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

  23. 2018.03.29: Симплициальная семантика предикатных модальных логик (продолжение)
    Докладчик: Шехтман В.Б.
  24. 2018.03.22: Симплициальная семантика предикатных модальных логик
    Докладчик: Шехтман В.Б.
    Аннотация. Симплициальная семантика была введена Д.П.Скворцовым в начале 1990-х гг. как обобщение семантики Крипке (которая во многих случаях оказывается неадекватной). В докладе будет дан краткий обзор определений и основных теорем и доказан недавний результат о неполноте. Материал частично совпадает с докладом в МИАН осенью 2017 г., но часть о неполноте будет новой.
  25. 2018.03.15: Циклические выводы для эквациональной теории алгебр Клини (продолжение)
    Докладчик: Кузнецов С.Л.
  26. 2018.03.01: Циклические выводы для эквациональной теории алгебр Клини
    Докладчик: Кузнецов С.Л.
    Аннотация. (по статье A. Das, D. Pous. A cut-free cyclic proof system for Kleene algebra. Proc. TABLEAUX '17, LNCS/LNAI vol. 10501)

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

  27. 2018.02.22: О некоторых свойствах моделей эпистемической логики свидетельств
    Докладчик: Крупский В.Н.
    Аннотация. Аксиоматизируются свойства таких моделей — функциональность (свидетель подтверждает не более одной формулы) и строгость (произведение свидетелей в точности соответствует применению Modus Ponens).
  28. осень 2017
  29. 2017.12.14: Временные логики с топологической модальностью (продолжение)
    Докладчик: Шехтман В.Б.
  30. 2017.12.07: Временные логики с топологической модальностью
    Докладчик: Шехтман В.Б.
    Аннотация. Мы рассмотрим логики линейного времени со стандартными связками «всегда будет» и «всегда было», к которым добавляется топологическая S4-модальность «локальной истинности». Будет построена аксиоматика и доказана финитная аппроксимируемость таких логик для класса всех линейных порядков и для рациональной прямой. Будет дан краткий обзор дальнейших результатов и проблем в этой области.
  31. 2017.11.30: Предтранзитивные логики конечной глубины (продолжение)
    Докладчик: Кудинов Андрей Валерьевич
  32. 2017.11.23: Предтранзитивные логики конечной глубины
    Докладчик: Кудинов Андрей Валерьевич
    Аннотация. Одной из самых известных нерешенных проблем модальной логики является следующая: является ли разрешимой логика, задаваемая аксиомой □□p → □□□p. Эта аксиома задает понятное первопорядковое свойство R3 ⊆ R2. В общем случае можно рассматривать формулы вида mp → □np для m < n. Такие формулы задают логики, которые часто называют предтранзитивными, т.к. в них выразимо транзитивное замыкание, т.е. существует формула A(p) такая, что для любой формулы B, любой модели M и ее точки x имеем: M,x⊧A(B) ⇔ формула B истинна во всех точках, достижимых из x по отношению R за конечное число шагов. Каноничность таких формул легко проверяется, а вот стандартные способы доказательства финитной аппроксимируемости (и, как следствие, разрешимости) проходят только для случая, когда m = 1; для случая же m > 1 ни финитная аппроксимируемость, ни разрешимость до сих пор не известна. В нашей совместной работе с И. Шапировским мы сделали небольшой шаг в направлении решения этой проблемы. Мы доказали, что если взять любую из упомянутых аксиом и добавить аксиомы, соответствующие тому, что глубина транзитивного замыкания отношения не превосходит данного k (для логики S4 такие формулы давно известны из работ Сегерберга и Максимовой; мы берем те же формулы, но для транзитивного замыкания), то полученная логика будет финитно аппроксимируемой и разрешимой.

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

  33. 2017.11.09: Реконструкция модального аргумента Гёделя (продолжение)
    Докладчик: Красненкова Анастасия Владимировна (канд. филос. наук; бакалавриат мехмата, науч. рук. В.Н.Крупский)
  34. 2017.11.02: Реконструкция модального аргумента Гёделя
    Докладчик: Красненкова Анастасия Владимировна (канд. филос. наук; бакалавриат мехмата, науч. рук. В.Н.Крупский)
    Аннотация. В докладе будет проанализирована реконструкция так называемого онтологического аргумента Геделя, проведенная в системе интерактивных доказательств Coq К.Бенцмюллером и Б.Палео. Будут также рассмотрены тактики Coq, позволяющие работать в системе модальной логики.
  35. 2017.10.26: О сложности аналитических функций нескольких переменных
    Докладчик: Белошапка Валерий Константинович, профессор, кафедра ТФФА.
    Аннотация. В математическом анализе, как и в дискретной математике, есть круг вопросов, связанных с оценками сложности объектов. Или, другими словами, вопросы о возможности выразить функции некоторого класса с суперпозициями функций другого, более узкого класса. В анализе этот круг вопросов связан с именами Э. Галуа, Ж. Лиувилля, Д. Гильберта, А. Островского, А. Н. Колмогорова, В. И. Арнольда, А. Г. Витушкина. Докладчик планирует рассказать о своем подходе к задаче оценки сложности аналитических функций нескольких переменных, о недавно полученных результатах, о связях и аналогиях с другими областями математики, о возникающих в этой задаче конструкциях и о стоящих на этом пути проблемах.
  36. 2017.10.12: Неразрешимость интуиционистской логики предикатов в языке с одной одноместной предикатной буквой и двумя предметными переменными
    Докладчик: Рыбаков Михаил Николаевич (Тверской государственный университет)
    Аннотация.
    1. Техническая часть доклада
    Известно, что интуиционистская логика в языке с двумя предметными переменными неразрешима. Будет показано, что этот результат можно получить при дополнительных ограничениях на язык: когда используются только позитивные формулы от одноместных предикатных букв. Далее будет показано, как все одноместные буквы позитивных формул промоделировать одной одноместной буквой (тоже с использованием лишь позитивных формул). Таким образом, будет представлен результат о неразрешимости позитивного фрагмента интуиционистской логики предикатов в языке с одной одноместной предикатной буквой и двумя предметными переменными.

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

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

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

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

    Литература / References
    [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.

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

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

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

  43. 2017.04.27: Некоторые теоремы полноты для модальных логик предикатов (продолжение)
    Докладчик: Шехтман В.Б.
  44. 2017.04.20: Некоторые теоремы полноты для модальных логик предикатов
    Докладчик: Шехтман В.Б.
    Аннотация. Будет доказана полнота в семантике Крипке для предикатной модальной логики с аксиомами транзитивности и плотности. При этом для построения нужной контрмодели используется игровой метод. Тем же методом можно упростить доказательства результатов Корси (1993) о полноте модальных предикатных логик плотных линейных порядков с переменными областями. Вкратце будет сказано и о других применениях.
  45. 2017.03.30: О временных модальных логиках интервалов над ℚ и ℝ. Финитная аппроксимируемость, сложность и описание класса конечных шкал
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
    Аннотация. За последние 10 лет были получены результаты о (не)разрешимости более 90% модальных интервальных логик над линейными порядками. Значительная часть результатов относится к работам В.Горанко, А.Монтанари, В.Б.Шехтмана и др. Однако, вопрос о прочих свойствах логик, таких как финитная аппроксимируемость, алгоритмическая сложность, описание класса конечных шкал и т.д. для многих интервальных логик остается открытым.

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

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

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

  49. осень 2016
  50. 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.

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

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

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

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

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

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

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

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

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

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

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

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

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

  67. 2016.03.10: Доказательство гипотезы Виссера-Зутхаута об интерпретациях арифметики Пресбургера в себя (продолжение)
    Докладчик: Запрягаев Александр Александрович, студ. 4-го курса, научный руководитель Л. Д. Беклемишев
  68. 2016.03.10: Доказательство гипотезы Виссера-Зутхаута об интерпретациях арифметики Пресбургера в себя
    Докладчик: Запрягаев Александр Александрович, студ. 4-го курса, научный руководитель Л. Д. Беклемишев
    Аннотация. Альберт Виссер предложил рассмотреть вопрос описания всех одномерных интерпретаций без параметров арифметики Пресбургера в себя и выдвинул гипотезу о том, что все такие интерпретации доказуемо изоморфны тождественной, что влечёт также невозможность интерпретировать арифметику Пресбургера ни в одной из своих конечно аксиоматизируемых подтеорий. Будет представлено полученное автором доказательство гипотезы Виссера–Зутхаута. Функция, осуществляющая изоморфизм интерпретации арифметики Пресбургера в себя тождественной, будет построена, согласно идее к.ф.-м.н. Ф.Н.Пахомова, на основе анализа интерпретированного отношения порядка. Также будет продемонстрирована неожиданная связь с задачей Улама — Коллатца о последовательности «3n+1».
  69. 2016.03.03: Абстрактные варианты второй теоремы Гёделя о неполноте для логик слабее классической (продолжение)
    Докладчики: Беклемишев Л.Д., Шамканов Д.С.
  70. 2016.02.25: Абстрактные варианты второй теоремы Гёделя о неполноте для логик слабее классической
    Докладчики: Беклемишев Л.Д., Шамканов Д.С.
    Аннотация. В докладе приводятся варианты условий Гильберта–Бернайса–Леба, работающие в очень общих предположениях относительно рассматриваемой логики. Также исследуется роль правил сокращения и ослабления для вывода второй теоремы Гёделя и строится игрушечный пример формальной системы, основанный на модальной логике типа K4 без правила сокращения, опровергающий формализованный вариант этой теоремы.
  71. осень 2015
  72. 2015.12.10: О полноте модальных логик, расширенных модальностью транзитивного замыкания
    Докладчик: Золин Е.Е., к.ф.-м.н., с.н.с.
    Аннотация. Доклад по совместной работе с И.Б.Шапировским. Известны аксиомы Сегерберга, которые при добавлении к модальной логике K дают полную по Крипке логику K+ с двумя модальностями: одной , отвечающей произвольному отношению R, и другой , отвечающей ее транзитивному замыканию R+. Возникает естественный вопрос: если аксиомы Сегерберга добавлять к произвольной (полной) модальной логике L, то в каких случаях получится полная по Крипке бимодальная логика L+? В докладе будут приведены найденные недавно (2015) достаточные условия на логику L, гарантирующие полноту логики L+. Данные условия являются довольно сильными (что сужает их область применимости) и гарантируют не только полноту, но и разрешимость, и финитную аппроксимируемость логики L+. Будет рассказано также о новом результате о достаточном условии полноты логики вида PDL(Φ), где Φ — некоторое множество полимодальных формул. Будут обсуждаться открытые вопросы в этой области.
  73. 2015.12.03: Полиномиальный алгоритм для формул ограниченной глубины в мультипликативной некоммутативной линейной логике (продолжение)
    Докладчик: Пентус М.Р.
  74. 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.
  75. 2015.11.19: Гибридные модальные логики
    Докладчик: Вахрушева Полина Викторовна, аспирантка, научный руководитель В.Б.Шехтман
    Аннотация. Краткий обзор–введение по гибридным логикам. Доклад основан на главе “Hybrid Logics” авторов Carlos Areces, Balder ten Cate из книги “Handbook of Modal Logic”. Будет приведена аксиоматика основных гибридных логик и доказаны некоторые теоремы о полноте.
  76. 2015.11.12: Итерации медленной непротиворечивости
    Докладчик: Пахомов Ф.Н., к.ф.-м.н., МИАН
    Аннотация. (не HTML-отредактировано) Рекурсивно аксиоматизируемые теории можно сравнивать по силе утверждения о их непротиворечивости Con(T). Хотя имеется ряд контрпримеров, но в случае "естественных" теорий T и U почти всегда оказывается, что либо примитивно рекурсивная арифметика PRA доказывает, что Con(T) влечет Con(U), либо PRA доказывает, что Con(U) влечет Con(T), либо PRA доказывает эквивалентность этих утверждений. Тем самым такое сравнение для "естественных" теорий оказывается линейным. Над теорией PA имеется "естественная" "немного" более сильная теория PA+Con(PA). Но, как оказывается, между этими двумя теориями имеются промежуточные по силе теории.

    В частности, С.Фридманом, М.Ратьеном и А.Вайерманом был предложен относительно "естественный" пример теории в этом промежутке. Теория PA является объединением конечно аксиоматизируемых теорий I?_n (PA со схемой индукции ограниченной на ?_n-формулы) по всем натуральным n. Для теории PA хорошо известен ряд примеров быстрорастущих общерекурсивных функций, чья определенность на всех числах недоказуема в PA, рассмотрим функцию такого рода F_{?_0}. Рассмотрим альтернативный метод перечисления аксиом PA, а именно метод, при котором аксиомы теории I?_n появляются на шаге F_{?_0}(n). Как оказывается, PA не может доказать эквивалентность этой аксиоматизации и стандартной, а утверждение Con(PA_s) о "медленной" непротиворечивости PA (непротиворечивости теории, задаваемой этим альтернативным методом перечисления аксиом) оказывается слабее обычного Con(PA). Теория PA+Con(PA_s) оказывается промежуточной по силе, между PA и PA+Con(PA). Более того, С.Фридмано, М.Ратьеном и А.Вайерманом было показано, что PA доказывает, что для всех ? имеет место ??_s?  ?? (здесь ?? означает Con(PA+?) и ?_s? означает Con(PA_s+?) ). Из чего, в частности, следует, что PA доказывает, что для всех ? и натуральных n имеет место ?_s^n? -> ??. Тем самым, все конечные итерации добавления "медленной" непротиворечивости примененные к PA дают теории более слабые, чем PA+Con(PA).

    Будет рассказано о результате состоящем в том, что PA доказывает, что для всех ? имеет место ?_s^{?_0}?  ??. Отметим, что от сюда непосредственно следует, что трансфинитные итерации добавления "медленной" непротиворечивости к PA дают в зазоре между PA и PA+Con(PA) цепь теорий возрастающей силы длины в точности ?_0.

    Кроме того, будет рассказано о том, что при замене в определение ?_s функции F_{?_0} на другие подходящие функции можно получать эквивалентности ?_s^??  ?? для ?=2 и ?=?.

  77. 2015.11.05: О канонических ультрарасширениях отношений и их топологических характеристиках (продолжение)
    Докладчик: Савельев Денис Игоревич, ИППИ РАН.
  78. 2015.10.29: О канонических ультрарасширениях отношений и их топологических характеристиках
    Докладчик: Савельев Денис Игоревич, ИППИ РАН.
    Аннотация. Известны два способа расширить данное двухместное отношение на множестве $X$ до двухместного отношения на множестве $\beta X$, состоящем из ультрафильтров над $X$. Один способ появился в 70-е гг. в работе Леммона и Скотта по модальной логике, другой — несколько лет назад в работе докладчика по теории моделей. Оба способа являются в определённом смысле каноническими. В докладе будет обсуждаться их соотношение, их взаимодействие с операциями алгебры отношений, а также будут сформулированы их топологические характеристики. Один тип характеристик будет дан в терминах стандартной бикомпактной топологии на множестве $\beta X$ ультрафильтров над $X$, другой — в терминах топологии Вьеториса на множестве замкнутых подмножеств в $\beta X$, которое можно отождествить с множеством фильтров над $X$.
  79. 2015.10.22: О некоторых интервальных временных модальных логиках. Разрешимость, финитная аппроксимируемость (продолжение)
  80. 2015.10.15: О некоторых интервальных временных модальных логиках. Разрешимость, финитная аппроксимируемость
    Докладчик: Чижов Алексей Сергеевич, аспирант ИППИ, научный руководитель В.Б.Шехтман
  81. 2015.10.08: Исчисление Ламбека с (суб)экспоненциальными модальностями (по совместной работе с А. Щедровым и М. Кановичем)
    Докладчик: Кузнецов С.Л., к.ф.-м.н., асс.
    Аннотация Исчисление Ламбека можно рассматривать как вариант некоммутативной линейной логики. Линейная логика имеет также одноместную связку, называемую экспоненциальной, выделяющую формулы, для которых в исчисление добавлены структурные правила (перестановка, сокращение, ослабление), которые не разрешены для произвольных формул. В докладе рассматриваются способы расширения исчисления Ламбека экспоненциальной модальностью с сохранением (не формально, а по существу) «ламбекова ограничения»: левая часть любой секвенции должна быть непустой. Рассматривается также субэкспоненциальная модальность, для которой разрешены только перестановка и сокращение, но не ослабление. Для предлагаемых расширений строятся исчисления генценовского типа и доказывается неразрешимость проблемы выводимости.
  82. 2015.10.01: Исчисление Ламбека с дополнительными аксиомами (по статье В. Бушковского) (продолжение)
  83. 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.

  84. весна 2015
  85. 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.

  86. 2015.05.07: О неразрешимости проблем распознавания для пропозициональных исчислений
    Докладчик: Боков Григорий Владимирович, к.ф.-м.н., м.н.с. кафедры МаТИС.
    Аннотация. В докладе будут рассмотрены следующие проблемы распознавания для пропозициональных исчислений с правилами вывода modus ponens и подстановки: распознавание аксиоматизации, распознавание расширения и распознавание полноты. В частности, будет доказано, что проблема распознавания расширения алгоритмически неразрешима для любого непустого исчисления, а проблемы распознавания аксиоматизации и полноты алгоритмически неразрешимы для любого исчисления, в котором выводима формула x → ( y → x ). Кроме того, в докладе будет приведён исторический обзор известных результатов по данной тематике.
  87. 2015.04.23: О реализации модальности в системе Coq
    Докладчик: Крупский В.Н.
    Аннотация. По работе Christoph Benzmuller & Bruno Woltzenlogel Paleo "Interacting with Modal Logics in the Coq Proof Assistant" (CSR 2015).
  88. 2015.04.09: О категорных моделях квантовой механики, связанных с линейной логикой
    Докладчик: Запрягаев Александр Александрович, студ. 3-го курса, научный руководитель Л. Д. Беклемишев
    Аннотация. В настоящем докладе обсуждается возможность применения аксиоматического подхода к квантовым вычислениям и алгоритмам. Даётся обзор классического подхода в терминах гильбертовых пространств (по Дж. фон Нойману) и устанавливается его ключевой результат — протокол квантовой телепортации. После обсуждения недостатков подобной модели и предлагается новый подход (S. Abramsky / B. Coecke, 2003), базирующийся на идеях современной теории категорий. Рассматриваются как формально-аксиоматический подход, так и метод диаграмм, позволяющий изображать квантовые протоколы в виде наглядных рисунков и являющийся мощным средством нахождения новых протоколов и доказательства тождеств о квантовых системах.
  89. 2015.XX.XX: Несеквенциальное исчисление Ламбека с двумя делениями
    Докладчик: Луговая Валентина Николаевна, Рыжова Анастасия Александровна, студ. 4-го курса, науч. рук. С.Л.Кузнецов.
    Аннотация. Исчисление L было введено И. Ламбеком для описания синтаксиса естественных языков. Это исчисление существует в двух вариантах — секвенциальном (генценовском) и несеквенциальном (гильбертовском). В исчислении Ламбека используются три связки — умножение, левое и правое деления. Естественный интерес представляет фрагмент исчисления Ламбека без операции умножения. В докладе предъявляется гильбертовское исчисление для этого фрагмента и доказывается его эквивалентность генценовскому исчислению.
  90. 2015.03.26: Лексикографические произведения и суммы модальных логик (продолжение)
    Докладчик: Шапировский И.Б.
  91. 2015.03.19: Лексикографические произведения и суммы модальных логик
    Докладчик: Шапировский И.Б.
    Аннотация. Мы будем рассматривать две естественные операции на шкалах Крипке — лексикографическое (или порядковое) произведение и сумму, и соответствующие им операции на модальных логиках. Наша цель — построение аксиоматик возникающих логик. Один конкретный результат такого рода был известен в связи с исследованиями по теории доказательств: в 2007 г. Л. Д. Беклемишев описал аксиоматику суммы нескольких экземпляров логики Гёделя-Лёба GL. Недавно нам удалось доказать несколько общих теорем такого рода, в частности, найти аксиоматики сумм и произведений логик K, K4, S4, S5 и многих других. Доклад основан на совместной работе с Ф. Балбиани и В. Б. Шехтманом.
  92. 2015.03.12: О некоторых медленно терминируемых системах преобразований термов
    Докладчик: Оноприенко Анастасия Александровна, студ. 3-го курса, научный руководитель Л. Д. Беклемишев
    Аннотация. В этой работе мы формулируем простое комбинаторное утверждение, называемое принципом Червя. Это наглядный пример истинной, но недоказуемой в арифметике Пеано PA теоремы. Её доказательство основано на использовании только счётных ординалов, а потому может быть проведено в теории ZFC. На основе принципа Червя мы строим простые системы подстановок термов в логике первого порядка. Число шагов работы таких систем на произвольном входе конечно, но не ограничивается никакой вычислимой функцией от длины входа, доказуемо тотальной в арифметике Пеано PA. Тем самым утверждение о терминируемости этих систем недоказуемо в PA.
  93. 2015.03.05: Бисимуляционные игры и локально табличные модальные логики (продолжение)
    Докладчик: Шехтман В.Б.
  94. 2015.02.26: Логика с модальностью неравенства DL
    Докладчик: Кудинов Андрей Валерьевич, к.ф.-м.н.
  95. 2015.02.19: Бисимуляционные игры и локально табличные модальные логики
    Докладчик: Шехтман В.Б.
  96. осень 2014
  97. 2014.12.11: О некоторых разрешимых финитно неаксиоматизируемых бимодальных логиках (продолжение)
    Докладчик: Матузенко Виктор Сергеевич, аспирант ИППИ, научный руководитель В. Б. Шехтман
  98. 2014.12.04: О некоторых разрешимых финитно неаксиоматизируемых бимодальных логиках
    Докладчик: Матузенко Виктор Сергеевич, аспирант ИППИ, научный руководитель В. Б. Шехтман
    Аннотация. По работе А.Куруш и С.Марселино.
  99. 2014.11.25: Теорема о характеризации для класса конечных шкал логики K×K
    Докладчик: Осипов Илья Игоревич, аспирант ИППИ, научный руководитель В. Б. Шехтман
    Аннотация. В докладе будет изложено доказательство того, что формулы первого порядка, сохраняющие истинность в бимодально эквивалентных конечных моделях логики K×K, — это в точности формулы, семантически эквивалентные в классе конечных шкал логики K×K переводам бимодальных формул.
  100. 2014.11.20: Произведения модальных логик в окрестностной семантике (продолжение)
    Докладчик: Кудинов Андрей Валерьевич, к.ф.-м.н.
  101. 2014.11.13: Произведения модальных логик в окрестностной семантике
    Докладчик: Кудинов Андрей Валерьевич, к.ф.-м.н.
  102. 2014.11.06: Об интуиционистской логике знания
    Докладчик: Крупский В.Н.
  103. 2014.10.30: Об усилении теоремы Крахта
    Докладчик: Пахомов Ф.Н., аспирант МИАН, научный руководитель Л. Д. Беклемишев
    Аннотация. В докладе будет рассказано об усилении теоремы Крахта. Крахт показал, что если кардинал является наименьшей мощностью, в которой имеется модель некоторой счётной теории второго порядка, то существует некоторая модальная логика такая, что этот кардинал равен наименьшей мощности, в которой имеется шкала Крипке, чья логика в точности равна этой модальной логике. Мы усиливаем этот результат, находя искомую модальную логику уже среди расширений S4.
  104. 2014.10.23: О модальных логиках, которым нужны очень большие шкалы
    Докладчик: Пахомов Ф.Н., аспирант, научный руководитель Л. Д. Беклемишев
    Аннотация. Будет разобрана статья М. Крахта “Modal logics that need very large frames”. Будет обсуждаться вопрос о том, какие кардиналы могут быть описаны как наименьшие мощности шкал в классе шкал с некоторой фиксированной модальной логикой. Совокупность таких кардиналов известна как спектр Кузнецова. Как оказывается, спектр Кузнецова может содержать очень большие кардиналы. В частности, если существует недостижимый (слабо компактный, измеримый) кардинал, то в спектре Кузнецова есть кардинал больший первого недостижимого (слабо компактного, измеримого) кардинала. Центральным результатом Крахта является то, что спектр Кузнецова совпадает с совокупностью всех кардиналов, являющихся наименьшими мощностями моделей фиксированных Π11 логик с конечными сигнатурами.
  105. 2014.10.16: Фильтруемость регулярных грамматических модальных логик
    Докладчик: Золин Е.Е., к.ф.-м.н.
    Аннотация. Данный доклад формально является продолжением предыдущего, но фактически от слушателей не будет требоваться знание содержания первой части. Мы расскажем, что такое грамматические модальные логики, в частности, регулярные. Мы покажем, что фильтруемость (определение будет дано) последних, а следовательно, их финитная аппроксимируемость и разрешимость легко получается из (рассказанных в прошлый раз) результатов о том, что операции транзитивного замыкания, объединения и композиции отношений в шкалах Крипке безопасны для фильтруемости. Наконец, мы приведем явные конструкции фильтрации для некоторых естественных семейств регулярных грамматических модальных логик (левосторонних, правосторонних и других). Данный доклад можно также считать дополнением к докладу (прошлого года) Станислава Кикотя о неразрешимых грамматических модальных логиках.
  106. 2014.10.09: Операции на шкалах, сохраняющие фильтруемость
    Докладчик: Золин Е.Е., к.ф.-м.н.
    Аннотация. Совместная работа с И. Шапировским и С. Кикотем. В модальной логике нередко изучается следующий вопрос: можно ли добавить в язык рассматриваемой логики новую модальность, расширив тем самым ее выразительные возможности, но не (сильно) испортив основные свойства логики, такие как полнота, разрешимость, финитная аппроксимируемость и т.п. Мы расскажем о таком свойстве логик, как фильтруемость (в общих чертах это — возможность устанавливать ее разрешимость методом фильтрации); приведем примеры фильтруемых и нефильтруемых (в данном смысле) логик; главное — рассмотрим вопрос о том, добавление каких модальностей (и сооответствующих им операций на отношениях достижимости, или более общо, на шкалах Крипке) сохраняет фильтруемость логики.
  107. 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, и предлагаем естественную классификацию непарадоксальных моделей.
  108. весна 2014
  109. 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.
  110. 2014.04.24: Финитная аппроксимируемость некоторых модальных логик, задаваемых хорновыми формулами
    Докладчик: Заплетин Андрей Максимович, студ. 5-го курса, научные руководители В.Б.Шехтман В.Б. и И.Б.Шапировский
  111. 2014.04.10: Канонические фильтрации и локально табличные модальные логики
    Докладчик: Шехтман В.Б.
  112. 2014.04.03: Алгоритмическая сложность проблемы выполнимости некоторых транзитивных плотных модальных логик
    Докладчик: Чижов Алексей Сергеевич, аспирант ИППИ, научный руководитель В.Б.Шехтман
  113. 2014.03.27: О неполноте в пучках Крипке квантифицированных версий некоторых S4-логик
    Докладчик: Маслов Николай Александрович, аспирант ИППИ, научный руководитель В.Б.Шехтман
    Аннотация. Будет рассказано обобщение результата Silvio Ghilardi, полученного в работе "Incompleteness results in Krilke semantics". Все результаты этой работы могут быть перенесены на случай пучков Крипке.
  114. 2014.03.20: Предикатные аналоги первичной логики Гуревича
    Докладчик: Подгайц Александра Ефремовна, аспирантка, научный руководитель Л.Д.Беклемишев
  115. 2014.03.13: О двух понятиях ультрарасширений бинарных отношений
    Докладчик: Савельев Денис Игоревич, ИППИ РАН.
    Аннотация. Существуют два различных понятия ультрарасширений бинарных отношений. Одно из них было обнаружено в модальной логике и использовано ван Бентемом для получения характеризации модальной определимости. Другое понятие ультрарасширений было недавно введено докладчиком в контексте общей теории моделей (некоторые близкие понятия были известны с 60-х гг. в двух разных областях: теории множеств и комбинаторных задачах алгебры). В докладе будет описано точное соотношение этих двух понятий, а также даны их топологические характеризации.
  116. 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.
  117. 2014.02.27: Проблема распознаваемости аксиоматик модальной логики K
    Докладчик: Золин Е.Е., к.ф.-м.н.
    Аннотация. В докладе будет дан ответ на вопрос о том, существует ли алгоритм, который по произвольному конечному множеству модальных формул распознаёт, даёт ли оно, вместе с тремя правилами вывода: modus ponens, подстановки и усиления, полную аксиоматику модальной логики K. Данный результат получен в 2013 году Чагровым, доказательство упрощено докладчиком. Аналогичным вопросом — (не)распознаваемостью аксиоматик для различных пропозициональных (не модальных) исчислений: классического, интуиционистского, суперинтуиционистских, противоречивого — занимались многие исследователи, начиная с первых работ Поста и Линьяла (1949) и Кузнецова (1963) и заканчивая Боковым (2009), получившим сравнительно краткое и изящное доказательство для классической логики, впоследствии упрощенное и обобщенное докладчиком на суперинтуиционистские локики (2012), а позже усиленное Боковым на импликативные суперинтуиционистские локики (2014).


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

    осень 2013
  119. 2013.12.10: Полнота исчисления Ламбека–Гришина с унарными модальностями относительно реляциононных моделей (продолжение)
    Докладчик: Смуров Иван Михайлович, аспирант, научный руководитель М.Р.Пентус
  120. 2013.12.03: Модальная логика интервалов Халперна–Шохама: происхождение, вычислительная сложность
    Докладчик: Чижов Алексей Сергеевич, аспирант ИППИ, научный руководитель В.Б.Шехтман
    Аннотация. В докладе будет представлена оригинальная работа Халперна–Шохама 1996 года, где вводится логика интервалов на временных структурах. Получены результаты вычислительной сложности для логики с шестью естественными модальностями.
  121. 2013.11.26: Полнота исчисления Ламбека–Гришина с унарными модальностями относительно реляциононных моделей
    Докладчик: Смуров Иван Михайлович, аспирант, научный руководитель М.Р.Пентус
  122. 2013.11.19: Неразрешимость модальных логик, связанных с контекстно-свободными грамматиками
    Докладчик: Кикоть Станислав Павлович, к.ф.-м.н., научный руководитель В.Б.Шехтман
  123. 2013.11.12: Финитная аппроксимирумость некоторых модальных логик, «похожих» на K4
    Докладчик: Заплетин Андрей Максимович, студ. 4-го курса, науч. рук. В.Б.Шехтман и И.Б.Шапировский.
    Аннотация. Будет приведено доказательство финитной аппроксимируемости, а значит, и разрешимости расширения модальной логики K аксиомой □ p → □□□ p. (Результат Д.Габбая 70-х гг).
  124. 2013.11.05: Сети доказательства для исчисления Ламбека и линейной логики
    Докладчик: Кузнецов С.Л., к.ф.-м.н., научный руководитель М.Р.Пентус
  125. 2013.10.29: Каноничность модальной логики S4.1
    Докладчик: Журавлев Александр Алексеевич, студ. 4-го курса, научный руководитель В.Б.Шехтман
  126. 2013.10.22: Теоремы полноты для гибридных логик (продолжение)
    Докладчик: Вахрушева Полина Викторовна, аспирантка, научный руководитель В.Б.Шехтман
  127. 2013.10.15: Теоремы полноты для гибридных логик
    Докладчик: Вахрушева Полина Викторовна, аспирантка, научный руководитель В.Б.Шехтман
  128. 2013.10.08: Некоторые результаты о неразрешимости модальных и интуиционистких предикатных логик с использованием семантики категорий (продолжение)
    Докладчик: Маслов Николай Александрович, аспирант, научный руководитель В.Б.Шехтман
  129. 2013.10.01: Некоторые результаты о неразрешимости модальных и интуиционистких предикатных логик с использованием семантики категорий
    Докладчик: Маслов Николай Александрович, аспирант, научный руководитель В.Б.Шехтман
  130. 2013.09.24: Неразрешимость модальных логик между K×K×K и S5×S5×S5 (продолжение)
    Докладчик: Осипов Илья Игоревич, аспирант ИППИ, научный руководитель В.Б.Шехтман
  131. 2013.09.17: Неразрешимость модальных логик между K×K×K и S5×S5×S5
    Докладчик: Осипов Илья Игоревич, аспирант ИППИ, научный руководитель В.Б.Шехтман
  132. весна 2013
  133. 2013.05.14: Некоторые теоремы о неполноте модальных предикатных логик в семантике Крипке
    Докладчик: Маслов Николай, аспирант, научный руководитель В.Б.Шехтман
  134. 2013.05.07: Временные гибридные логики с модальностями «вчера» и «завтра»
    Докладчик: Вахрушева Полина Викторовна, науч. рук. В.Б.Шехтман.
  135. 2013.04.30: Финитная аппроксимируемость и другие свойства модальной логики K×K×K
    Докладчик: Осипов Илья Игоревич, аспирант ИППИ, научный руководитель В.Б.Шехтман
  136. 2013.04.23: О работах Якуба Михалишина в модальной логике
    Докладчик: Кикоть Станислав Павлович, к.ф.-м.н., научный руководитель В.Б.Шехтман
  137. 2013.04.16: О модальной логике конечноместных операций на топологическом пространстве и итерированной производной Кантора (продолжение)
    Докладчик: Савельев Д.И.
  138. 2013.04.09: Кванторная логика S4 с модальностями “de re” и “de dicto”
    Докладчик: Яворская Т.Л.
  139. 2013.04.02: О модальной логике конечноместных операций на топологическом пространстве и итерированной производной Кантора
    Докладчик: Савельев Д.И.
  140. 2013.03.26: О понятии выразимости модели Крипке в модальной логике
    Докладчик: Золин Е.Е.
    Аннотация. В первой половине доклада (на прошлом заседании семинара) было сформулировано определение понятия, указанного в заголовке доклада, и приведены простейшие примеры его применения. Во второй половине доклада будут рассказаны, с разной степенью подробности, два более серьёзных недавних результата, полученных с использованием данной техники.

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

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

  141. 2013.03.19: О понятии выразимости модели Крипке в модальной логике
    Докладчик: Золин Е.Е.
    Аннотация. Указанное в названии понятие, введенное докладчиком, оказалось удобным инструментом при доказательстве неразрешимости или получении нижних оценок вычислительной сложности различных модальных логик. Оно позволяет представить такое доказательство в виде двух частей, имеющих самостоятельный интерес, что делает доказательство более прозрачным. Будут сформулированы локальный и глобальный варианты данного понятия и приведены некоторые их применения.
  142. 2013.03.12: О логике регионов с булевыми связками
    Докладчик: Матвеева Екатерина Сергеевна, науч. рук. В.Б.Шехтман.
  143. 2013.03.05: Порядковые суммы шкал Крипке
    Докладчик: Шапировский И.Б.
    Аннотация. Всякая шкала (W,R), где отношение R транзитивно, может быть рассмотрена как частично упорядоченное множество своих сгустков (максимальных подмножеств W, в которых отношение универсально). Операция порядковой суммы шкал является обобщением этой несложной конструкции на случай, где вместо сгустков рассматриваются произвольные шкалы. Мы расскажем, как можно проверять выполнимость модальных формул на таких шкалах, и получим простое доказательство разрешимости в полиномиальной памяти для целого ряда расширений K4.
  144. 2013.02.26: Модальные интервальные логики с отношением «включение» (продолжение)
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
  145. 2013.02.19: Модальные интервальные логики с отношением «включение»
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
  146. осень 2012
  147. 2012.12.18: Графы Эрдёша и примеры канонических модальных логик, не определимых никаким элементарным классом шкал (продолжение)
    Докладчик: Маслов Николай Александрович, науч. рук. В.Б.Шехтман.
  148. 2012.12.11: Графы Эрдёша и примеры канонических модальных логик, не определимых никаким элементарным классом шкал
    Докладчик: Маслов Николай Александрович, науч. рук. В.Б.Шехтман.
    Аннотация. Доклад по статье: Robert Goldblatt, Ian Hodkinson, and Yde Venema "Erdős graphs resolve Fine's canonicity problem", Bull. Symbolic Logic 10 no. 2 (June 2004), 186-208. [pdf] Abstract: 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ős that there are finite graphs with arbitrarily large chromatic number and girth.
  149. 2012.12.04: Простое бестиповое лямбда-исчисление
    Докладчик: Мухутдинова Татьяна
  150. 2012.11.27: Нижняя оценка длины совмещающего типа в исчислении Ламбека
    Докладчик: Сорокин Алексей
  151. 2012.11.20: Отсутствие равномерной интерполяции в исчислении Ламбека без умножения
    Докладчик: Смуров Иван Михайлович, науч. рук. М.Р.Пентус
  152. 2012.11.13: Критерий выводимости для исчисления Лабека без умножения
    Докладчик: Смуров Иван Михайлович, науч. рук. М.Р.Пентус
  153. 2012.11.06: О модальных логиках некоторых произведений окрестностных шкал (продолжение)
    Докладчик: Кудинов Андрей Валерьевич
  154. 2012.10.30: Теоремы о полноте и неполноте для тождеств в полурешетках
    Докладчик: Кикоть Станислав Павлович (Лондон)
  155. 2012.10.23: О модальных логиках некоторых произведений окрестностных шкал
    Докладчик: Кудинов Андрей Валерьевич
  156. 2012.10.09: О модальной логике топологической динамики: действия полугрупп
    Докладчик: Савельев Денис Игоревич
  157. 2012.09.25: О произведениях модальных логик с логикой неравенства
    Докладчик: Осипов Илья Игоревич, науч. рук. В.Б.Шехтман.
  158. 2012.09.18: Математическая морфология
    Докладчик: Кузнецов С.Л.
  159. весна 2012
  160. 2012.05.15: Дихотомия среди некоторых элементарно порождённых модальных логик
    Докладчик: Кикоть Станислав Павлович (Лондон)
  161. 2012.04.24: О неразрешимости модальных логик хэмминговых шкал фиксированной конечной размерности больше двух
    Докладчик: Шапировский И.Б.
  162. 2012.04.17: Равномерные оценки и допустимые правила вывода
    Докладчик: Шехтман В.Б.
  163. 2012.04.10: Примеры типов исчисления Ламбека, не имеющих равномерного постинтерполянта
    Докладчик: Смуров Иван Михайлович, науч. рук. М.Р.Пентус
  164. 2012.04.03: Теорема Гольдблатта–Томасона для модальных шкал Крипке
    Докладчик: Маслов Николай Александрович, науч. рук. В.Б.Шехтман.
  165. 2012.03.27: Некоторые обобщения теоремы ван Бентема
    Докладчик: Осипов Илья Игоревич, науч. рук. В.Б.Шехтман.
  166. 2012.03.20: Деривационные модальные логики с модальностью неравенства (продолжение)
    Докладчики: Кудинов А.В., Шехтман В.Б.
  167. 2012.03.13: Деривационные модальные логики с модальностью неравенства
    Докладчики: Кудинов А.В., Шехтман В.Б.
  168. 2012.03.06: Модальная логика с переменными модальностями
    Докладчик: Золин Е.Е.
  169. 2012.02.28: Модальные логики хэмминговых пространств
    Докладчик: Шапировский И.Б.
  170. 2012.02.21: Модальная логика и запросы к базам знаний
    Докладчик: Золин Е.Е.
  171. осень 2011
  172. 2011.12.13: Эволюция регуляторного сигнала экспрессии гена
    Докладчик: Куриленко Владислав Игоревич, науч. рук. В.А.Любецкий.
  173. 2011.11.29: Топологические модальные логики
    Докладчик: Шехтман В.Б.
  174. 2011.11.15: Разрешимые интервальные логики с модальностью «касается»
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
  175. 2011.11.08: L-полнота вариантов исчисления Ламбека
    Докладчик: Звонкин М.М.
  176. 2011.11.01: О числе расширений для соединений модальных логик над S4
    Докладчик: Измайлов Максим
  177. 2011.10.18: Модальная определимость формул первого порядка с несколькими свободными переменными (продолжение)
    Докладчик: Золин Е.Е. (по совместной работе с Кикотем С.П.)
  178. 2011.10.11: Модальная определимость формул первого порядка с несколькими свободными переменными
    Докладчик: Золин Е.Е. (по совместной работе с Кикотем С.П.)
  179. 2011.12.04: О логике доказательств первого порядка (продолжение)
    Докладчик: Яворская Т.Л.
  180. 2011.09.27: О логике доказательств первого порядка
    Докладчик: Яворская Т.Л.
  181. весна 2011
  182. 2011.05.17: Логика доказательств первого порядка
    Докладчик: Яворская Т.Л.
  183. 2011.05.10: Алгоритм построения супердерева по набору деревьев
    Докладчики: Котляров Никита, Куриленко Владислав
  184. 2011.05.03: Аналог теоремы Ван Бентема-Розена для шкал с бинарными предикатами (продолжение)
    Докладчик: Осипов Илья Игоревич, науч. рук. В.Б.Шехтман.
  185. 2011.04.26: Аналог теоремы Ван Бентема-Розена для шкал с бинарными предикатами
    Докладчик: Осипов Илья Игоревич, науч. рук. В.Б.Шехтман.
  186. 2011.04.19: Неразрешимость одной градуированной модальной логики
    Докладчик: Золин Е.Е.
  187. 2011.04.12: Гибридные модальные логики (продолжение)
    Докладчик: Вахрушева Полина Викторовна, науч. рук. В.Б.Шехтман.
  188. 2011.04.05: О предтранзитивных модальных логиках
    Докладчики: Шапировский Илья Борисович, Кудинов Андрей Валерьевич
  189. 2011.03.29: О логиках отрезков вещественной оси (продолжение)
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
  190. 2011.03.22: Гибридные модальные логики
    Докладчик: Вахрушева Полина Викторовна, науч. рук. В.Б.Шехтман.
  191. 2011.03.15: О логиках отрезков вещественной оси
    Докладчик: Чижов Алексей Сергеевич, науч. рук. В.Б.Шехтман.
  192. осень 2010
  193. 2010.11.25: О минимальной логике доказуемости, связанной со 2-й теоремой Геделя
    Докладчик: Беклемишев Л.Д.
  194. 2010.11.18: Позитивные фрагменты полимодальной логики доказуемости
    Докладчик: Дашков Евгений Владимирович, науч. рук. Л.Д.Беклемишев.
  195. 2010.11.11: О предтабличных расширениях логик S4 и K4
    Докладчик: Измайлов Максим, науч. рук. В.Б.Шехтман.
  196. 2010.09.16: Дескрипционные и модальные логики: сходства и различия (продолжение)
    Докладчик: Золин Е.Е.
  197. 2010.09.09: Дескрипционные и модальные логики: сходства и различия
    Докладчик: Золин Е.Е.


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

    осень 2013
  199. 2013.12.12: Интернализация доказательств в обобщенных системах Фреге для классической логики
    Докладчик: Саватеев Ю.В., к.ф.-м.н., научный руководитель М.Р.Пентус
    Аннотация. Будет представлен общий метод интернализации доказательств для формальных систем описания классической логики и описана связь получающихся в результате систем с модальными логиками.
  200. 2013.12.11: О стратегических играх, имеющих определенное решение (online доклад)
    Докладчик: Артёмов С.Н., проф., Нью-Йорк
    Аннотация. В своей диссертации 1950 года Нэш обосновывал введение эквилибриума как решения игры предположением о том, что рациональное решение единственно и может быть выведено игроками из описания правил игры. Мы исследуем это предположение методами эпистемической модальной логики для класса стратегических игр с упорядоченными предпочтениями. Мы показываем, что предположение Нэша верно далеко не всегда, и что доля разрешимых игр стремится к нулю с ростом размера игры. Более того, критерием существования определенного решения является не единственность эквилибриума, а сходимость процесса устранения строго доминированных стратегий.
  201. 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.
  202. 2013.11.07: «Первичная» логика Гуревича–Неемана PL и правило замены подформулы на эквивалентную
    Докладчик: Прохоров И.В., бакалавриат ВШЭ
    Аннотация. Будет рассказан результат о разрешимости за полиномиальное время расширения логики PL слабым правилом замены.
  203. весна 2013
  204. 2013.04.18: Конъюнктивные грамматики в нормальной форме Грейбах и исчисление Ламбека с аддитивными связками
    Докладчик: Кузнецов С.Л.
    Аннотация. Предложенные Охотиным конъюнктивные грамматики — это обобщение контекстно-свободных грамматик добавлением операции «конъюнкция»: если из u1, ..., uk выводится одно и то же слово w и в грамматике есть правило A → u1 & ... & uk, то считается, что слово w выводится из A. Для конъюнктивных грамматик определяется аналог нормальной формы Грейбах; теорема о приведении к этой нормальной форме пока доказана только для случая однобуквенного алфавита. С помощью конъюнктивных грамматик можно задать некоторые нетривиальные языки, например { a4n | n > 0 }. Мы докажем, что язык, порождённый конъюнктивной грамматикой в нормальной форме Грейбах, может быть порождён категориальной грамматикой, основанной на исчислении Ламбека, расширенном операцией пересечения (аддитивной конъюнкцией).
  205. 2013.04.11: Логика первого порядка со связывающим модальностями
    Докладчик: Яворская Т.Л.
  206. 2013.02.21: Автоматы, основанные на моноидах, и теорема Хомского–Шюгценберже
    Докладчик: Сорокин А.А.
  207. осень 2012
  208. 2012.12.02: Арифметическая полнота для позитивной логики равномерной схемы рефлексии
    Докладчик: Беклемишев Л.Д.
    Аннотация. Будет доказана арифметическая полнота позитивной логики для этой модальности (в стиле теоремы Соловея), что решает задачу, оставленную открытой в моём предыдущем докладе на эту тему.
  209. 2012.11.29: Верхняя оценка длины совмещающего типа в исчислении Ламбека
    Докладчик: Сорокин Алексей
  210. 2012.11.15: Об аксиоматизации позитивных логик доказуемости
    Докладчик: Беклемишев Л.Д.
    Аннотация. Позитивные логики доказуемости позволяют интерпретировать пропозициональные переменные не только как индивидуальные арифметические предложения, но и как схемы. Это позволяет рассматривать, в частности, равномерную схему рефлексии как модальность. Будет рассказано о текущих результатах по аксиоматизации позитивных логик доказуемости и вопросах, остающихся открытыми.
  211. осень 2011
  212. 2011.11.10: Интерполяционные свойства логик доказуемости и нормализация термов рефлексивной комбинаторной логики
    Докладчик: Шамканов Д.С.
  213. 2011.11.03: PSpace-полнота замкнутого фрагмента логики доказуемости GLP
    Докладчик: Пахомов Ф.Н.
  214. 2011.10.20: Σ1-предложения и рекурсивно перечислимые множества
    Докладчик: Шавруков В.Ю. (Амстердам)
  215. 2011.10.13: Исчисление Ламбека: открытые проблемы
    Докладчик: Пентус М.Р.
  216. 2011.09.28: Основные понятия теории процессов
    Докладчик: Миронов А.
    Аннотация. Теория процессов является одним из основных математических формализмов, предназначенных для моделирования и верификации вычислительных систем. Ее основы были заложены выдающимся английским математиком Р. Милнером. В докладе будут изложены основные понятия теории процессов, в том числе — алгебраические операции на процессах, понятие наблюдаемого бимоделирования. Кроме того, будет представлен один из вариантов обобщения понятия процесса — процесс с передачей сообщений, а также показано применение этого понятия для решения задач моделирования и верификации телекоммуникационных протоколов.

Собрал информацию: Е.Е.Золин
HTML 4.01   CSS 3