Семинары 2019-2022 гг.

2022 год

Докладчик: Ирина Агаджанян

Название: Π_1^0-сложность некоторых квантифицированных модальных логик

СЛАЙДЫ

Дата: 09.12.2022

Аннотация:

Пусть дана модальная пропозициональная логика L. Рассмотрим следующие логики:
- QLwfin - минимальное предикатное расширение пропозициональной модальной логики класса конечных L-шкал
- QL.bfwfin - минимальное предикатное расширение пропозициональной модальной логики класса конечных L-шкал с постоянными областями

Сложностной класс П_1^0 можно определить так. Множество (в данном случае формул) принадлежит классу П_1^0, если его дополнение рекурсивно перечислимо.

Основной результат, который будет доказан:
Пусть L — одна из пропозициональных модальных логик: K, T, D, K4,K4.3, S4, S4.3, GL, GL.3, Grz, Grz.3, KB, KTB, S5. Тогда монадические фрагменты логик QLwfin и QL.bfwfin являются Π_1^0-сложными, т.е. принадлежат классу Π_1^0.

Источник: Rybakov M., Shkatov D. Algorithmic properties of modal and superintuitionistic logics of monadic predicates over finite frames

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

Докладчик: Александр Грефенштейн

Название: Бескванторная логика для рассуждений о знании и вероятностивыводами

Youtube

Дата: 02.12.2022

Аннотация:

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

Название: Деление на n без аксиомы выбора.

Youtube

Дата: 10.06.2022

Аннотация:

Рассмотрим два множества, А и В. Допустим, что для некоторого натурального числа n существует биекция между Axn и Bxn. Как построить биекцию между А и В, не используя аксиому выбора? Если для некоторого n и любой пары множеств, А и В, из существования биекции между Axn и Bxn следует существование биекции между А и В, то мы говорим, что мы умеем делить на n в кардинальной арифметике ZF. Аналогичное деление на n в ZFC -- вещь несложная и давно известная. А в ZF доказательство возможности такого деления для любого натурального n впервые придумали Адольф Линденбаум и Альфред Тарский в 1949 году. Однако их рассуждения не были опубликованы, и доказательство потерялось. В 1949 году Альфред Тарский опубликовал новое доказательство, но оно довольно сложное (" Cancellation laws in the arithmetic of cardinals"). Джон Хортон Конвей, Петер Доил и Сесил Цю (Cecil Qiu) смогли упроситить это доказательство ("Division by three", 1994; "Division by four", 2015). Об их работах я расскажу в докладе. Кроме этого, я расскажу о том, как можно изменить формулировку деления на n так, что деление перестанет быть возможным (Патрик Лутц, "Conway Can Divide by Three, But I Can’t", 2021). Никаких предварительных знаний для понимания доклада не требуется, однако, для более глубокого понимания, будет полезно знать, что такое аксиома выбора и кардинальная арифметика.

Докладчик: Ирина Агаджанян

Название: PSPACE-трудность константного фрагмента логик на интервале [K, wGrz]

Youtube

СЛАЙДЫ

Дата: 03.06.2022

Аннотация:

Слабая логика Гжегорчика, или wGrz. Работы изучающие её начали появляться не так давно. Эта логика привлекала интерес исследователей, в том числе благодаря своей связи с логиками доказуемости. В рамках данного доклада будет доказано, что wGrz является PSPACE-трудной, а также, что для любой логики, находящейся в интервале [K, wGrz] верно, что ее константный фрагмент, является PSPACE-трудным.

Докладчик: Павел Разумный

Название: О модальной предикатной логике QGL с нефундированными выводами

Youtube

Дата: 20.05.2022

Аннотация:

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

Докладчик: Лукашов Никита

Название: Аксиоматика геометрии оригами (предиката Sym(A, l, B))

Youtube

СЛАЙДЫ

Дата: 13.05.2022

Аннотация:

В 1989 г. J. Justin [Justin, 1989] и H. Huzita [Huzita, 1989] предложили список из шести операций, в соответствии с которыми разрешаются складывать из листа бумаги различные фигурки (по аналогии с построениями циркулем и линейкой). Однако данные положения сегодня нельзя назвать аксиомами в строгом логическом смысле, поэтому возник вопрос о формализации плоскости оригами с точки зрения математической логики. В статье [Beklemishev et al., 2020] предлагается одно из его возможных решений.

Одним из базовых понятий авторы взяли ортогональность двух прямых (которую можно проверить лишь два раза согнув бумагу) и получили, что построенная ими аксиоматика является неразрешимой. Но помимо ортогональности в математике оригами возникает ещё одно естественное отношение – симметрия $Sym(A, l, B)$ двух точек относительно прямой (проверяемая только одним изгибом).

В качестве задачи 1 в [Beklemishev et al., 2020] было предложено найти естественную с точки зрения математики оригами аксиоматику теперь для предиката $Sym(A, l, B)$, и в докладе мною будут предоставлены соотвующие аксиомы.

