Летняя школа «Логика, лингвистика и формальная философия 2025»
Репортаж о летней школе «Логика, лингвистика и формальная философия 2025».
Школа прошла в рамках проекта "Международное академическое сотрудничество" - "Плюралистические взгляды на логику и формальную философию".
Курс Cергея Одинцова «Конструктивные семантики и IF-логика»
Пятую летнюю школу «Логика, лингвистика и формальная философия» открыл Сергей Одинцов с логико-математическим курсом лекций на тему «Конструктивные семантики и IF-логика». В первой части своего мини-курса лектор подробно рассказал об истории создания и сущности Independence-Friendly First Order Logic (IF-FOL или дружественной к независимости первопорядковой логики), разработанной Яакко Хинтиккой в статье 1996 года «The Principles of Mathematics Revisited». Язык данной первопорядковой логики, рассмотренной Сергеем Одинцовым, включает в себя: индивидные переменные, константы, функциональные символы, имена предикатных символов, связки из классической логики высказывания, а также кванторы всеобщности и существования.
В ходе первой лекции были представлены доказательства теорем, раскрывающих важные свойства логики IF-FOL. Так, Сергей Одинцов показал, что для этой логики верна теорема компактности Мальцева, теорема Бета об определимости, а также, что она обладает свойством Левенгейма-Сколема. Лектор подробно рассказал о теоретико-игровой семантике (GTS) из двух игроков Элоизы и Абеляра или верификатора и фальсификатора в традиции Хинтикки. Экстенсивная win-lose игра в рамках такой семантики будет представлена кортежем (N, H, Z, P, u), где: N – множество, чьи элементы мы называем игроками; H – множество конечных последовательностей, называемых историями или попросту ходов в игре; Z – множество терминальных историй без продолжения/следующего хода; P – функция игрока, которая по любой нетерминальной истории показывает ход какого игрока следующий; u – функция выигравшего, демонстрирующая победителя по каждой терминальной истории. В играх с неполной информации также появится отношение эквивалентности на истории, благодаря которым некоторые истории для игроков станут неразличимы.
Во второй лекции Сергей Одинцов подробней остановился на особенностях интуиционистских логик. Лектор рассказал про проект логики Колмогорова, взявшего за основу исчисление Гильберта 1923 года. Колмогоров предложил свой перевод из классической логики высказываний в интуиционистскую логику. Перед переменными ставилось двойное отрицание, а для более сложных формул связка переносилась через трансляцию, а впереди ставилось отрицание. Благодаря этому переводу Колмогоров смог осуществить точное вложение КЛВ в рассматриваемый вариант интуиционистской логики.
Затем Сергей Одинцов исследовал связь между конструктивной семантикой и теоретико-игровой семантикой для логики предикатов первого порядка. Лектор представил доказательство теоремы Гливенко о связи классов формул, доказуемых в классических и интуиционистских системах естественного вывода. Затем была рассмотрена арифметика Гейтинга HA как теория с аксиомами арифметики Пеано над интуиционистским исчислением предикатов. Эта арифметика корректна, но не полна относительно семантики реализуемости. Сергей Одинцов с опорой на принцип Маркова представил доказательство того факта, что предложение р выводимое в HA из реализуемых предложений само будет реализуемым (теорема Нельсона). В конце лекции слушатели узнали, что, по сути, эффективная игровая семантика является эквивалентной реализуемости по Нельсону, ограниченной на формулы без импликации.
В заключительной лекции Сергей Одинцов сосредоточился на построении конструктивной семантики для IF-FOL логики. Она должна соотноситься с игровой семантикой так же, как соотносятся реализуемость по Нельсону и игровая семантика для обычной первопорядковой логики. Но прежде чем перейти к такой семантике, лектор рассказал о реализуемости негативных формул по Клини. В ходе третьей части мини-курса была представлена избыточная логика Нельсона N3 и её аксиомы, табличное исчисление с отмеченными формулами для интуиционистской логики, предложенное Воробьевым. Слушатели также узнали о доказательстве теоремы о полноте, согласно которой конечное множество отмеченных формул Int-выполнимо, если и только если оно является Ti-совместным (т. е. никакая таблица для этого множества не замкнута).
Возвращаясь к IF-FOL, Сергей Одинцов представил публике особенную трамп-семантику, как эффективную версию теоретико-игровой семантики. В этой модификации семантики мы рассматриваем уже не просто одну оценку s, а семейство оценок T с общей областью определения. Иными словами, оценки s ∈ T не обязаны быть определены на всём множестве переменных. В конце своего курса лектор доказал, что трамп-реализация для IF-FOL является обобщением реализуемости по Нельсону, ограниченной на фрагмент FOL без импликации (как и в случае с GTS).
Курс Александра Подобряева «Квантификация переменной силы в языках мира»
Александр Подобряев выступил на школе с лингвистическим курсом «Квантификация переменной силы в языках мира». В своей первой лекции он подробно рассказал об основах формальной семантики и лямбда-исчисления, прежде всего об аспектах, раскрывающих суть языкового поведения квантификации. Так, модальные операторы были определены как типы обобщенных кванторов над мирами, которые различаются по силе (экзистенциальная или универсальная) и базе (как минимум, или деонтическая, или эпистемическая).
Однако в естественных языках оказывается, что истинность экзистенциального утверждения не исключает истинности универсального утверждения, то есть возможность семантически не исключает необходимость. Это возможно, если понимать фразы с «может» как порождающие скалярную импликатуру, когда стандартная интерпретация исключает альтернативное прочтение «должен» по максиме количества. Тогда предположим язык с оператором возможности, но без оператора необходимости. В контекстах восходящего следования (например, «Вася курит как паровоз, значит он курит») не возникнет скалярной импликатуры, а значит этот единственный оператор можно будет использовать как в обоих модальностях. Такой феномен называется квантификацией переменной силы и про его реальные примеры Александр Подобряев рассказал в своем курсе.
Так, участники школы узнали о языке индейцев не-персе (nez-perce), в котором оператор возможности усиливается до необходимости в отсутствие более сильных альтернатив. Суффикс o’qa в этом языке тяготеет к экзистенциальному прочтению (носители языка в ходе тестов настаивали на интерпретации через возможность). Поэтому, когда индейцы не-персе говорят ненавязчивым гостям «Все в порядке, вы не обязаны сейчас уходить!», то отрицается наличие разрешения на возможность уйти, а не необходимость ухода. В языке лиллуэт у коренного народа в северных регионах Канады наблюдается обратная ситуация, безальтернативный оператор k’a выражает необходимость и может ослабляться до возможности. Вольный приближенный перевод на русский можно выразить конструкцией «должно быть», колеблющемся между универсальным и экзистенциальным прочтением. Наконец третий пример квантификации переменной силы, о котором рассказал лектор, встречается в древнеанглийском. В поэме «Беовульф» есть глагол motan (предшественник must) с пресуппозицией неизбежной актуализации, если пропозиция возможна, то ей «суждено» произойти.
Во всех этих случаях (не-персе, лиллуэт, древнеанглийский) исследователями предполагался анализ, где в семантике оператора специфицирована какая-то одна сила квантификации, а усиление/ослабление объясняется без вмешательства непосредственно в семантику. Александр Подобряев представил как раз такой подход, в котором модальный оператор выражается парой силы (force) и оттенка (flavour): (Fo, Fl). Если мы предположим, что оператор всегда должен быть окончательно специфицирован по силе, то в нем всегда будет зашита конкретная сила квантификации и определено к каким модальным базам (эпистемической или деонтической) он принадлежит. Таким образом мы получим семантическую универсалию. В конце своего курса Александр обратил внимание слушателей на тот факт, что не было обнаружено языков, в которых есть экзистенциальный, но нет универсального квантора. А в ходе обсуждения с аудиторией был поднят вопрос о переменной силе между императивом и разрешением.
Курс Натальи Ивлиевой «Дизъюнкция в грамматической теории импликатур»
Курс «Дизъюнкция в грамматической теории импликатур» Натальи Ивлиевой был посвящен особому поведению конструкций как или и либо в русском и английском языке. В естественных языках дизъюнктивные конструкции обычно воспринимаются в нестрогом смысле, а прочтение с истинностью/возможностью только одного из дизъюнктов традиционно считается скалярной импликатурой, возникающей прагматически в зависимости от контекста. Чтобы ее породить, слушателю надо подвергнуть отрицанию логически более сильное альтернативное высказывание, в котором дизъюнкция заменяется на конъюнкцию. Но у лингвистов эта картина вызывает много вопросов: как порождается эта импликатура? Что значит быть более сильной альтернативой? На каком уровне порождаются импликатуры?
В грайсианских теориях такие импликатуры возникают на уровне речевого акта по максимам, и тогда вложенные импликатуры становятся невозможны. Но этот подход проблематично анализирует симметричные альтернативы. У или есть альтернатива строгой дизъюнкции, но её отрицать нельзя, поскольку высказывание станет внутренне противоречивым. Это общая проблема для грайсианского анализа скалярных элементов. Поэтому Наталья Ивлиева подчеркнула важность теории возможных и невозможных альтернатив. Тут на помощь нам могут прийти шкалы Лоуренса Хорна и алгоритм Зауэрланда, предполагающий возможность эпистемического шага. Это значит, что говорящий имеет определенное мнение относительно истинности альтернатив, и с помощью этого допущения выводятся более сильные вторичные импликатуры, если только они не противоречат первичным. Эти альтернативные подходы позволяют объяснить ограничение Херфорда – запрет на следование одного дизъюнкта из другого (она живет в Париже или во Франции).
Подобные случаи демонстрируют, что импликатуры могут возникать локально, посередине высказывания. Существует лексическая теория, которая призвана объяснять подобные феномены. Однако она часто неверно предсказывает слишком локальные импликатуры, как в случае фразы «Каждый мой студент читал Толстого или Достоевского». Естественно сделать вывод о том, что все студенты прочитали хотя бы одного или обоих авторов, но в лексической теории конъюнктивное прочтение отбрасывается. Поэтому хотя глобальные импликатуры в естественном языке возможны (и даже предпочтительней), нам все же необходим механизм для объяснения их локальных собратьев.
По мнению Натальи Ивлиевой, локальные импликатуры порождаются не в прагматике, а в грамматике при помощи непроизносимого оператора, который имеет семантику похожую на семантику частицы только. John only saw Mary or Sue; каждый студент читал только Толстого или Достоевского. Формально такая невидимая конструкция представляет из себя невидимый оператор истощения (exhaust) EXH(P). Он отрицает не просто все альтернативы, а только подмножество альтернатив, потенциально отрицаемых без противоречия. Этот оператор может находиться на разных уровнях и применяться в том числе локально, а в ассерцию (утверждение) как ответ на обсуждаемый вопрос по умолчанию вшито исчерпывание. На оператор истощения, как объяснила лектор, также накладывается ограничение на дистрибуцию: истощение не может ослаблять значение, и если значение с EXH слабее значения без EXH, то EXH-структура не лицензируется.
Курс Рикардо Кавассане и Италы Д’Оттавиано «Pragmatic Nonsense»
В своей лекции бразильский ученый Рикардо Кавассане вместе с Италой Д’Оттавиано рассказал о классическом, начиная с работ Витгенштейна, разделении абсурда/бессмыслицы (nonsense) на формальный и прагматический. Бессмысленным в формальном смысле надо понимать выражение без корректной интерпретации, то есть без истинностного статуса. Так, некоторое выражение А будет бессмысленным, если и только если – это неправильно построенная формула, например «Сократ равен», «3 5 +», «b<». Этот вид бессмыслицы более точно можно определить как отсутствие интерпретации I на структуре E в домене D на языке L для некоторой неправильной построенной формулы.
Второй вид бессмыслицы также определяется через неопределенный истинностный статус, но на этот раз уже в особом понимании прагматической истины. Естественным примером прагматической истины могут выступать медицинские тесты, которые показывают результат всегда с некоторой, пусть даже минимальной, но погрешностью. Суждение о наличии болезни с опорой на тест будет прагматически истинным. Формально такие суждения мы делаем в рамках простой прагматической структуры A в виде пары (E, P), где E – это частично упорядоченная структура, а P – это набор предложений формального языка L, называемый набором первичных предложений для А.
Таким образом, в контексте теории прагматической истины любая правильно построенная формула формального языка, интерпретируемая на основе простой прагматической структуры, будет считаться прагматически бессмысленной, если набор первичных предложений такой структуры не является правильно построенным. То есть в тех случаях, когда он не включает соответствующие данные наблюдений и теоретические результаты, или если он включает предложения, которые не согласуются с такими данными. Как показал Рикардо Кавассане слушателям лекции, теория прагматического абсурда расширяет теорию формальной бессмыслицы так же, как теория прагматической истины расширяет семантическую теорию истины Альфреда Тарского.
Курс Анастасии Оноприенко «Модальные напарники интуиционистской логики и её расширений»
С курсом «Модальные напарники интуиционистской логики и её расширений» выступила на летней школе Анастасия Оноприенко. Самое первое занятие лектор начала с краткого введения в интуиционистскую логику, напомнив слушателям задачную интерпретацию связок и формул этого языка, известную также как семантика BHK (Брауэр-Гейтинг-Колмогоров). В свое время Курт Гедель предложил понимать каждую подформулу как подзадачу основной формулы, добавляя к каждой из подформул модальный оператор необходимости «бокс». Тогда получается, что если подобрать подходящую целевую логику, то с помощью такого перевода интуиционистскую логику можно погрузить в модального напарника S4.
Затем лектор рассказала о расширении логики S4 до логики Гржегорчика (Grz) с помощью формулы: □((□(p → □p) → p) → p). Таким образом мы получаем логику с частичным порядком без бесконечно возрастающих цепочек миров, которая является максимальным напарником для Int. Анастасия объяснила, что помимо двух крайних логик S4 и Grz все промежуточные логики между ними также будут напарниками для Int. В заключительной части лекции для наглядности на доске была построена решетка минимальных и максимальных напарников из двух отображений [τL, σL]. Отображение тау означает, что для формулы А, расширяющей Int есть логика τL = S4 + модальный перевод А. S5 по этому отображению – минимальный напарник классической логики. Отображение сигма означает, что для формулы А, расширяющей Int есть логика τL = S4Grz + модальный перевод А.
Во второй лекции Анастасия Оноприенко рассказала об альтернативных Геделевскому переводах интуиционистских логик в модальные, а также о модальных напарниках Int, не расширяющих S4. Лектор попыталась вместе со слушателями найти нормальное расширение логики К и минимальную логику для корректного и точного перевода. Таковой оказалась логика K□(D4!), в которой формулы D и 4! под боксом лежат как аксиомы. Формула D показывает, что из более сильного оператора необходимости следует оператор возможности: □φ → ◊φ. А формула 4! является сокращением для двух других, отражающих возможность навешивания и снятия боксов □□φ → □φ и □φ → □□φ.
Чтобы выразить различия между классами логик лектор предложила обобщение в виде модели (W, R, N, D). От обычной модели Крипке её отличает только множество нормальных N и выделенных миров D. Когда множества N и D совпадают – это будут обычные модели. В логике S2 для шкал все выделенные миры являются нормальными. В S3 шкалы таковы, что D будет подмножеством N, а R будет предпорядком. Эта же логика будет модальным напарником Int, если рассматривать перевод Si (как Геделевский перевод T, только бокс вешается не на все связки). Затем Анастасия Оноприенко показала, что существует целый континуум максимальных нормальных модальных напарников для Int по обоим переводам. Этот континуум на лекции был сопоставлен всем подмножествам ряда натуральных чисел.
В последней лекции мини-курса Анастасия вместе со слушателями изучила модальные напарники, которые являются расширениями S4. Если мы привели конечный список формул, добавленных к Int, мы уже знаем, что нам нужна логика S4 и модальный перевод всех добавленных формул Т(А). Но как возможен переход в обратную сторону, как понять для какой логики является модальным напарником S4 + формулы B? Для этого лектор предложила воспользоваться методом канонических формул, представленным в обобщенных шкалах Крипке. Они состоят из трех элементов (W, R, S), то есть к обычной шкале добавляется S – булеаново множество W, замкнутое относительно всех связок и взятия внутренностей I. Ограничения распространяются на все возможные оценки для модальной логики. Тогда как для Int логики ограничение на S будет аналогичным, но с точки зрения истинности в интуиционистских моделях.
Эти обобщенные шкалы можно расширить до полных канонических моделей с помощью канонических формул Y. Таким образом, логика S4 расширяется произвольной формулой, по которой можно написать конечное число канонических формул. В свою очередь уже из них некоторые определены на шкалах с частичным порядком (как в S4), а некоторые на шкалах с кластерами (как в S5). С помощью этого раскрытия можно сразу написать чьим модальным напарником будет эта расширенная логика. Анастасия Оноприенко в ходе своего курса показала слушателям, что для каждого частичного порядка можно написать интуиционистский аналог, но для кластерных логик это невозможно.
Курс Игоря Зайцева и Юрия Казакова «Ключевые метатеоремы теории доказательств: нормализуемость выводов и устранимость сечения в интуиционистской логике»
Игорь Зайцев и Юрий Казаков стажеры-исследователи Международной лаборатории логики, лингвистики и формальной философии представили совместный курс лекций «Ключевые метатеоремы теории доказательств: нормализуемость выводов и устранимость сечения в интуиционистской логике». Их лекции были посвящены прежде всего доказательственным системам и разным правилам вывода в них. Игорь Зайцев в первой лекции выделил три главных исчисления среди теорий доказательств: аксиоматические исчисления, натуральные исчисления (естественный/натуральный вывод, разработанный Станиславом Яськовским), а также секвенциальные исчисления (предложенные Герхардом Генценом).
Именно на секвенциальном исчислении сделал особый акцент в своих лекциях Игорь Зайцев. Сперва лектор рассказал об истории этого вида исчисления и о базовых понятиях по теме курса. Так участники школы узнали, что нормализацией называют процесс преобразования вывода для устранения всех обходных путей, что приводит к доказательству, непосредственно отражающему зависимость заключения от допущений. В свою очередь обходной путь – это любой вывод с правилом введения, за которым следует правило исключения, применяемое к заключению правила введения. То есть некоторый лишний шаг на пути к желаемому выводу. Так что вывод считается нормальным, если все главные (major) посылки правил удаления являются допущениями.
Изначальной мотивацией Генцена при создании секвенциального исчисления было исследовать особые свойства натуральных исчислений. Его основная теорема гласит: каждое чисто логическое док-во можно привести к некоторой определённой нормальной форме. Для её строгой формулировки Генцен вводит логистическое исчисление, в котором есть аксиомы, но нет никаких допущений. Но для этого непригодно классическое натуральное исчисление, оно подходит лишь в интуиционистской форме. Игорь Зайцев в ходе второй лекции доказал метатеорему об устранимости сечения (правило вывода, позволяющее удалить промежуточное высказывание) для интуиционистской логики G3QInt без исходных структурных правил и с обратимыми логическими правилами, разработанной Клини.
В своей половине курса Юрий Казаков презентовал участникам летней школы доказательство теоремы о нормальной форме для натурального вывода. Лектор также начал с базовых правил введения и исключения для разных связок в данном исчислении. Отдельное внимание Юрий уделил правилам для кванторов всеобщности и существования. Данный вывод будет выглядеть как дерево, в котором под гипотезами понимаются открытые допущения. Для наглядности слушателям были представлены некоторые доказательства, после чего лектор перешел к теореме о нормальной форме для исчисления NJ. Для этого были рассмотрены разные варианты преобразований после введения параметров по случаям внутри индукции, в зависимости от сложности сечения. Юрий выделил три таких случая: когда сложность равна 0 (константа ложь), равна 1 (конъюнкции, импликации, дизъюнкции, непротиворечия) и когда присутствует хотя бы один фрагмент сечения, например с квантором существования.
В заключительной лекции курса Юрий Казаков задался вопросом: какие ещё следствия кроме максимальных формул может дать нам натуральный вывод? Ключевой идеей для лектора была возможность перехода от доказательства теоремы нормальности к тому, что вывод обладает свойством подформульности. Иными словами, любая строчка станет подформулой допущения, либо конечной формулой вывода. Для доказательства этой идеи Юрий Казаков предложил альтернативу ветвям дерева доказательств – «нити», т. е. последовательности формул, которые включают: допущения, посылки правила введения или главные посылки правила исключения. Но они не могут включать малые посылки правил исключения (отрицания и импликации) или конечные формулы вывода.
Как показал Юрий, у исчислений и доказанных для них в ходе курса метатеорем, существует глубокое философское значение. Можно предложить семантическое прочтение логических констант и правил введения как утверждений постулирующих устройство связок. А правила исключения будут соответственно следствиями из определений связок, и таким образом мы получим программу теоретико-доказательственной семантики. Так что проверка на устранение сечений и максимальных формул не просто показывает какие-то свойства исчислений, но доказывает фундаментальную гармонию между двумя типами правил констант.
Курс Фабио Бертато «Deontic and Axiological Concepts and Values in Formal Ethics»
Лекция Фабио Бертато, представителя университета Кампинас, называлась «Deontic and Axiological Concepts and Values in Formal Ethics». Она опиралась на ключевую в области формальной философии работу 1982 года Франца фон Кучеры «Основания этики». В ней автор впервые разработал всеобъемлющую формализацию для ключевых понятий в области этики: деонтических концепций (обязательство, запрет и разрешение), аксиологических понятий (хорошее, плохое, безразличное) и степеней их различия. Фабио Бертато обратил отдельное внимание слушателей на различие между модусом действия и собственно действием, которые различаются как типы и токен, то есть прообраз и некоторое конкретное воплощение морального поступка.
Затем лектор представил основные принципы для разных модальных этических операторов, основанные на логических законах, как например обязательность тавтологий или проносимость оператора обязательства через квантор всеобщности или импликацию. Также Фабио Бертато рассказал о формализации для обязательств при некотором условии, которая позволила в байесианском ключе переводить этические понятия в числовой эквивалент для оценки конкретных ситуаций. Наконец, в заключение лекции наработки формальной этики и аксиоматизации моральных свойств были приложены к классическим учениям о нравственности, прежде всего к кантовской деонтологии и одной из формулировок категорического императива.
