R-I-G constructs for the logics of time

Tolstukhin Aleksei Post-graduate student, the department of Logics, M. V. Lomonosov Moscow State University 119234, Russia, Moskva oblast', g. Moscow, ul. Leninskie Gory, 1, of. 834 alexei.tolstukhin@gmail.com Other publications by this author

Введение

Временная логика как ветвь модальной логики обязана своим происхождением новозеландскому логику и философу Артуру Н. Прайору ^{[10, 11]}. Но не смотря на то, что временная логика существует уже более полувека, она до сих пор является популярным предметом исследования среди многих ученых. А с развитием компьютерных технологий логика времени стала особенно актуальной.

Безусловно, кроме своего практического применения, временная логика представляет интерес и для философского рассмотрения. Многие исследователи ^[12] склоны считать, что время в фокус рассмотрения философов попало благодаря работе "Критика чистого разума" немецкого философа И. Канта: «На этой априорной необходимости основывается также возможность аподиктических основоположений об отношениях времени или аксиом о времени вообще. Время имеет только одно измерение: различные времена существуют не вместе, а последовательно...". Однако проблему овременненых высказываний поднимает ещё Аристотель в ^[1], который пытается разобраться, каким образом оценивать высказывания о событиях, которые ещё не произошли и неизвестно произойдут ли, на всем известном примере о морском сражении.

Системы временной логики обладают довольно богатыми выразительными возможностями. Однако этот очевидный плюс приводит к ряду проблем, связанных с рассуждениями в данных системах. В статье рассматривается одна из таких проблем - проблема «остановки» вывода для временной логики .

Проблема «остановки» является распространенной проблемой для многих модальных логик. Суть проблемы заключается в том, что при построении вывода в исчислениях для модальных логик мы сталкиваемся с бесконечностью вывода, вызванной цикличностью в отдельных ветвях вывода, а иногда и с бесконечностью самих ветвлений. Существуют различные подходы к решению этих проблем, одним из которых является процедура loop-check ^[4]. При этом нет единого универсального метода решения.

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

Для решения проблемы «остановки» для мы будем использовать аналитико-табличное исчисление -- -конструкций, которое является производным от -конструкций исчисления ^[2], которое также основано на идее мозаик.

Метод мозаик используется для доказательства полноты и разрешимости систем неклассической и фрагментов первопорядковой классической логики. Своими корнями метод уходит в область алгебраических логик. Среди первых работ, где используется данный метод, можно указать работы венгерского логика И.Немети ^[8]. Изначально мозаики применялись к модальным логикам, в том числе многомерным. М. Рейнолдс, работавший с последними ^[13], перенес метод на временные логики, адаптировав под разные системы.

С помощью мозаик доказывают полноту аксиоматизации логики линейного времени с прайоровскими модальностями и , её разрешимость, полноту аналитико-табличного формализма ^[7]. Кроме того данный метод позволяет исследовать вопросы, связанные с алгоритмической сложностью проблем разрешимости ^[15].

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

По мере построения аналитической таблицы мы строим модель Крипке для формулы, а значит можем судить о её общезначимости и выполнимости.

В первой части статьи даны основные определения, аксиомы и семантика рассматриваемой логики .

Вторая часть посвящена -- -конструкциям и аналитическим таблицам.

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

1. Основные определения

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

Формулами языка являются пропозициональные переменные и выражения вида , , , , , , , , где и - формулы языка . Далее заглавными буквами латинского алфавита (, , и т.д.) будем обозначать произвольные формулы, а заглавными буквами греческого алфавита (, и т.д.) - множества формул.

содержит следующий перечень аксиом:

Пропозициональная связка определяется стандартно через и .

Правила системы :

Семантическими структурами являются структуры Крипке (), где - непустое множество, а - бинарное отношение на множестве , которое обладает следующими свойствами:

1. (свойство антирефлексивности);

2. (свойство асимметричности);

3. (свойство транзитивности);

4. (свойство линейности).

Определение 1 Модельной структурой (моделью) называем кортеж , в котором:

1. ;

2. есть отношение на ;

3. есть функция оценки.

Истинность формулы в модели определяется следующим образом: , для каждой пропозициональной переменной и формул и :

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

Определение 2 Пара и функция : образуют мозаику c базой {}, если для любой формулы из и для каждого выполняются следующие условия:

Если база мозаики является одноэлементным множеством, то данная мозаика называется вырожденной.

Определение 3 Множество M называется насыщенным множеством мозаик, если для всякой мозаики верны следующие утверждения:

1. Если и , то существует такая мозаика , что , и ;

3. Если и , то существует такая мозаика , что , и .

Всякое множество состоящее только из вырожденной мозаики, является насыщенным.

Таким образом, основной леммой является следующее утверждение.

Лемма 1 Формула выполняется в тогда и только тогда, когда существует согласованное насыщенное множество мозаик для .

Для доказательства данной леммы достаточно доказать два утверждения:

Утверждение 1 Если формула выполняется в , то существует согласованное множество мозаик .

Утверждение 2 Если существует насыщенное множество мозаик для формулы , то выполним в некоторой модели .

Для доказательства обоих утверждений используются ассоциированные структуры с разметкой. При доказательстве первого утверждения также демонстрируется методология решения проблемы дефектов прошлого и будущего. Подробное доказательство изложено в ^[7].

2. Аналитические таблицы

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

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

Определение 4 Индексированная формула есть пара , или просто , где есть целое положительное число, а - формула языка .

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

Определение 5 -- -конструкция есть тройка множеств , где - множество пар индексов, - множество целых положительных чисел, а - множество индексированных формул языка .