Литература:

[Huzita, 1989] Huzita, H. (1989). Axiomatic development of origami geometry. In Proceedings of the First International Meeting of Origami Science and Technology, 1989, pages 143–158.

[Justin, 1989] Justin, J. (1989). R ́esolution par le pliage de l’ ́equation du troisieme degr ́e et applications g ́eom ́etriques. In Proceedings of the first international meeting of origami science and technology, pages 251–261. Ferrara, Italy.

[Beklemishev et al., 2020] Beklemishev, L., Dmitrieva, A., and Makowsky, J. (2020). Axiomatizing origami planes.

Докладчик: Степан Шахкаламов

Название: Линейная Логика

Youtube

Дата: 29.04.2022

Аннотация:

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

Литература:

Matsuhiro Okada, An Introduction to Linear Logic: Expressiveness and Phase Semantics, разделы 1-3

Докладчик: Чепасов Анатолий

Название: Допустимость нефундированных доказательств в логике доказуемости GLP.

Youtube

Дата: 22.04.2022

Аннотация:

Полимодальная логика доказуемости GLP, представленная Г. Джапаридзе со счётным числом модальностей, имеет важные приложения в теории доказательств. Нефундированное исчисление GLP_inf допускает счётные деревья доказательств, в которых каждая бесконечной ветка имеет бесконечное число применений правила nec_0. Оказывается, логика GLP допускает нефундированные доказательства, то есть множества доказуемых теорем обычного исчисления GLP и нефундированного совпадают.

Оригинальное доказательство этого факта основано на семантических соображениях. Мы же рассмотрим задачу с синтаксической стороны:

1. научимся конструктивно сводить нефундированное доказательство в логике GLP_inf к фундированному с дополнительным омега-правилом Лёба

2. Сведём утверждение к допустимости омега-правила в обычном фундированной и конечном исчислении GLP.

3. Сведём допустимость правила к фундированности порядка на множестве недоказуемых формул.

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

Докладчик: Александр Грефенштейн

Название: Бескванторная линейная вероятностная логика (в измеримом случае)

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

Докладчик: Степан Г. Кузнецов

Название: Алгебраические семантики интуиционистской логики

Youtube

СЛАЙДЫ

Дата: 04.02.2022

Аннотация:

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

Докладчик: Мирошниченко Елена

Название: Смешанные топо-крипке произведения модальных логик
Дата: 28.01.2022

Youtube

СЛАЙДЫ

Аннотация:

В докладе мы определим произведения топологических пространств со шкалами Крипке и соответствующие этой семантической конструкции произведения модальных логик. Обсудим свойства таких произведениях и то, какие формулы общезначимы в таких произведениях, и как можно аксиоматизировать топо-крипке произведения модальных логик в некоторых случаях. Изложение будет следовать статье Филипа Кремера "Topological-Frame Products of Modal Logics".

Докладчик: Степан Кузнецов

Название: Реляционные модели для исчисления Ламбека с единицей и без

Дата: 21.01.2022

Youtube

СЛАЙДЫ

Аннотация:

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

2021 год

Докладчик: Колмаков Евгений

Название: Предикаты доказуемости и связанные с ними алгебры

Дата: 15.10.2021

Аннотация:

11 декабря 2020

Докладчик: Сергеев Александр

Название: Логика и игры

Аннотация: Теория игр и логика - две близкие науки. В докладе мы рассмотрим их взаимосвязь. Начнём с простых примеров и основных понятий теории игр. Далее покажем, как модальная логика упрощает доказательство теоремы Цермело о детерминированности игр с нулевой суммой.

27 ноября 2020

Докладчик: Чепасов Анатолий

Название: Устранение сечения в исчислении вложенных секвенций для логики доказуемости GLP и его приложения

Аннотация: Полимодальная логика доказуемости GLP, введенная Г. Джапаридзе, имеет важные приложения в теории доказательств. Мы рассмотрим исчисление для данной логики в формализме вложенных секвенций и обсудим теорему об устранении правила сечения. Поскольку логика GLP неполна по Крипке, во многих исследованиях, связанных с данной логикой, используется её полный по Крипке фрагмент, обозначаемый J. В качестве приложения теоремы об устранении сечения, мы приведем синтаксическое доказательство результата о сведении логики GLP к логике J.

20 ноября 2020

Докладчик: Латыпова Юлия

Название: О логиках конечной ширины и их полноте.

Аннотация: Логиками конечной ширины называются логики, содержащие K4 и аксиому ширины n для некоторого натурального n. В 1974 году Кит Файн доказал полноту логик конечной ширины.
Из доказательства Файна следует, что логики конечной ширины полны относительно класса всех своих обратно фундированных шкал. Это позволяет ставить вопрос о полноте логик конечной ширины относительно класса своих обратно фундированных шкал, высота которых ограничена некоторым ординалом. Мы докажем, что логики конечной ширины не финитно аппроксимируемы, и, более того, не полные относительно класса своих обратно фундированных шкал высоты не более ω2.

