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

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

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


    весна 2016
  1. 2016.03.10: Доказательство гипотезы Виссера-Зутхаута об интерпретациях арифметики Пресбургера в себя
    Докладчик: Запрягаев А.А., студ. 4-го курса, научный руководитель Л. Д. Беклемишев
    Аннотация. А. Виссер (Утрехт) предложил рассмотреть вопрос описания всех одномерных интерпретаций без параметров арифметики Пресбургера в себя и выдвинул гипотезу о том, что все такие интерпретации доказуемо изоморфны тождественной, что влечёт также невозможность интерпретировать арифметику Пресбургера ни в одной из своих конечно аксиоматизируемых подтеорий. Будет представлено полученное автором доказательство гипотезы Виссера–Зутхаута. Функция, осуществляющая изоморфизм интерпретации арифметики Пресбургера в себя тождественной, будет построена, согласно идее к.ф.-м.н. Ф.Н.Пахомова, на основе анализа интерпретированного отношения порядка. Также будет продемонстрирована неожиданная связь с задачей Улама–Коллатца о последовательности «3n+1».
  2. 2016.03.03: Абстрактные варианты второй теоремы Гёделя о неполноте для логик слабее классической (продолжение)
  3. 2016.02.25: Абстрактные варианты второй теоремы Гёделя о неполноте для логик слабее классической
    Докладчики: Л.Д.Беклемишев, Д.С.Шамканов
    Аннотация. В докладе приводятся варианты условий Гильберта–Бернайса–Леба, работающие в очень общих предположениях относительно рассматриваемой логики. Также исследуется роль правил сокращения и ослабления для вывода второй теоремы Гёделя и строится игрушечный пример формальной системы, основанный на модальной логике типа K4 без правила сокращения, опровергающий формализованный вариант этой теоремы.
  4. осень 2015
  5. 2015.12.10: О полноте модальных логик, расширенных модальностью транзитивного замыкания
    Докладчик: Золин Е.Е., к.ф.-м.н., с.н.с.
    Аннотация. Доклад по совместной работе с И.Б.Шапировским. Известны аксиомы Сегерберга, которые при добавлении к модальной логике K дают полную по Крипке логику K+ с двумя модальностями: одной , отвечающей произвольному отношению R, и другой , отвечающей ее транзитивному замыканию R+. Возникает естественный вопрос: если аксиомы Сегерберга добавлять к произвольной (полной) модальной логике L, то в каких случаях получится полная по Крипке бимодальная логика L+? В докладе будут приведены найденные недавно (2015) достаточные условия на логику L, гарантирующие полноту логики L+. Данные условия являются довольно сильными (что сужает их область применимости) и гарантируют не только полноту, но и разрешимость, и финитную аппроксимируемость логики L+. Будет рассказано также о новом результате о достаточном условии полноты логики вида PDL(Φ), где Φ — некоторое множество полимодальных формул. Будут обсуждаться открытые вопросы в этой области.
  6. 2015.12.03: Полиномиальный алгоритм для формул ограниченной глубины в мультипликативной некоммутативной линейной логике (продолжение)
  7. 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.
  8. 2015.11.19: Гибридные модальные логики
    Докладчик: Вахрушева Полина, аспирантка, научный руководитель В.Б.Шехтман
    Аннотация. Краткий обзор–введение по гибридным логикам. Доклад основан на главе “Hybrid Logics” авторов Carlos Areces, Balder ten Cate из книги “Handbook of Modal Logic”. Будет приведена аксиоматика основных гибридных логик и доказаны некоторые теоремы о полноте.
  9. 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 и ?=?.

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

  17. весна 2015
  18. 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.

  19. 2015.05.07: О неразрешимости проблем распознавания для пропозициональных исчислений
    Докладчик: Боков Григорий Владимирович, к.ф.-м.н., м.н.с. кафедры МаТИС
    Аннотация. В докладе будут рассмотрены следующие проблемы распознавания для пропозициональных исчислений с правилами вывода modus ponens и подстановки: распознавание аксиоматизации, распознавание расширения и распознавание полноты. В частности, будет доказано, что проблема распознавания расширения алгоритмически неразрешима для любого непустого исчисления, а проблемы распознавания аксиоматизации и полноты алгоритмически неразрешимы для любого исчисления, в котором выводима формула x → ( y → x ). Кроме того, в докладе будет приведён исторический обзор известных результатов по данной тематике.
  20. 2015.04.23: О реализации модальности в системе Coq
    Докладчик: Крупский В.Н.
    Аннотация. По работе Christoph Benzmuller & Bruno Woltzenlogel Paleo "Interacting with Modal Logics in the Coq Proof Assistant" (CSR 2015).
  21. 2015.04.09: О категорных моделях квантовой механики, связанных с линейной логикой
    Докладчик: Запрягаев А.А., студ. 3-го курса, научный руководитель Л. Д. Беклемишев
    Аннотация. В настоящем докладе обсуждается возможность применения аксиоматического подхода к квантовым вычислениям и алгоритмам. Даётся обзор классического подхода в терминах гильбертовых пространств (по Дж. фон Нойману) и устанавливается его ключевой результат — протокол квантовой телепортации. После обсуждения недостатков подобной модели и предлагается новый подход (S. Abramsky / B. Coecke, 2003), базирующийся на идеях современной теории категорий. Рассматриваются как формально-аксиоматический подход, так и метод диаграмм, позволяющий изображать квантовые протоколы в виде наглядных рисунков и являющийся мощным средством нахождения новых протоколов и доказательства тождеств о квантовых системах.
  22. 2015.XX.XX: Несеквенциальное исчисление Ламбека с двумя делениями
    Докладчик: Луговая В.Н., Рыжова А.А., студ. 4-го курса, научный руководитель С. Л. Кузнецов
    Аннотация. Исчисление L было введено И. Ламбеком для описания синтаксиса естественных языков. Это исчисление существует в двух вариантах — секвенциальном (генценовском) и несеквенциальном (гильбертовском). В исчислении Ламбека используются три связки — умножение, левое и правое деления. Естественный интерес представляет фрагмент исчисления Ламбека без операции умножения. В докладе предъявляется гильбертовское исчисление для этого фрагмента и доказывается его эквивалентность генценовскому исчислению.
  23. 2015.03.26: Лексикографические произведения и суммы модальных логик (продолжение)
  24. 2015.03.19: Лексикографические произведения и суммы модальных логик
    Докладчик: Шапировский И.Б.
    Аннотация. Мы будем рассматривать две естественные операции на шкалах Крипке — лексикографическое (или порядковое) произведение и сумму, и соответствующие им операции на модальных логиках. Наша цель — построение аксиоматик возникающих логик. Один конкретный результат такого рода был известен в связи с исследованиями по теории доказательств: в 2007 г. Л. Д. Беклемишев описал аксиоматику суммы нескольких экземпляров логики Гёделя-Лёба GL. Недавно нам удалось доказать несколько общих теорем такого рода, в частности, найти аксиоматики сумм и произведений логик K, K4, S4, S5 и многих других. Доклад основан на совместной работе с Ф. Балбиани и В. Б. Шехтманом.
  25. 2015.03.12: О некоторых медленно терминируемых системах преобразований термов
    Докладчик: Оноприенко Анастасия, студ. 3-го курса, научный руководитель Л. Д. Беклемишев
    Аннотация. В этой работе мы формулируем простое комбинаторное утверждение, называемое принципом Червя. Это наглядный пример истинной, но недоказуемой в арифметике Пеано PA теоремы. Её доказательство основано на использовании только счётных ординалов, а потому может быть проведено в теории ZFC. На основе принципа Червя мы строим простые системы подстановок термов в логике первого порядка. Число шагов работы таких систем на произвольном входе конечно, но не ограничивается никакой вычислимой функцией от длины входа, доказуемо тотальной в арифметике Пеано PA. Тем самым утверждение о терминируемости этих систем недоказуемо в PA.
  26. 2015.03.05: Бисимуляционные игры и локально табличные модальные логики (продолжение)
    Докладчик: Шехтман В.Б.
  27. 2015.02.26: Логика с модальностью неравенства DL
    Докладчик: Кудинов А.В., к.ф.-м.н.
  28. 2015.02.19: Бисимуляционные игры и локально табличные модальные логики
    Докладчик: Шехтман В.Б.
  29. осень 2014
  30. 2014.12.11: О некоторых разрешимых финитно неаксиоматизируемых бимодальных логиках (продолжение)
  31. 2014.12.04: О некоторых разрешимых финитно неаксиоматизируемых бимодальных логиках
    Докладчик: Матузенко Виктор, аспирант ИППИ, научный руководитель В. Б. Шехтман
    Аннотация. По работе А.Куруш и С.Марселино.
  32. 2014.11.25: Теорема о характеризации для класса конечных шкал логики K×K
    Докладчик: Осипов Илья, аспирант ИППИ, научный руководитель В. Б. Шехтман
    Аннотация. В докладе будет изложено доказательство того, что формулы первого порядка, сохраняющие истинность в бимодально эквивалентных конечных моделях логики K×K, — это в точности формулы, семантически эквивалентные в классе конечных шкал логики K×K переводам бимодальных формул.
  33. 2014.11.20: Произведения модальных логик в окрестностной семантике (продолжение)
  34. 2014.11.13: Произведения модальных логик в окрестностной семантике
    Докладчик: Кудинов А.В., к.ф.-м.н.
  35. 2014.11.06: Об интуиционистской логике знания
    Докладчик: Крупский В.Н.
  36. 2014.10.30: Об усилении теоремы Крахта
    Докладчик: Пахомов Ф.Н., аспирант МИАН, научный руководитель Л. Д. Беклемишев
    Аннотация. В докладе будет рассказано об усилении теоремы Крахта. Крахт показал, что если кардинал является наименьшей мощностью, в которой имеется модель некоторой счётной теории второго порядка, то существует некоторая модальная логика такая, что этот кардинал равен наименьшей мощности, в которой имеется шкала Крипке, чья логика в точности равна этой модальной логике. Мы усиливаем этот результат, находя искомую модальную логику уже среди расширений S4.
  37. 2014.10.23: О модальных логиках, которым нужны очень большие шкалы
    Докладчик: Пахомов Ф.Н., аспирант, научный руководитель Л. Д. Беклемишев
    Аннотация. Будет разобрана статья М. Крахта “Modal logics that need very large frames”. Будет обсуждаться вопрос о том, какие кардиналы могут быть описаны как наименьшие мощности шкал в классе шкал с некоторой фиксированной модальной логикой. Совокупность таких кардиналов известна как спектр Кузнецова. Как оказывается, спектр Кузнецова может содержать очень большие кардиналы. В частности, если существует недостижимый (слабо компактный, измеримый) кардинал, то в спектре Кузнецова есть кардинал больший первого недостижимого (слабо компактного, измеримого) кардинала. Центральным результатом Крахта является то, что спектр Кузнецова совпадает с совокупностью всех кардиналов, являющихся наименьшими мощностями моделей фиксированных Π11 логик с конечными сигнатурами.
  38. 2014.10.16: Фильтруемость регулярных грамматических модальных логик
    Докладчик: Золин Е.Е., к.ф.-м.н.
    Аннотация. Данный доклад формально является продолжением предыдущего, но фактически от слушателей не будет требоваться знание содержания первой части. Мы расскажем, что такое грамматические модальные логики, в частности, регулярные. Мы покажем, что фильтруемость (определение будет дано) последних, а следовательно, их финитная аппроксимируемость и разрешимость легко получается из (рассказанных в прошлый раз) результатов о том, что операции транзитивного замыкания, объединения и композиции отношений в шкалах Крипке безопасны для фильтруемости. Наконец, мы приведем явные конструкции фильтрации для некоторых естественных семейств регулярных грамматических модальных логик (левосторонних, правосторонних и других). Данный доклад можно также считать дополнением к докладу (прошлого года) Станислава Кикотя о неразрешимых грамматических модальных логиках.
  39. 2014.10.09: Операции на шкалах, сохраняющие фильтруемость
    Докладчик: Золин Е.Е., к.ф.-м.н.
    Аннотация. Совместная работа с И. Шапировским и С. Кикотем. В модальной логике нередко изучается следующий вопрос: можно ли добавить в язык рассматриваемой логики новую модальность, расширив тем самым ее выразительные возможности, но не (сильно) испортив основные свойства логики, такие как полнота, разрешимость, финитная аппроксимируемость и т.п. Мы расскажем о таком свойстве логик, как фильтруемость (в общих чертах это — возможность устанавливать ее разрешимость методом фильтрации); приведем примеры фильтруемых и нефильтруемых (в данном смысле) логик; главное — рассмотрим вопрос о том, добавление каких модальностей (и сооответствующих им операций на отношениях достижимости, или более общо, на шкалах Крипке) сохраняет фильтруемость логики.
  40. 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, и предлагаем естественную классификацию непарадоксальных моделей.
  41. весна 2014
  42. 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.
  43. 2014.04.24: Финитная аппроксимируемость некоторых модальных логик, задаваемых хорновыми формулами
    Докладчик: Заплетин Андрей, студ. 5-го курса, научные руководители В.Б.Шехтман В.Б. и И.Б.Шапировский
  44. 2014.04.10: Канонические фильтрации и локально табличные модальные логики
    Докладчик: Шехтман В.Б.
  45. 2014.04.03: Алгоритмическая сложность проблемы выполнимости некоторых транзитивных плотных модальных логик
    Докладчик: Чижов Алексей, аспирант ИППИ, научный руководитель В.Б.Шехтман
  46. 2014.03.27: О неполноте в пучках Крипке квантифицированных версий некоторых S4-логик
    Докладчик: Маслов Николай, аспирант ИППИ, научный руководитель В.Б.Шехтман
    Аннотация. Будет рассказано обобщение результата Silvio Ghilardi, полученного в работе "Incompleteness results in Krilke semantics". Все результаты этой работы могут быть перенесены на случай пучков Крипке.
  47. 2014.03.20: Предикатные аналоги первичной логики Гуревича
    Докладчик: Подгайц Александра, аспирантка, научный руководитель Л.Д.Беклемишев
  48. 2014.03.13: О двух понятиях ультрарасширений бинарных отношений
    Докладчик: Савельев Д.И., ИППИ РАН
    Аннотация. Существуют два различных понятия ультрарасширений бинарных отношений. Одно из них было обнаружено в модальной логике и использовано ван Бентемом для получения характеризации модальной определимости. Другое понятие ультрарасширений было недавно введено докладчиком в контексте общей теории моделей (некоторые близкие понятия были известны с 60-х гг. в двух разных областях: теории множеств и комбинаторных задачах алгебры). В докладе будет описано точное соотношение этих двух понятий, а также даны их топологические характеризации.
  49. 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.
  50. 2014.02.27: Проблема распознаваемости аксиоматик модальной логики K
    Докладчик: Золин Е.Е., к.ф.-м.н.
    Аннотация. В докладе будет дан ответ на вопрос о том, существует ли алгоритм, который по произвольному конечному множеству модальных формул распознаёт, даёт ли оно, вместе с тремя правилами вывода: modus ponens, подстановки и усиления, полную аксиоматику модальной логики K. Данный результат получен в 2013 году Чагровым, доказательство упрощено докладчиком. Аналогичным вопросом — (не)распознаваемостью аксиоматик для различных пропозициональных (не модальных) исчислений: классического, интуиционистского, суперинтуиционистских, противоречивого — занимались многие исследователи, начиная с первых работ Поста и Линьяла (1949) и Кузнецова (1963) и заканчивая Боковым (2009), получившим сравнительно краткое и изящное доказательство для классической логики, впоследствии упрощенное и обобщенное докладчиком на суперинтуиционистские локики (2012), а позже усиленное Боковым на импликативные суперинтуиционистские локики (2014).


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

    осень 2013
  1. 2013.12.10: Полнота исчисления Ламбека–Гришина с унарными модальностями относительно реляциононных моделей (продолжение)
    Докладчик: Смуров Иван, аспирант, научный руководитель М.Р.Пентус
  2. 2013.12.03: Модальная логика интервалов Халперна–Шохама: происхождение, вычислительная сложность
    Докладчик: Чижов Алексей, аспирант ИППИ, научный руководитель В.Б.Шехтман
    Аннотация. В докладе будет представлена оригинальная работа Халперна–Шохама 1996 года, где вводится логика интервалов на временных структурах. Получены результаты вычислительной сложности для логики с шестью естественными модальностями.
  3. 2013.11.26: Полнота исчисления Ламбека–Гришина с унарными модальностями относительно реляциононных моделей
    Докладчик: Смуров Иван, аспирант, научный руководитель М.Р.Пентус
  4. 2013.11.19: Неразрешимость модальных логик, связанных с контекстно-свободными грамматиками
    Докладчик: Кикоть С.П., к.ф.-м.н., научный руководитель В.Б.Шехтман
  5. 2013.11.12: Финитная аппроксимирумость некоторых модальных логик, «похожих» на K4
    Докладчик: Заплетин Андрей, студ. 4-го курса, научные руководители В.Б.Шехтман и И.Б.Шапировский
    Аннотация. Будет приведено доказательство финитной аппроксимируемости, а значит, и разрешимости расширения модальной логики K аксиомой □ p → □□□ p. (Результат Д.Габбая 70-х гг).
  6. 2013.11.05: Сети доказательства для исчисления Ламбека и линейной логики
    Докладчик: Кузнецов С.Л., к.ф.-м.н., научный руководитель М.Р.Пентус
  7. 2013.10.29: Каноничность модальной логики S4.1
    Докладчик: Журавлев Александр, студ. 4-го курса, научный руководитель В.Б.Шехтман
  8. 2013.10.22: Теоремы полноты для гибридных логик (продолжение)
  9. 2013.10.15: Теоремы полноты для гибридных логик
    Докладчик: Вахрушева Полина, аспирантка, научный руководитель В.Б.Шехтман
  10. 2013.10.08: Некоторые результаты о неразрешимости модальных и интуиционистких предикатных логик с использованием семантики категорий (продолжение)
  11. 2013.10.01: Некоторые результаты о неразрешимости модальных и интуиционистких предикатных логик с использованием семантики категорий
    Докладчик: Маслов Николай, аспирант, научный руководитель В.Б.Шехтман
  12. 2013.09.24: Неразрешимость модальных логик между K×K×K и S5×S5×S5 (продолжение)
  13. 2013.09.17: Неразрешимость модальных логик между K×K×K и S5×S5×S5
    Докладчик: Осипов Илья, аспирант ИППИ, научный руководитель В.Б.Шехтман
  14. весна 2013
  15. 2013.05.14: Некоторые теоремы о неполноте модальных предикатных логик в семантике Крипке
    Докладчик: Маслов Николай, аспирант, научный руководитель В.Б.Шехтман
  16. 2013.05.07: Временные гибридные логики с модальностями «вчера» и «завтра»
    Докладчик: Вахрушева Полина
  17. 2013.04.30: Финитная аппроксимируемость и другие свойства модальной логики K×K×K
    Докладчик: Осипов Илья, аспирант ИППИ, научный руководитель В.Б.Шехтман
  18. 2013.04.23: О работах Якуба Михалишина в модальной логике
    Докладчик: Кикоть С.П., к.ф.-м.н., научный руководитель В.Б.Шехтман
  19. 2013.04.16: О модальной логике конечноместных операций на топологическом пространстве и итерированной производной Кантора (продолжение)
    Докладчик: Савельев Д.И.
  20. 2013.04.09: Кванторная логика S4 с модальностями “de re” и “de dicto”
    Докладчик: Яворская Т.Л.
  21. 2013.04.02: О модальной логике конечноместных операций на топологическом пространстве и итерированной производной Кантора
    Докладчик: Савельев Д.И.
  22. 2013.03.26: О понятии выразимости модели Крипке в модальной логике
    Докладчик: Золин Е.Е.
    Аннотация. В первой половине доклада (на прошлом заседании семинара) было сформулировано определение понятия, указанного в заголовке доклада, и приведены простейшие примеры его применения. Во второй половине доклада будут рассказаны, с разной степенью подробности, два более серьёзных недавних результата, полученных с использованием данной техники. В первом, полученном докладчиком, утверждается неразрешимость некоторой (градуированной) модальной логики с одной модальностью (т.е. одним отношением в шкале Крипке). Второй результат касается нижней оценки сложности некоторой модальной логики (так же с одной модальностью); данный результат получен Ian Pratt-Hartmann в 2009 г, доказательство упрощено докладчиком.
  23. 2013.03.19: О понятии выразимости модели Крипке в модальной логике
    Докладчик: Золин Е.Е.
    Аннотация. Указанное в названии понятие, введенное докладчиком, оказалось удобным инструментом при доказательстве неразрешимости или получении нижних оценок вычислительной сложности различных модальных логик. Оно позволяет представить такое доказательство в виде двух частей, имеющих самостоятельный интерес, что делает доказательство более прозрачным. Будут сформулированы локальный и глобальный варианты данного понятия и приведены некоторые их применения.
  24. 2013.03.12: О логике регионов с булевыми связками
    Докладчик: Матвеева Екатерина
  25. 2013.03.05: Порядковые суммы шкал Крипке
    Докладчик: Шапировский И.Б.
    Аннотация. Всякая шкала (W,R), где отношение R транзитивно, может быть рассмотрена как частично упорядоченное множество своих сгустков (максимальных подмножеств W, в которых отношение универсально). Операция порядковой суммы шкал является обобщением этой несложной конструкции на случай, где вместо сгустков рассматриваются произвольные шкалы. Мы расскажем, как можно проверять выполнимость модальных формул на таких шкалах, и получим простое доказательство разрешимости в полиномиальной памяти для целого ряда расширений K4.
  26. 2013.02.26: Модальные интервальные логики с отношением «включение» (продолжение)
  27. 2013.02.19: Модальные интервальные логики с отношением «включение»
    Докладчик: Чижов Алексей
  28. осень 2012
  29. 2012.12.18: Графы Эрдёша и примеры канонических модальных логик, не определимых никаким элементарным классом шкал (продолжение)
  30. 2012.12.11: Графы Эрдёша и примеры канонических модальных логик, не определимых никаким элементарным классом шкал
    Докладчик: Маслов Николай
    Аннотация. Доклад по статье: 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.
  31. 2012.12.04: Простое бестиповое лямбда-исчисление
    Докладчик: Мухутдинова Татьяна
  32. 2012.11.27: Нижняя оценка длины совмещающего типа в исчислении Ламбека
    Докладчик: Сорокин Алексей
  33. 2012.11.20: Отсутствие равномерной интерполяции в исчислении Ламбека без умножения
    Докладчик: Смуров Иван
  34. 2012.11.13: Критерий выводимости для исчисления Лабека без умножения
    Докладчик: Смуров Иван
  35. 2012.11.06: О модальных логиках некоторых произведений окрестностных шкал (продолжение)
    Докладчик: Кудинов А.В.
  36. 2012.10.30: Теоремы о полноте и неполноте для тождеств в полурешетках
    Докладчик: Кикоть С.П. (Лондон)
  37. 2012.10.23: О модальных логиках некоторых произведений окрестностных шкал
    Докладчик: Кудинов А.В.
  38. 2012.10.16:
  39. 2012.10.09: О модальной логике топологической динамики: действия полугрупп
    Докладчик: Савельев Д.И.
  40. 2012.10.02:
  41. 2012.09.25: О произведениях модальных логик с логикой неравенства
    Докладчик: Осипов Илья
  42. 2012.09.18: Математическая морфология
    Докладчик: Кузнецов С.Л.
  43. весна 2012
  44. 2012.05.15: Дихотомия среди некоторых элементарно порождённых модальных логик
    Докладчик: Кикоть С.П. (Лондон)
  45. 2012.04.24: О неразрешимости модальных логик хэмминговых шкал фиксированной конечной размерности больше двух
    Докладчик: Шапировский И.Б.
  46. 2012.04.17: Равномерные оценки и допустимые правила вывода
    Докладчик: Шехтман В.Б.
  47. 2012.04.10: Примеры типов исчисления Ламбека, не имеющих равномерного постинтерполянта
    Докладчик: Смуров Иван
  48. 2012.04.03: Теорема Гольдблатта–Томасона для модальных шкал Крипке
    Докладчик: Маслов Николай
  49. 2012.03.27: Некоторые обобщения теоремы ван Бентема
    Докладчик: Осипов Илья
  50. 2012.03.20: Деривационные модальные логики с модальностью неравенства (продолжение)
  51. 2012.03.13: Деривационные модальные логики с модальностью неравенства
    Докладчики: Кудинов А.В., Шехтман В.Б.
  52. 2012.03.06: Модальная логика с переменными модальностями
    Докладчик: Золин Е.Е.
  53. 2012.02.28: Модальные логики хэмминговых пространств
    Докладчик: Шапировский И.Б.
  54. 2012.02.21: Модальная логика и запросы к базам знаний
    Докладчик: Золин Е.Е.
  55. осень 2011
  56. 2011.12.13: Эволюция регуляторного сигнала экспрессии гена
    Докладчик: Куриленко В.И.
  57. 2011.12.06:
  58. 2011.11.29: Топологические модальные логики
    Докладчик: Шехтман В.Б.
  59. 2011.11.22:
  60. 2011.11.15: Разрешимые интервальные логики с модальностью «касается»
    Докладчик: Чижов Алексей
  61. 2011.11.08: L-полнота вариантов исчисления Ламбека
    Докладчик: Звонкин М.М.
  62. 2011.11.01: О числе расширений для соединений модальных логик над S4
    Докладчик: Измайлов Максим
  63. 2011.10.18: Модальная определимость формул первого порядка с несколькими свободными переменными (продолжение)
  64. 2011.10.11: Модальная определимость формул первого порядка с несколькими свободными переменными
    Докладчик: Золин Е.Е. (по совместной работе с Кикотем С.П.)
  65. 2011.12.04: О логике доказательств первого порядка (продолжение)
  66. 2011.09.27: О логике доказательств первого порядка
    Докладчик: Яворская Т.Л.
  67. весна 2011
  68. 2011.05.17: Логика доказательств первого порядка
    Докладчик: Яворская Т.Л.
  69. 2011.05.10: Алгоритм построения супердерева по набору деревьев
    Докладчики: Котляров Никита, Куриленко Владислав
  70. 2011.05.03: Аналог теоремы Ван Бентема-Розена для шкал с бинарными предикатами (продолжение)
  71. 2011.04.26: Аналог теоремы Ван Бентема-Розена для шкал с бинарными предикатами
    Докладчик: Осипов Илья
  72. 2011.04.19: Неразрешимость одной градуированной модальной логики
    Докладчик: Золин Е.Е.
  73. 2011.04.12: Гибридные модальные логики (продолжение)
    Докладчик: Вахрушева Полина
  74. 2011.04.05: О предтранзитивных модальных логиках
    Докладчики: Шапировский И.Б., Кудинов А.В.
  75. 2011.03.29: О логиках отрезков вещественной оси (продолжение)
    Докладчик: Чижов Алексей
  76. 2011.03.22: Гибридные модальные логики
    Докладчик: Вахрушева Полина
  77. 2011.03.15: О логиках отрезков вещественной оси
    Докладчик: Чижов Алексей
  78. осень 2010
  79. 2010.11.25: О минимальной логике доказуемости, связанной со 2-й теоремой Геделя
    Докладчик: Беклемишев Л.Д.
  80. 2010.11.18: Позитивные фрагменты полимодальной логики доказуемости
    Докладчик: Дашков Евгений
  81. 2010.11.11: О предтабличных расширениях логик S4 и K4
    Докладчик: Измайлов Максим
  82. 2010.09.16: Дескрипционные и модальные логики: сходства и различия (продолжение)
  83. 2010.09.09: Дескрипционные и модальные логики: сходства и различия
    Докладчик: Золин Евгений


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

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

HTML 4.01   CSS 3