-- -конструкцию для удобства будем записывать в виде .

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

Традиционно правила редукции будем записывать в виде дроби:

Все правила системы можно разделить на преобразующие индексированные форму множества и модифицирующие множество . Запись в посылке правила означает, что множество содержит индексированную формулу , а в знаменателе правила обозначает . В этом случае индексированная формула называется редуцируемой формулой, а индексированные формулы, добавляемые к множеству в заключении правила - . означает, что множество содержит пары индексов .

Определение 7 L-аналитико-табличное исчисление есть конечная совокупность правил редукции ,..., .

Пусть имеется конечная последовательность -- -конструкций , ,..., ().

Определение 8 Последовательность , ,..., , ,..., получена из последовательности , ,..., применением правила , если совпадает с посылкой правила , а ,..., - с его заключением.

Представим -аналитико-табличное исчисление.

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

Используем стандартное определение дерева с корнем.

Определение 9 Пусть - конечное дерево -- -конструкций и получено из применением правила .

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

Определение 10

1. Любая отдельно взятая -- -конструкция есть -дерево.

2. Если есть -дерево и есть -дерево.

3. Ни что иное не является -деревом.

Определение 11 -аналитическая таблица для формулы языка - конечное -дерево, корень которого есть -- -конс- трукция вида .

Определение 12 -- -конструкция замкнута в случае, если для некоторых и : . Ветвь -аналитической таблицы замкнута, если последняя -- -конструкция в этой ветви замкнута. -аналитическая таблица замкнута, если все её ветви замкнуты. Формула языка называется -совместной, если не существует замкнутой аналитической таблицы для . Формула языка есть теорема -аналитико-табличного исчисления, если не существует замкнутой -аналитической таблицы для .

Определение 13 Ветвь -аналитической таблицы закончена в том случае, если к последней её -- -конструкции не применимо ни одно правило -аналитико-табличного исчисления. -анали- тическая таблица закончена, если закончены все её незамкнутые ветви. -аналитическая закончена, если закончена всякая её ветвь.

3. Построение аналитико-табличного вывода на основе -- -конструкций

Наличие завершенной аналитической таблицы ещё не гарантирует того, что в множество содержит полное насыщенное множество мозаик. По сути множество - это накопитель информации о взаимосвязи моментов времени и не более того. Для того, чтобы утверждать выполнима ли формула, необходимо: во-первых, показать, что множество пар, содержащихся в множестве можно использовать как базу для мозаик, дополнив функций ; во-вторых, обосновать, что полученное множество мозаик является насыщенным.

Рассмотрим процедуру построения -- -конструкции для формулы .

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

Теперь можно приступить к подробному рассмотрению множества . Определим функцию следующим образом: каждому элементу пар из множества сопоставляется множество формул с этим индексом, то есть

где формула с индексом - индексированная формула.

В результате получается следующий набор множеств.

Рассмотрим первую пару из множества (1,2). Для удобства будем называть пары из множества протомозаиками. Является ли протомозаика () мозаикой?

Согласно определению мозаики для пары (1,2) должно выполняться следующее условие: . В связи с этим дополним множество формулой . Остальные условия из определения выполняются.

Аналогично достраиваем протомозаику (2,3) до мозаики добавлением формулы в множество .

Таким образом, множество протомозаик является множеством мозаик. Следующим шагом является проверка, является ли данное множество насыщенным множеством мозаик?

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

Первая мозаика из содержит в себе формулу , а значит, согласно определению, должна существовать такая мозаика , что и . Такой мозаикой является мозаика .

Однако сама мозаика содержит , а соответствующей мозаики, которая бы выполняла условие насыщенного множества мозаик у нас нет. Такая ситуация называется максимальным дефектом будущего. Максимальные дефекты для своего исправления требуют наличие свидетеля. Согласно процедуре исправления дефектов мы можем дополнить наше множество такой мозаикой , что .

Пусть такой мозаикой будет :

Таким образом, возникает противоречие. Мозаика не соответствует третьему условию из определения мозаики. Исправить это возможно дополнением множества формулами и , последняя из которых приводит к возникновению нового дефекта будущего. Так можно продолжать до бесконечности.

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

Определение 14 -- -конструкция называется вниз насыщенной относительно правил нашего исчисления, если выполняются следующие условия:

1. не замкнута,

2. ,

3. и ,

4. или ,

5. для всех таких, что ,

6. для всех таких, что ,

7. существует такой, что и для некоторого ,

8. существует такой, что и для некоторого ,

9. ,

10. или или для некоторого ,

11. или или для некоторого .

Для вниз насыщенным мозаик существует следущие леммы.

Лемма 2 Если есть незамкнутая насыщенная аналитическая таблица для формулы языка , то существует вниз насыщенная -- -конструкция

Лемма 3 Пусть есть вниз насыщенная -- -конструкция. Тогда существует насыщенное множество мозаик .

Таким образом, формула, которая была рассмотрена выше явлется выполнимой, так как её аналитическая таблица незамкнута. По Лемме 2 мы можем получить вниз насыщенную -- -конструкцию для нее. Следовательно, по лемме 3, формула является выполнимой. Доказательства лемм в силу громоздкости в данной статье опущены.

Заключение

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

Возникает резонный вопрос, а можно ли построить исчисление таким образом, чтобы полученное множество уже являлось необходимым насыщенным множеством мозаик. Возможный ответ заключается в построении -- -исчисления аналогичного тому, что представлено в работе Рейнолдса, Маркса и Микуласа ^[7].