13 ноября 2020

Докладчик: Разумный Павел
Название: Об интерполяционном свойстве Линдона для интуиционистской логики высказываний

Аннотация: Доклад будет посвящен доказательству интерполяционного свойства Линдона для интуиционистской логики высказываний Int.
В начале мы обсудим семантическое доказательство свойства Линдона для модальной логики S4,
после чего с помощью перевода Гёделя-Тарского установим наличие данного свойства для логики Int.

6 ноября 2020

Докладчик: Запрягаев Александр

Название: Арифметика Бюхи и теорема Кобхэма-Семёнова

Аннотация: На докладе пойдёт речь о представлении множеств, распознаваемых конечными автоматами, формулами в слабых арифметических теориях. Мы покажем, что распознаваемость подмножества N^m чисел, записанных в k-ичной системе счисления, автоматом эквивалентна выразимости с помощью сложения и дополнительной функции "y - наибольшая степень k, на которую делится x." Тем самым, существует серия расширений арифметики Пресбургера (теории натуральных чисел со сложением), естественно соответствующая автоматным подмножествам натурального ряда.
Мы обсудим связанные вопросы алгоритмической разрешимости. Также мы наметим доказательство фундаментальной теоремы Кобхэма-Семёнова, которая связывает определимость при различных основаниях систем счисления k1, k2: если показатели k1 и k2 мультипликативно независимы (т.е. не существует s, t > 0, r > 1 таких, что r^s = k1, r^t = k2), то определимость подмножества N^m независимо в арифметиках Бюхи с показателем k1 и k2 эквивалентна простой определимости в арифметике Пресбургера.

30 октября 2020

Докладчик: Гаицгори Георгий

Название: Вероятностные алгоритмы и вероятностно проверяемые доказательства.

Аннотация: В теории алгоритмов существуют не только детерминированные, но и вероятностные алгоритмы. В этом докладе я дам определение вероятностной машины Тьюринга и расскажу, что такое вероятностные алгоритмы. Я дам определение класса задач BPP (bounded-error, probabilistic, polynomial) и приведу пример задачи, которая решается полиномиальным вероятностным алгоритмом, но не детерминированным. Затем я расскажу о классе вероятностно проверяемых доказательств PCP (probabilistically checkable proofs), расскажу PCP теорему о том, что любое решение задачи в классе NP имеет вероятностно проверяемое доказательство логарифмической сложности случайности, и с помощью этой теоремы докажу, что задача поиска наибольшей клики в графе является NP трудной.

16 октября 2020

Докладчик: Дмитрий Шкатов.

Доклад основан на совместных исследованиях с М. Н. Рыбаковым (ИППИ РАН и ВШЭ)

Название: Алгоритмические свойства предикатных модальных логик структур (N, <) и (N, <=) в языках с ограничениями на число переменных и предикатных букв.

В докладе будут рассмотрены алгоритмические свойства предикатных модальных логик структур (N, <) и (N, <=) в языках с ограничениями на количество переменных и количество и местность предикатных букв. Мы покажем, что эти логики Sigma^1_1 полны в языках с двумя переменными и двумя одноместными предикатными буквами.

9 октября 2020

Докладчик: Шехтман Валентин Борисович (по совместной работе с Шкатовым Д.П.)

Название: Полупроизведения и произведения модальных логик: некоторые перспективы.

Операции полупроизведения и произведения шкал Крипке и модальных логик возникают при изучении логик с несколькими модальностями, а также модальных логик предикатов. Мы рассматриваем полупроизведения и произведения 1-модальных логик с S5.

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

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

2 октября 2020

Докладчик: Слюсарев Владислав

Название: Введение в теорию моделей модальной логики

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

Данный доклад является продолжением доклада "Введение в модальную логику". Он ознакомит слушателя с основными понятиями и утверждениями теории моделей для семантики Крипке. Будут рассмотрены следующие темы:
* Определимые и неопределимые классы шкал Крипке
* Бисимуляция, теорема о бисимуляции
* Операции, сохраняющие общезначимость: несвязные суммы, порождённые подшкалы, p-морфизмы, ультрарасширения
* Критерий Голдблатта-Томасона (без доказательства)
* Определимость в расширенных модальных языках
* Применение задачи определимости в теории графов

25 сентября 2020

Докладчик: Слюсарев Владислав

Название: Введение в модальную логику

