КАРТОЧКА
ПРОЕКТА ФУНДАМЕНТАЛЬНЫХ И ПОИСКОВЫХ НАУЧНЫХ ИССЛЕДОВАНИЙ,
ПОДДЕРЖАННОГО РОССИЙСКИМ НАУЧНЫМ ФОНДОМ
Информация подготовлена на основании данных из Информационно-аналитической системы РНФ, содержательная часть представлена в авторской редакции. Все права принадлежат авторам, использование или перепечатка материалов допустима только с предварительного согласия авторов.
ОБЩИЕ СВЕДЕНИЯ
Номер 23-28-01465
НазваниеПроблема кросс-мировой предикации в модальной логике
РуководительБорисов Евгений Васильевич, Доктор философских наук
Организация финансирования, регион федеральное государственное бюджетное учреждение науки Институт философии и права Сибирского отделения Российской академии наук, Новосибирская обл
| Период выполнения при поддержке РНФ | 2023 г. - 2024 г. |
Конкурс№78 - Конкурс 2022 года «Проведение фундаментальных научных исследований и поисковых научных исследований малыми отдельными научными группами».
Область знания, основной код классификатора 08 - Гуманитарные и социальные науки, 08-202 - Логика. Философия языка
Ключевые словамодальная логика первого порядка, семантика возможных миров, кросс-мировая предикация, теория доказательства, логический анализ естественного языка
Код ГРНТИ02.21.00
ИНФОРМАЦИЯ ИЗ ЗАЯВКИ
Аннотация
Проблема, которой посвящен проект, возникает в контексте логического анализа некоторых высказываний и рассуждений на естественном языке средствами модальной логики первого порядка, основанной на семантике возможных миров. Проблема состоит в том, что некоторые предложения естественного языка не допускают адекватной формализации указанными средствами. Например, к таковым относится предложение «Джон мог быть выше, чем Мэри, как она есть»: оно говорит, что Джон, каков он в некотором возможном мире, выше, чем Мэри, какова она в действительном мире, т.е. приписывает Джону и Мэри кросс-мировое отношение. Проблема связан с тем, что стандартная семантика возможных миров, не «видит» кросс-мировых отношений: она позволяет отображать только внутримировые отношения. Это делает необходимой разработку принципиально новых модальных логик, преодолевающих данное ограничение, что и является целью проекта.
Следует отметить, что семантика возможных миров применяется не только в логическом анализе естественного языка: она имеет применения в метаматематике, теории языков программирования, теории игр, логистике и др., что обеспечивает широкий спект возможных применений логик, отражающих для кросс-мировую предикацию.
Актуальность темы проекта обусловлена широким распространением феномена кросс-мировой предикации в естественном языке (он встречается в алетических, темпоральных, деонтических, эпистемических и многих других контекстах) и отсутствием удовлетворительной логической системы, способной отображать этот феномен. При в кросс-мировой предикации могут быть задействованы предикаты любой местности (не только двухместные, как предикат "выше" в приведенном примере), что существенно осложняет разработку адекватных логик.
В литературе было предложено несколько логических систем, отображающих феномен кросс-мировой предикации, но они обладают очень ограниченной выразительной силой и используют усложненные формальные языки. Результатом проекта станет логическая система, отображающая данный феномен во всех его формах и основанная на стандартном формальном языке.
Разработка кросс-мировой логики включает в себя описание формального языка, определение семантики, разработку теории доказательства и доказательство метатеоремы об адекватности данной теории доказательства данной семантике. Формальный язык и семантика для кросс-мировой логики без ограничений на отношение достижимости (кросс-мировой логики К) уже разработаны руководителем проекта. В рамках проекта планируется решить дальнейшие задачи:
1) Разработать теорию доказательства гильбертовского типа для кросс-мировой логики K и доказать метатеорему о ее корректности и полноте относительно кросс-мировой семантики без ограничений на отношение достижимости.
2) Разработать теорию доказательства генценовского типа для кросс-мировой логики K и доказать метатеорему о ее корректности и полноте относительно кросс-мировой семантики без ограничений на отношение достижимости.
3) Разработать кросс-мировые логики S4, S5, D (с соответствующими ограничениями на отношение достижимости в семантике). Тем самым будут получены кросс-мировые логики, пригодные для отображения кросс-мировой предикации в темпоральных, алетических и деонтических контекстах.
4) Разработать перевод формул кросс-мировой логики на язык двухсортной немодальной первопорядковой логики. Перевод будет сохранять истинностное значение переводимой формулы относительно релевантных моделей при выполнении релевантных условий (это будет отдельная метатеорема). Перевод будет использован как эвристическое средство, показывающее соотношение кросс-мировой логики и стандартной первопорядковой немодальной логики.
Полученные кросс-мировые логики будут превосходить имеющиеся аналоги по выразительной силе; при этом используемый в них формальный язык будет проще формальных языков, используемых в имеющихся аналогах, что обеспечит более широкий спектр возможных применений.
Ожидаемые результаты
1) Определение функции перевода формул кросс-мировой логики на язык двухсортной немодальной первопорядковой логики, сохраняющей истинностное значение переводимых формул относительно релевантных моделей при выполнении релевантных условий.
2) Кросс-мировая логика K с теорией доказательства гильбертовского типа и доказательством метатеоремы о ее корректности и полноте относительно кросс-мировой семантики без ограничений на отношение достижимости. Демонстрация того факта, что данная логика превосходит имеющиеся аналоги по выразительной силе и простоте языка.
3) Кросс-мировая логика K с теорией доказательства генценовского типа и доказательством метатеоремы о ее корректности и полноте относительно кросс-мировой семантики без ограничений на отношение достижимости.
4) Кросс-мировые логики D, S4, S5 с теорией доказательства гильбертовского и генценовского типа. Для каждой логики будет доказано, что соответствующая теория доказательства корректна и полна относительно семантики с соответствующими ограничениями на отношение достижимости.
5) Демонстрация того факта, что данные логики превосходят имеющиеся аналоги по выразительной силе и простоте языка.
Результаты будут представлены в четырех статьях в журналах, индексируемых в Web of Science Core Collection или Scopus. Результаты будет иметь высокую научную значимость, поскольку откроют для модальной логики новое применение – формализацию и логический анализ рассуждений о кросс-мировых отношениях.
ОТЧЁТНЫЕ МАТЕРИАЛЫ
Аннотация результатов, полученных в 2023 году
Проект посвящен проблеме кросс-мировой предикации. Этот феномен имеет место в модальных контекстах в естественном языке, но он не может быть репрезентирован средствами стандартной модальной логики. Для репрезентации этого феномена необходима модальная логика первого порядка, базирующаяся на нестандартной семантике, которая позволяет ассоциировать объекты с мирами. Целью отчетного этапа была разработка такого рода логики. Разработанная логика (CWPL, crossworld predication logic) представляет собой модальную логику первого порядка с равенством. Семантика CPWL представляет собой семантику возможных миров с кросс-мировой интерпретацией предикатов и без ограничений на отношение достижимости. В результате выполнения проекта в 2023 г. была дана полная характеристика языка и семантики CWPL, был определен ее перевод на язык двухсортной немодальной логики первого порядка, было дано сравнение ее выразительных возможностей и выразительных возможностей гибридной логики Коцерека, и была разработана теория доказательства CWPL, корректная и полная относительно ее семантики.
Особенности синтаксиса CWPL состоят в следующем. 1) Формальный язык CWPL содержит лямбда-оператор. 2) Термы CWPL – это индивидные переменные и индивидные константы, однако в атомарных формулах CWPL в качестве термов используются только переменные.
Семантика CWPL кардинально отличается от семантики стандартных модальных логик в следующих аспектах.
1) В семантике CWPL предикаты имеют кросс-мировую интерпретацию. Это значит, что n-местному предикату экстенсионалы назначаются не для каждого мира (той или иной модели), но для каждой упорядоченной n-ки миров.
2) Формулы оцениваются на истинность/ложность относительно моделей, миров и оценок переменных (как в стандартной семантике), а также (в отличие от стандартной семантики) относительно частичных функций от переменных к возможным мирам – VP-функций. VP-функции формально репрезентируют ассоциацию объектов с мирами, подразумеваемую при использовании кросс-мировой предикации.
3) При оценке формул относительно заданных модели, мира и оценки переменных в качестве VP-функции, если не оговорено иное, используется пустая функция (пустое множество). С учетом этого, общезначимость в CWPL определяется так: формула общезначима, если она истинна относительно любой модели, любого возможного мира в данной модели, любой оценки переменных в данной модели и пустой VP-функции.
4) Выявлен ряд семантических свойств CWPL, отличающих ее от стандартных модальных логик первого порядка в аспекте общезначимости. Например, формула Ɐx◊P(x)→ⱯxP(x) оказывается общезначимой в CWPL, тогда как в любой стандартной логике она таковой не является. Этот результат важен для разработки теории доказательства CWPL и демонстрации ее полноты.
Кроме того, был разработан перевод формул CWPL на язык двухсортной первопорядковой (немодальной) логики (FOL2), т.е. дано рекурсивное определение функции перевода от формул CWPL к формулам FOL2. При этом определена функция от моделей CWPL к моделям FOL2 и доказано, что перевод сохраняет истинность, т.е. если формула CWPL истинна в некотором мире некоторой модели CWPL, то ее перевод истинен в соответствующей модели FOL2.
Было дано сравнение CWPL и гибридной логики Коцурека (H) по выразительной силе. С этой целью разработан перевод с языка CWPL на язык H и определена функция от моделей H к моделям CWPL. Показано, что перевод сохраняет истинность относительно соответствующих моделей. Показано, что H превосходит CWPL по выразительной силе, и что это обусловлено использованием гибридных операторов в формальном языке H. С другой стороны, CWPL превосходит H по простоте языка. Показано также, что язык CWPL лучше соответствует целям формализации тех фрагментов естественного языка, которые не содержат выражений, соответствующих гибридным операторам.
Была разработана табличная теория доказательства для логики CWPL0, которая является упрощенной версией CWPL. Было показано, что эта теория доказательства корректна и полная относительно описанной семантики. Было показано, что посредством ряда модификаций теория доказательства для CWPL0 может быть трансформирована в теорию доказательства для CWPL, причем демонстрация корректности и полноты CWPL0 может быть трансформирована в демонстрацию корректности и полноты CWPL.
По результатам проекта подготовлены к печати три статьи. Кроме того, результаты были представлены в трех докладах на международных научных конференциях.
Публикации
1. Борисов Е.В. A nonhybrid logic for crossworld predication / Негибридная логика для кросс-мировой предикации Логические исследования / Logical Investigations, Логические исследования / Logical Investigations. 2023. Т. 29. № 2. C. 125-147 (год публикации - 2023) https://doi.org/10.21146/2074-1472-2023-29-2-125-147
2. Борисов Е.В. Логика для кросс-мировой предикации: теория доказательства Вестник Томского государственного университета. Философия. Социология. Политология, - (год публикации - 2024)
3. Ламберов Л.Д. К вопросу об особенностях CPL Вестник Томского государственного университета. Философия. Социология. Политология, Вестник Томского государственного университета. Философия. Социология. Политология. 2023. № 74. С. 17–24 (год публикации - 2023) https://doi.org/10.17223/1998863Х/74/2