| академик РАН академик РАН |
Лев Дмитриевич Беклемишев
Алексей Львович Семёнов |
Видеозаписи докладов на YouTube
С. А. Мелиховым была введена в рассмотрение совместная логика задач и высказываний QHC. В логике QHC каждая формула имеет один из двух сортов: высказывание либо задача. Формулы сорта высказывание представляют собой «классическую часть» логики QHC — а именно, для них выполнены все законы классической логики. Формулы сорта задача представляют собой «интуиционистскую часть» логики QHC — для них выполнены все законы интуиционистской логики. Формулы сорта высказывание и сорта задача в логике QHC связаны между собой двумя модальностями ? и !, меняющими сорт формул.
В докладе будет дан обзор основных результатов диссертационной работы докладчика, касающейся совместной логики задач и высказываний QHC. Подробно изучены различные варианты семантики пропозиционального фрагмента логики QHC - логики HC: алгебраическая семантика, реляционная семантика, топологическая семантика. Для всех представленных в работе классов моделей имеет место теорема о полноте и свойство конечных моделей (тем самым установлена разрешимость логики HC). Получен ответ на вопрос, поставленный С. А. Мелиховым, о соотношении ED-принципа и PC-правила. Построена семантика типа Крипке логики QHC и доказана теорема о сильной полноте этой логики относительно предлагаемой семантики. Установлено, что логика QHC является консервативным расширением интуиционистской модальной логики QH4. Доказаны дизъюнктивное и экзистенциальное свойства логики QHC (для формул сорта задача).
Во-первых, рассматривается понятие доказуемой n-доказуемости, являющееся вариацией одного из важных сильных понятий доказуемости. В отличие от множества всех n-доказуемых формул, т.е. доказуемых в обычном смысле в данной теории, расширенной множеством всех истинных Πn-предложений, совокупность формул, утверждение об n-доказуемости которых может быть доказано средствами некоторой перечислимой метатеории, образует перечислимую теорию. В работе найдены естественные рекурсивные аксиоматизации таких теорий в терминах итерированных схем локальной рефлексии, что позволило установить ряд свойств введенных теорий. Помимо этого исследуется вопрос об ускорении доказательств для исходных аксиоматизаций этих теорий по отношению к найденным.
Во-вторых, вводятся новые варианты принципов, выражающих корректность данной теории, а именно, схемы рефлексии с определимыми параметрами, и устанавливается их соотношение с известными формами рефлексии. На этой основе дается новое теоретико-модельное доказательство результата о консервативности между схемами равномерной и локальной рефлексии. Кроме того, исследуется естественным образом возникший вопрос о теоретико-доказательственной силе так называемой теоремы Фефермана, связанной с понятием 1-доказуемости и схемой локальной рефлексии.
В-третьих, изучаются вопросы изоморфизма алгебр доказуемости формальных теорий. Как известно, предикат доказуемости данной арифметической теории индуцирует на булевой алгебре Линденбаума этой теории некоторый унарный оператор, что приводит к понятию алгебры доказуемости данной теории. В работе усиливается знаменитый результат В.Ю. Шаврукова, дающий достаточное условие неизоморфизма алгебр доказуемости для пары арифметических теорий. Полученное усиление позволяет построить ряд новых интересных примеров пар теорий с неизоморфными алгебрами доказуемости.
In this talk I will speak about a recent line of work that connects cyclic proofs to KA and certain extensions. I will show how a natural non-wellfounded system can be made regular via enriching the syntax of usual sequents to a form of 'hypersequent'. This takes advantage of several basic techniques on the cyclic proof side as well as known normal forms from automaton theory.
As an application, I will explain how to recover an alternative demonstration of Kozen's and Krob's result, as well as a later strengthening to so-called 'left-handed' KAs, due to Boffa '95 (cf. also Kozen & Silva '12).
[1] Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. LICS 1991.
[2] M. Boffa. Une condition impliquant toutes les identites rationnelles.
Theoretical Informatics and Applications 29(6), 515-518, 1995. (in French)
[3] Dexter Kozen, Alexandra Silva. Left-handed completeness. RAMICS 2012.
Доклад основан на результатах, вошедших в диссертационную работу докладчика: автореферат.
Важным вопросом является сложность проверки свойств таких протоколов, как в общем случае, так и для ограниченных подклассов протоколов. Протоколы на популяциях связаны с сетями Петри, поэтому недавняя неэлементарная нижняя оценка на сложность достижимости в сетях Петри автоматически порождает некоторые нижние оценки для общего случая. В докладе будут приведены результаты о вычислительной сложности разных вопросов о протоколах на популяциях, часть из которых получена докладчиком.
Этот вопрос был чрезвычайно актуален после того, как Разборов (1985) показал, что некоторая монотонная булева функция из класса NP не может быть вычислена схемой полиномиального размера в монотонном базисе. Если бы наличие схемы полиномиального размера в стандартном полном базисе влекло наличие схемы полиномиального размера в монотонном базисе (для монотонных функций), то из результата Разборова вытекало бы, что P не равно NP! Однако Разборов же (позже в 1985) доказал, что одно не всегда влечет другое, так что доказать неравенство P и NP таким способом не получится.
Вместо монотонных функций мы рассмотрели аналогичный вопрос для класса самодвойственных функций (т.е. функций, принимающих противоположные значения в противоположных точках булева куба), и там ситуация оказалась противоположной. Стандартный базис для этого класса состоит из функции голосования от 3 переменных и отрицания. Мы показали, что если самодвойственная функция имеет схему полиномиального размера в стандартном полном базисе, то эта функция имеет и схему полиномиального размера в стандартном самодвойственном базисе. Доказан также аналогичный результат о переходе от схем в монотонном базисе к схемам в базисе, состоящим из одной лишь функции голосования от 3 переменных (для функций, являющимися одновременно монотонными и самодвойственными). Отметим, что эти результаты верны не только для размера, но и для глубины схем.
Мы применяем наш результат к функции голосования от n переменных при нечетном n (это функция монотонна и самодвойственна). Для этой функции давно известна явная конструкция схемы логарифмической по n глубины в монотонном базисе. Благодаря нашему результату отсюда извлекается явная схема логарифмической по n глубины, состоящая только из функций голосования от 3 переменных. У этого результата имеются следствия в области протоколов конфиденциального вычисления (Кохен и др. 2013). Для схем, состоящих только из функций голосования от 3 переменных, ранее была известна лишь неявная конструкция (Вэлиент, 1984).
Помимо функции голосования, мы изучаем также другие пороговые функции, получая для них усиления известных результатов. Здесь вместо теорем о переходе от одних схем к другим нам потребовались другие технические инструменты, а именно коммуникационная сложность. Мы получили новый результат о переходе от коммуникационных протоколов к булевым схемам, обобщающий известный результат Карчмера и Вигдерсона (1991).
По совместной работе с В. Подольским (ССС 2020)
Обструкцией назовем слово, не являющееся подсловом в A, всякое подслово которого уже является подсловом A.
Мы покажем [1], что количество обструкций длины не более n в равномерно рекуррентном слове не меньше log3 n.
[1] Igor Melnikov and Ivan Mitrofanov. On cogrowth function of uniformly recurrent sequences. 2020. https://arxiv.org/abs/2001.02272
После краткого обзора унивалентных оснований математики внимание будет сосредоточено на проблемах, возникающих в связи с доказательствами, традиционное понимание которых затруднено или невозможно по причине их длины и сложности. Будут приведены примеры; позиции докладчика будут критически сопоставлены с положениями известного провокационного текста Николая Вавилова [2].
В заключение будут высказаны соображения о формализации преподаваемой математики.
[1] Homotopy Type Theory: Univalent Foundations for Mathematics.
Univalent Foundations Project, Institute for Advanced Study, 2013.
(465 pages)
arXiv: 1308.0729
[2] Nikolai Vavilov. Reshaping the metaphor of proof.
Philosophical Transactions of the Royal Society A. Mathematical,
Physical, and Engineering Sciences, 2019.
DOI: 10.1098/rsta.2018.0279
Гипотеза чувствительности утверждает, что эти две величины полиномально связаны, то есть каждая из них выражается как полином от другой. Эта гипотеза оставалась открытой с 1992 года и была доказана летом 2019 года в работе Хао Хуанг [1]. Доказательство при этом оказалось совсем несложным. В докладе мы расскажем об этой гипотезе и о связях ее с другими вопросами в теории сложности вычислений. Если позволит время, будет также рассказана идея доказательства.
[1] Hao Huang. Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture. July 2019, arXiv.
[1] S. Kuznetsov. The logic of action lattices is undecidable. LICS 2019, IEEE, 2019, 9 pp.
(pdf)
[2] S. Kuznetsov. Action logic is undecidable. 2019,
arXiv:1912.11273
[3] S. Kuznetsov. *-continuity vs. induction: divide and conquer.
AiML vol. 12, College Publications, 2018, pp. 439-510.
(pdf)
[4] S. Kuznetsov. The Lambek calculus with iteration: two variants.
WoLLIC 2017, LNCS vol. 10388, Springer, 2017, pp. 182-198.
(arXiv:1705.07309)
Доклад посвящен доказательству этой гипотезы, предложенному недавно авторами совместно с Дж.-Т. Ю в статьях [1] и [2]. Конструкции в доказательстве используют приложения теории моделей, в частности, элементы нестандартного анализа. <!-- Доклад посвящен доказательству гипотезы Концевича (2005) об изоморфизме между группой автоморфизмов алгебры Вейля Wn и группой полиномиальных симплектоморфизмов аффинного пространства размерности 2n в характеристике нуль, предложенному недавно авторами совместно с Дж.-Т. Ю в статьях [1] и [2]. Конструкции в доказательстве используют приложения теории моделей, в частности, элементы нестандартного анализа. -->
В докладе будут сформулированы необходимые определения из алгебры и элементов теории моделей. Далее будет проведено построение гомоморфизма Φ: Aut Wn,ℂ → Aut Pn,ℂ (биективность которого устанавливается в [1]), основанное на процедуре редукции по модулю бесконечно большого простого числа, а также рассмотрен вопрос о независимости этого построения от выбора ультрафильтра на множестве индексов и бесконечно большого простого [2]. Также предполагается обсудить связь гипотезы Концевича с проблемой якобиана.
[1] Alexei Kanel-Belov, Andrey Elishev, Jie-Tai Yu.
Augmented polynomial symplectomorphisms and quantization,
2018, arXiv
[2] Alexei Kanel-Belov, Andrey Elishev, Jie-Tai Yu.
Independence of the B-KK isomorphism of infinite prime,
2019, arXiv
Для случая слабой монадической теории эта проблема была решена С. Ф. Сопруновым в 1988 году [2]. Для элементарного и монадического случая полного решения проблемы неизвестно.
В докладе будет изложено принадлежащее С. Ф. Сопрунову решение проблемы для случая элементарных теорий произвольных структур, обогащающих порядок на натуральных числах [3,4]. Будет доказано, что у всякой разрешимой (то есть имеющей разрешимую теорию) структуры (ℕ,Σ), где конечная сигнатура Σ содержит предикат < (или в которой он выразим), существует обогащение (одноместным предикатом, не выразимым в сигнатуре Σ), также являющееся разрешимым.
[1] Elgot C., Rabin M. Decidability and undecidability of extensions of second (first) order theory of
(generalized) successor. Journal of Symbolic Logic, 1966, vol. 31, no. 2, pp. 169–181.
[2] Сопрунов С.Ф. Разрешимые обогащения структур. Вопросы кибернетики, 1988, вып. 134, с. 175–179.
[3] Soprunov S. An infinite branch in a decidable tree.
22 Mar 2018.
arXiv:1801.00423.
[4] Soprunov S. There is no maximal decidable expansion of the (ℕ,{<}) structure.
20 Nov 2019.
arXiv:1911.09059.
Начиная с работ Колмогорова, можно проследить возможность перевода математических утверждений между тремя «языками» — вероятностным, комбинаторным и сложностным. В докладе предполагается краткий обзор основных результатов в этом направлении, а также более подробный разбор недавнего результата: применение «шума» (каждый бит слова с небольшой вероятностью меняется) увеличивает энтропию/сложность/размер — это неформальное утверждение будет сформулировано на этих трёх языках и объяснено, как переход от одного языка к другому позволяет получить его доказательство.
Этот же метод позволяет построить негиперболическую группу с неположительной кривизной, не содержащую ℤ×ℤ в качестве подгруппы.
Так, вопрос о существовании примитивно рекурсивных копий алгебраических структур оказывается связанным с понятиями копируемых и диагонализируемых классов структур, введенными А. Монталбаном (2013). Проблема описания структур, имеющих примитивно рекурсивные (автоматные) копии, в некотором смысле оказывается эквивалентной проблеме описания 0'-вычислимых структур, имеющих вычислимые копии.
С другой стороны, вопросы примитивно рекурсивной сложности алгебраических структур и отношений на них оказывается связанным со значениями беcкванторных формул, в параметры которых подставляются попарно различные элементы структуры. Кроме того, структуры, между копиями которых изоморфизм находится равномерно примитивно рекурсивно, образует специальный класс счетно-категоричных структур, имеющий чисто теоретико-модельное описание.
Коммуникационная сложность отличается от этого тем, что вход разрезается на две части и делится между двумя игроками, Алисой и Бобом. Их задача та же — вычислить значение f. За единицу времени им разрешается послать один бит от одного игрока к другому. Считая, что любые локальные вычисления бесплатны (не занимают совсем никакого времени), насколько быстро мы теперь можем вычислить f? Эта величина и называется коммуникационной сложностью функции f.
В вопросной сложности вход снова дается нам целиком. При этом бесплатны любые операции, кроме чтения битов входа (чтение одного бита занимает единицу времени).
Наконец, информационная сложность определяется также, как и коммуникационная, за исключением того, что посылка одного бита может занимать меньше единицы времени. Например, случайный бит, независимый от входов игроков, может быть послан бесплатно. В общем случае время на посылку бита пропорционально количеству информации, которое содержится в этом бите о входе посылающего (строго это количество информации определяется при помощи энтропии Шеннона).
Теоремы, связывающие коммуникационную и вопросную сложность, оказываются полезны в схемной сложности. Рассмотрение информационной сложности позволяет отвечать на некоторые вопросы в коммуникационной сложности. Будет рассказано о результатах докладчика на эти темы.
Ситуация проста для 3-, 4- и 6-угольника (все невырожденные траектории периодичны), исследована для 5- и 10-угольника. Автор получил результаты для 8- и 12-угольника.
В докладе пойдет речь о том, как устроены периодические, апериодические и вырожденные точки, периоды и периодические слова точек, как соответствующие множества точек расположены на плоскости, и почему компьютер оказался практически необходимым для полноценного исследования.
(i) derivations lead only to true sequents;
(ii) cut free proofs may be non-elementary shorter than cut free LK proofs.
This research is based on properties of Hilbert's epsilon calculus and is part of efforts to complement Hilber's stepwise concept of proof by useful global concepts. We use these ideas to provide analytic calculi for Henkin quantifiers and demonstrate soundness, (cut free) completeness and cut elimination. Furthermore, we show that, in the case of quantifier macros such as Henkin quantifiers for a partial semantics, global calculi are the only option to preserve analyticity.
Своими воспоминаниями о В. А. Успенском также поделились (ссылки на соответствующие моменты видеозаписи):
• акад. Сергей Иванович Адян
(включая комментарий к зачитанному
А. Л. Семеновым
поздравлению
с 60-летием проф. Н. К. Верещагина,
ученика В. А. Успенкого),
• акад. Алексей Львович Семёнов,
• проф. Владимир Михайлович Тихомиров,
• проф. Елена Наумовна Зарецкая,
• проф. Екатерина Владимировна Рахилина.
В докладе будут приведены примеры существенно второпорядковых условий, которые позволяют получить:
(а) бесконечные классы предикатных модальных (и суперинтуиционистских) неперечислимых логик и неполных по Крипке исчислений;
(б) примеры полных по Крипке рекурсивно аксиоматизируемых предикатных модальных логик, которые не полны относительно первопорядково определимых классов шкал (и/или классов порождённых корневых шкал).
Если останется время, то будут представлены результаты, связанные с неразрешиостью и неперечислимостью модальных и суперинтуиционистских предикатных логик в языке с одной одноместной предикатной буквой и малым числом (2-3) предметных переменных.
В докладе будет дан обзор результатов о сложности в терминах количества состояний для разных видов автоматов и приведены некоторые новые результаты.
We will survey some uncomputability and characterization results in this setting: domino problem, language, entropies, traces, periods, quasiperiods, Kolmogorov complexity, Turing degrees. If time permits, we will conclude with open questions, especially in the larger setting of Cayley graphs.