Аннотация: Модальная логика, возникшая в начале XX века как формализация модальностей (логических операторов, таких как "необходимо/возможно", "доказуемо/неопровержимо", "всегда/когда-либо" и других), сейчас представляет собой обширную отрасль математической логики, имеющую множество теоретических и практических приложений. В математике изучаются отношения между модальными и классическими логиками (такими как логика первого и второго порядков), а также свойства модальной логики как формальной системы (например, полнота и разрешимость). Семантика Крипке, позволяющая интерпретировать модальные формулы как высказывания о направленных графах, открывает широкие возможности для применения аппарата модальной логики в различных областях, в том числе: верификация программ, семантические сети, запросы к структурированным данным; различные задачи лингвистики и теории игр.

Цель доклада - познакомить слушателей с модальной логикой и семантикой Крипке. Будут рассмотрены следующей темы:
* язык модальной логики
* семантика (модели и шкалы Крипке, их свойства и связь с модальными формулами)
* исчисление (аксиомы и правила вывода)
* канонические шкалы и модели, теорема о полноте
* разрешимость

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

18 сентября 2020

Докладчик: Кузнецов Степан Львович

Название доклада: Звёздочка Клини и бесконечные вычисления

Время: 18 сен 2020 04:20 PM Москва

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

22 мая 2020

Иван Попов выступит с докладом об интуиционистской логике и игре И. Межирова для интуиционистской логики высказываний.

Аннотация доклада: На семинаре мы введем интуиционистскую логику, рассмотрев ее отличия от классической логики. А так же рассмотрим формулировку и доказательство теоремы об игре И. Межирова для интуиционистской логики высказываний (которая была озвучена и доказана в начале 21 века).

15 мая 2020

Михиал Фадин выступит с докладом "Классические результаты теории Рамсея".

Аннотация доклада:

Мы обсудим теорему Рамсея, бесконечную теорему Рамсея, теорему Париса — Харрингтона, теорему Эрдёша-Душника-Миллера, теорему Хиндмана, теорему Ван дер Вардена, а также докажем классическую и бесконечную теоремы Рамсея.

8 мая 2020

Степан Казанин выступит с докладом о гипотезе Артина.

Аннотация доклада: В теории полей типичны утверждения о том, что многочлен невысокой степени от большого числа переменных имеет корень. Теоремы такого типа играют важную роль в теории чисел, и Серж Ленг доказал, что однородное уравнение степени d от n переменных над полем F_p((t)) имеет нетривиальное решение при d^2<n. Оказалось, что для поля Q_p, во многих отношениях сходного с F_p((t)), эта теорема верна не всегда, но верна для достаточно больших p. Исторически первое доказательство этого факта существенно опиралось на аппарат теории моделей. Я расскажу об этом результате, следуя книге Кейслера и Чена «Теория моделей».

24 апреля 2020

Виталий Гулевский выступит с докладом о теореме Гливенко.

Аннотация доклада: Доклад будет посвящён связи интуиционистского исчисления высказываний с классическим. В частности, теореме Гливенко. Доклад основан на лекциях по математической логике и теории алгоритмов («Языки и исчисления» Н.К. Верещагин, А. Шень)

27 марта 2020

Даниил Рогозин выступит с докладом " Семантика накрытий для некоммутативной логики кванталей ".

Аннотация: Кванталь - это полная решётка с бинарной ассоциативной операцией, обладающей свойством непрерывности, то есть, такая операция согласована со всеми верхними гранями. Изначально квантали возникли как расширения понятия локали (полной алгебры Гейтинга) для обобщения таких конструкций, как спектр C*-алгебры. В докладе мы рассмотрим систему накрытий для инфинитарной логики предикатов с произведением и делениями для интерпретации данных некоммутативных связок в духе семантики Крипке-Жояля. Доказательство теоремы о полноте здесь использует пополнение по Дедекинду-Макнейлу и теорему представлении квантали как алгебру, ассоциированную с некоторой системой накрытий. Доклад основан на работе Роберта Гольдблатта "A Kripke-Joyal Semantics for Noncommutative Logic in Quantales".

13 марта 2020

Александр Сергеев выступит с докладом "Бесконечные игры. Игра Банаха-Мазура и игра Гейла-Стюарта".

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

6 марта 2020

Степан Кузнецов выступит с докладом "Модели мультипликативно-аддитивного исчисления Ламбека на решётках синтаксических понятий".

(по работам К. Вурма)

Аннотация: Исчисление Ламбека допускает естественную интерпретацию на алгебре формальных языков, имеет место теорема о полноте (Пентус 1995). Однако расширение исчисления Ламбека операциями объединения и пересечения (т.н. аддитивные операции) уже не обладает свойством полноты относительно языковых моделей, поскольку в этом исчислении не выводится закон дистрибутивности. Решётки синтаксических понятий - это модификация алгебр формальных языков при помощи некоторой операции замыкания, естественной с точки зрения лингвистических приложений. Решётки синтаксических понятий не обязательно дистрибутивны, и относительно них исчисление Ламбека с аддитивными операциями полно (Вурм 2012).

28 февраля 2020

Елена Мирошниченко выступит с докладом "Модальные логики произведений некоторых топологических пространств".

Аннотация: Доклад будет посвящён нахождению модальных логик произведений некоторых пространств. В частности, мы рассмотрим Q×Q, логикой которого оказывается соединение (fusion) S4 и S4. Это довольно красиво получается, если рассматривать так называемые "окрестностные шкалы".

Доклад основан на недавней статье А.В. Кудинова «Modal logic of some products of neighborhood frames»

21 февраля 2020

Арсений Аристархов выступит с докладом "Эпистемическая логика SSL и топология".

Аннотация:

Краткое описание топологической семамантики модальной логики S4, теорема Тарского-МакКинзи.
Бимодальный язык и его топологическая семантика
Примеры моделей
Связь одномодальной и двумодальной логик.
Аксиомы SSL
Аксиомы различных пространств.
Примеры.

14 февраля 2020

Александр Запрягаев выступит с докладом "Гипотеза Виссера об арифметике Пресбургера".

Аннотация:

Рефлексивной называется математическая теория, способная доказать непротиворечивость всех своих конечных подтеорий. Среди известных примеров рефлексивных теорий - арифметика Пеано PA и теория множеств ZFC. Из рефлексивности вытекает невозможность интерпретировать теорию в какой-либо из её конечных подтеорий. В отличие от самой рефлексивности, это чисто теоретико-интерпретационное свойство может быть установлено даже для слабых теорий, не обладающих методами кодирования синтаксиса. А. Виссер высказал гипотезу о том, что это свойство выполняется для арифметики Пресбургера, то есть элементарной теории натурального ряда с операцией сложения, без умножения. Можно заметить, что для этого достаточно доказать,что любая интерпретация PrA в самой себе определимо изоморфна тождественной.

Настоящий доклад сообщает доказательство гипотезы Виссера, полученное докладчиком и Ф. Пахомовым, в многомерном случае (одномерное было получено ранее). Также устанавливается описание линейных порядков, определимых в арифметике Пресбургера, как сужений лексикографического порядка на Z^n на некоторое определимое множество и показывается, как наличие подобного описания существенно упрощает доказательство.

7 февраля 2020

Александр Кильянов "Невычислимые по Тьюрингу функции".

Аннотация: Мы поговорим про вычислимость функций, рассмотрим несколько примеров невычислимых, основным из которых будет Busy Beaver. Доклад будет содержать базовые понятия, связанные с машиной Тьюринга

24 января 2020

Дарья Криницина "Фильтры, фильтрованные произведения и их приложения".

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

17 января 2020

Даня Рогозин "Введение в канонические расширения".

Аннотация: Каноническое расширение - это плотное и компактное пополнение частично-упорядоченной структуры, введенное Йонсенном и Тарским для представления булевых алгебр с операторами, частным случаем которых являются модальные алгебры, алгебры модальных логик. Канонические расширения могут быть применимы не только к булевым алгебрам, но и к более слабыми структурам, таким как частично-упорядоченные множества и решетки. В данном докладе мы обсудим канонические расширения на примере решеток и рассмотрим пример их использования в изучении дистрибутивных модальных логик, логик ограниченных дистрибутивных решеток, расширенных модальными операторами. Доклад основан на статье М. Герке и Дж. Воcмера “A view of canonical extension” и на статье М. Герке, И. Венемы, И. Нагахаши “A Sahlqvist theorem for distributive modal logic”.

2019 год

20 декабрь 2019

Федор Пахомов "О полноте трансфинитных итераций схем рефлексии".

Аннотация: Из второй теормы Гёделя о неполноте следует, что добавление к арифметической теории T утверждения Con(T), выражающего непротиворечивость T, всегда усиливает непротиворечивые теории T. В своей диссертации А. Тьюринг рассмотрел естественное расширение этой идеи - прогрессии теорий T_α получаемых в результате трансфинитной итерации расширения теорий с помощью непротиворечивости (прогрессии Тьюринга), в качестве T₀ можно, например, взять первопорядковую арифметику PA. В связи с такими прогрессиями есть естественный вопрос о том, всякое ли истинное арифметическое утверждение будет доказауемо в T_α для подходящих α. Ответ на этот вопрос отрицателен в общем случае, но положителн для Π₁ предложений. Как было установлено С. Феферманом, для того, чтобы получать произвольные истинные арифметически предложения в подходящих итерациях необходимо вместо непротиворечивости добавлять к теории T схему равномерной рефлексии RFN(T), т.е. схему выражающую тот факт, что всякое T-доказуемое арифметическое предложение истинно. Прогрессии основанные на RFN известны как прогрессии Тьюринга-Фефермана.

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

13 декабря 2019

Глеб Красилич "Обобщение метода Мало для получения больших кардинальных чисел".

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

6 декабря 2019

Оскар Бирзович "Неограниченная теория категорий".

Аннотация: Мы обсудим различные варианты оснований для теории категорий, и увидим, какие при этом возникают сложности и парадоксы. Также я расскажу про опровержение Эрнста гипотезы Фефермана о существовании неограниченных оснований для наивной теории категорий. Для понимания доклада достаточно базового знакомства с теорией множеств и теорией категорий.

Ссылки:
[1] S.Feferman, "Foundations of unlimited category theory: what remains to be done" (The Review of Symbolic Logic, 2013);
[2] M.Ernst, "The prospects of unlimited category theory: doing what remains to be done" (The Review of Symbolic Logic, 2014).

29 ноября 2019

Искандера Шагитовича Калимуллина " Автоматные, примитивно рекурсивные и вычислимые структуры".

Аннотация: Лекция посвящена современным исследованиям по теории вычислимых моделей. Будет сделан обзор как наиболее интересных результатов в этой области, так и современной методологии исследований. Будут приведены примеры использования методов релятивизации и обращения скачка. Эти методы позволяют установить Σ¹₁-полноту (и, следовательно, не-арифметичность) индексного множества автоматно представимых структур.

15 ноября 2019

Андрей Микрюков "Негёделевы расширения PA и их «естественные» представления"

Аннотация: в докладе рассматриваются некоторые теории, доказывающие свою собственную непротиворечивость «естественным» образом, и методы получения таких теорий. Также рассматриваются некоторые попытки формализовать понятия «естественное представление» и «естественная формализация». Повествование опирается на статью “Natural representations and extensions of goedel's second theorem” by Karl-Georg Niebergall (2005).

1 ноября 2019

Даниил Рогозин "Топологическая двойственность для алгебр Гейтинга"

Аннотация: Алгебры Гейтинга - это алгебры интуиционистской логики, которые можно рассматривать как обобщение булевых алгебр. Как хорошо известно из теоремы Стоуна, всякая булева алгебра представима как алгебра открыто-замкнутых множеств некоторого компактного хаусдорфового вполне несвязного пространства. Такие пространства также называются пространствами Стоуна. Более того, категория булевых алгебр двойственно эквивалентна категории пространств Стоуна.

Довольно естественным является вопрос, как устроена топологическая двойственность для алгебр Гейтинга. Мы рассмотрим пространства Эсакиа, специальную разновидность пространств Пристли, и их интересные свойства. После чего мы увидим, что всякая алгебра Гейтинга представима как алгебра открыто-замкнутых множеств некоторого пространства Эсакиа. Если останется время, мы поговорим про более сильный факт: категория алгебр Гейтинга и их гомоморфизмов двойственно эквивалентна категории пространств Эсакиа и непрерывных p-морфизмов.
ВИДЕО

18 октября 2019

Валентин Борисович Шехтман "Бисимуляционные игры и их применение в модальной логике"

Аннотация: Бисимуляционные игры возникли в модальной логике для анализа моделей Крипке и теоретической информатике для изучения абстрактных систем переходов. В докладе будет дан обзор результатов из модальной логики, которые доказываются с помощью бисимуляционных игр: о нормальной форме, финитной аппроксимируемости и локальной табличности.
ВИДЕО

11 октября 2019

Раджаб Агамов "Введение в модальную логику"

Аннотация: Модальная логика как и математическая логика возникла в начале 20-го века, но имела в большей степени философскую мотивировку. Исследователи из математики, философии, информатики, лингвистики, политологии и экономики работают над разнообразными модальными логиками, фокусируясь на множестве различных тем с множеством совершенно разных приложений. Математики подходят к этой области преимущественно с теоретико-модельной точки зрения. Для философов модальная логика является мощным инструментом для семантики. Многие понятия в философии языка могут быть формализованы в модальной логике. Люди которые занимаются компьютерными науками с другой стороны, используют модальную логику для представления программ. Model checking и временная логика являются очень популярными областями компьютерных наук, в которых широко используются модальные логики.

Целью данного доклада является знакомство с базовыми понятиями и результатами в области модальной логики и базовой техникой: модели и шкалы Крипке, p-морфизмы, порожденные подмодели и если успеем каноническая модель.

ВИДЕО

27 сентября 2019

Станислав Кикоть "О (монотонной) определенности рекурсивных запросов относительно производных таблиц"

Аннотация: В первой части доклада я расскажу о задачах определенности и монотонной определенности формулы-запроса над набором формул для производных таблиц, о полученных в Оксфорде результатах в этой области и об открытых вопросах. Во второй части доклада я покажу, как эти задачи можно решать при помощи интерполяций Крейга и Линдона и попробую организовать мозговой штурм одного из открытых вопросов при помощи циклических выводов('производная таблица' - мой вольный перевод слова view).

13 сентября 2019

Степан Кузнецов "Бесконечные и циклические выводы для алгебр Клини и их расширений"

Аннотация: Понятие алгебры Клини естественным образом обобщает два класса алгебр - алгебру формальных языков и алгебру бинарных отношений, с операцией итерации ("звёздочка Клини"). Другие две операции - умножение (конкатенация на языках и композиция на отношениях) и объединение. В докладе будет рассказано об аксиоматизации эквациональных теорий (т.е. множеств всех общезначимых тождеств) в алгебрах Клини и их расширениях с помощью операций пересечения и делений. Мы начнём с аксиоматизаций с помощью омега-правила и с помощью нефундированных выводов, а потом перейдём к циклическим выводам, моделирующим правила индукции. В присутствии делений индуктивные аксиоматизации оказываются неполными (W. Buszkowski 2007) и при этом неразрешимыми (S. Kuznetsov 2019). Для чистой алгебры Клини индуктивная аксиоматизация полна (D. Kozen 1994), однако задача построения для её эквациональной теории циклического исчисления без сечения нетривиальна (A. Das, D. Pous 2017). На этом докладе будет дан только обзор основных результатов и некоторые примеры; наиболее интересные результаты можно будет разобрать в деталях на будущих заседаниях семинара.

14 июня 2019

Николай Почекай "Теория типов Мартина Лёфа"

Аннотация: Я расскажу о синтаксисе теории зависимых типов Мартина Лёфа. Если останется время, то также расскажу о её категорной семантике.

7 июня 2019

Елизавета Нестерова "О циклических выводах в модальном мю-исчислении"

Доклад подготовлен по первой половине статьи Bahareh Afshari, Graham E. Leigh "Cut-free Completeness for Modal Mu-Calculus"

17 мая 2019

Анна Дмитриева "Теорема Зиглера о неразрешимости некоторых теорий полей"

Аннотация: В данном докладе я перескажу статью Мартина Зиглера "Some Undecidable Field Theories" 1980 года. При помощи построения некоторого специального поля, будет доказано, что любая конечная подтеория полной теории действительных или комплексных чисел является неразрешимой. Так же, если останется время, мы обсудим, какие результаты о неразрешимости некоторых теорий геометрии можно отсюда получить.

19 апреля 2019

Евгения Колмакова "Об изоморфизмах алгебр доказуемости"

Аннотация: Как известно, алгебра Линденбаума формальной системы не отражает теоретико-доказательственную силу этой системы. Действительно, для любых двух достаточно сильных перечислимых непротиворечивых теорий соответствующие им алгебры Линденбаума являются счётными безатомными булевыми алгебрами и поэтому изоморфны. Обогащение алгебры Линденбаума унарным оператором доказуемости в данной формальной теории приводит к понятию алгебры доказуемости для этой теории. Такие структуры позволяют выразить многие факты о доказуемости и отличить разные по силе теории (в частности, алгебры доказуемости для теорий PA и ZF неизоморфны). В докладе будет приведено достаточное условие изоморфизма алгебр доказуемости, а также построены нетривиальные автоморфизмы таких алгебр. Доклад основан на статье В. Ю. Шаврукова "Isomorphisms of Diagonalizable Algebras".

ВИДЕО

12 апреля 2019

Владимир Горячев "Теорема Руйтенбурга"

Аннотация: Рассмотрим пропозициональную формулу A=A_0 и зафиксируем в ней переменную x. Построим последовательность формул A_n, где A_k получается из A_k-1 подстановкой A вместо x. Теорема Руйтенбурга утверждает, что полученная последовательность будет заключительно периодической с периодом два с точностью до доказуемой эквивалентности в интуиционистской логике. В докладе я расскажу план доказательства этой теоремы.

ВИДЕО

22 марта 2019

Александр Запрягаев "Интерпретации линейных порядков и себя в арифметике Пресбургера"
Продолжение доклада
ВИДЕО

15 марта 2019

Александр Запрягаев "Интерпретации линейных порядков и себя в арифметике Пресбургера"
ВИДЕО

Аннотация: Арифметика Пресбургера (PrA), введённая М. Пресбургером в 1929, является элементарной теорией натурального ряда с операцией сложения без умножения. В отличие от арифметики Пеано, она полна и разрешима, до достаточно богата, чтобы обладать схемой индукции. В связи с этим естественно возникает вопрос об исследовании её свойств в сравнении с известными свойствами более богатых теорий.
Арифметика Пеано или ZFC являются рефлексивными теориями, то есть доказывающими непротиворечивость каждой из своих конечно аксиоматизируемых подтеорий. Известно, что все секвенциальные теории с полной схемой индукции в своём языке также являются рефлексивными. Из рефлексивности следует невозможность интерпретировать теорию ни в одной из своих конечно аксиоматизируемых подтеорий, что можно считать следом рефлексивности для более слабых теорий с принципом индукции, недостаточно выразительных для формализации утверждения о непротиворечивости: в частности, арифметики Пресбургера. А. Виссер предложил найти ответ, возможна ли такая интерпретация для конкретных слабых арифметик.
Настоящий доклад посвящён работе докладчика (с Ф. Пахомовым) по исследованию интерпретаций в арифметике Пресбургера. Известно, что для выполнения гипотезы Виссера о несуществовании достаточно показать отсутствие интерпретаций PrA в себе, нкроме определимо изоморфных тождественной. Однако, в отличие от PA, PrA не способна кодировать m-ки натуральных чисел одним числом, поэтому принципиально различаются одномерных и многомерный случаи. Eстественно возникает задача об описании линейных порядков, интерпретируемых в PrA. Было установлено, что все порядки, определимые в PrA, являются разреженными.
На основе модификации ранга Кантора-Бендиксона было показано, что все линейные порядки, интерпретируемые m-мерно в PrA, имеют модифицированный ранг m или ниже. На основании этой теоремы было получено доказательство гипотезы Виссера в одномерном случае, а также то, что все интерпретации в многомерном случае изоморфны тождественной, но неясно, определимо ли. Заключительная часть доклада будет посвящена прогрессу в данном вопросе, а также в поиске необходимого и достаточного условия на линейные порядки, определимые в любом числе измерений, с полным описанием двумерного случая.

1 марта 2019

Степан Кузнецов "Глубинное устранение сечения".
ВИДЕО

Аннотация: Теорема об устранении сечений ("Hauptsatz" Генцена) - один из фундаментальных результатов теории доказательств. Обыкновенно синтаксическое доказательство устранимости сечения сталкивается с трудностями при переносе сечения через правило сокращения. Генцен обходит эту проблему путём замены правила сечения (Schnitt) на более общее правило смешения (Mischung). Мы изложим другой подход [Braüner, de Paiva 1996] к устранению сечения в системах с правилом сокращения, на примере линейной логики с экспоненциальной модальностью. Этот подход можно назвать глубинным устранением сечения. Мы также покажем, как метод глубинного устранения сечения помогает в случаях, когда сформулировать правило смешения затруднительно, - в системах с ограниченной ассоциативностью [Kanovich et al. 2017].

22 февраля 2019

Продолжение доклада Петра Огарка. По техническим причинам видеозапись этого семинара отсутствует.

15 февраля 2019

Петр Огарок "Эквивалентность циклической арифметики и арифметики Пеано"
ВИДЕО

Аннотация: Циклические доказательства – это способ построения формальных доказательств в логиках с индуктивными определениями в виде циклических графов, наглядно представляющих доказаетльства методом "бесконечного спуска". Легко показать, что они обобщают обычные доказательства по индукции. Нетривиальным является вопрос, является ли класс утверждений, доказуемых циклическими выводами, более широким. Я расскажу решение этого вопроса в специальном случае: циклическая формулировка арифметики первого порядка совпадает с обычной арифметикой Пеано. В основном я буду следовать статье 2017 года Alex Simpson, Cyclic Arithmetic Is Equivalent to Peano Arithmetic.

8 февраля 2019

Кудинов А.В. "Динамическая эпистемическая логика."

1 февраля 2019

Пахомов Ф.Н. "О границах применимости второй теоремы Гёделя о неполноте." - Продолжение.
ВИДЕО

25 января 2019

Пахомов Ф.Н. "О границах применимости второй теоремы Гёделя о неполноте"
ВИДЕО

Аннотация: Часто вторую теорему Гёделя о неполноте формулируют в узкой форме, как утверждение о том, что какая-то конкретная формальная теория (например PA или ZFC) не может доказать собственную непротиворечивость. Тем не менее, даже формулировка данная самим Гёделем в его статье 1931 года имела большую общность и покрывала все непротиворечивые расширения его базисной системы P примитивно-рекурсивными множествами аксиом. В настоящем докладе я сделаю обзор результатов отвечающих на вопрос о том, на какие теории можно обобщить вторую теорему Гёделя о неполноте. Нестрогая мотивирующая формулировка второй теоремы о неполноте говорит, что никакая достаточно сильная непротиворечивая теория не может доказать собственную непротиворечивость. Для того, чтобы сделать такую формулировку строгим математическим утверждением во-первых нужно описать класс теорий которые будут считаться достаточно сильными. Но кроме того, как оказывается, в отличие от таких сильных теорий как PA и ZFC для слабых теорий гораздо острее встает вопрос о том, какие формулы языка теории следует считать формализациями утверждениями о непротиворечивости. Я расскажу о нескольких различных подходов к тому, как именно производить такие уточнения. Кроме того, я расскажу, о примерах теорий, которые могут доказать собственную непротиворечивость и тем самым ограничивают то, насколько вторая теорема Гёделя может быть обобщена.

Нашли опечатку?
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!
Сервис предназначен только для отправки сообщений об орфографических и пунктуационных ошибках.