Содержание к диссертации
Введение
1 Основные определения и теоремы 13
1. Семантика Крипке 13
2. Допустимые правила вывода 21
2 Логика LTKr 23
3. LT Кг-фреймы 23
4. р-морфные образы ЬТКг-фреймов 25
5. Синтаксис LTKr 28
6. Свойства n-канонической модели LTKr
3 Разрешимость логики LTKr 38
4 Правила вывода LTKr
7. Строение п-характеристической модели LTKr 45
8. Разрешимость по допустимости правил вывода LTKr 47
Заключение 65
Список литературы
- Допустимые правила вывода
- р-морфные образы ЬТКг-фреймов
- Свойства n-канонической модели LTKr
- Разрешимость по допустимости правил вывода LTKr
Введение к работе
Актуальность темы
С начала 2000-х годов перспективным и быстро развивающимся стало направление модальных и много-модальных пропозициональных логик, описывающих рассуждения, доказательства и процессы вычислений. Такие логики позволяют перейти от языка, выражающего простые факты и утверждения, к более богатому и выразительному. Они имеют дело с высказываниями, содержащими в себе такие модальности, как возможно, необходимо, до тех пор, пока ... и т.д., которые нельзя выразить с помощью языка классических пропозициональных логик. Более широкая выразительность достигается посредством добавления к классической пропозициональной системе одного или нескольких модальных операторов (обычно или О).
Обычно модальные операторы читаются как «необходимо, что...», «возможно, что...», однако, существует великое множество различных интерпретаций. В случае временных логик, модальное выражение Пр может быть истолковано как «всегда в будущем верно р», а Ор - «существует момент в будущем, когда верно р». Такой язык эффективен при описании процессов во времени. Причем любую временную логику можно расширить до много-модальной посредством добавления операторов, представляющих будущее и прошлое. Такие логики нашли широкое применение при изучении искусственного интеллекта (AI) и в компьютерных науках (CS), для проверки корректности вычислительных программ.
Еще одним примером много-модальных логик являются логики Знания с модальностями, представляющими знания агентов. Они применимы для формализации утверждений об агентах, обладающих некоторой неполной информацией. Такие эпистемические модели имеют свой предел выразимости: с их помощью трудно описать процесс изменения информации, доступной агенту. Добавление временной модальности в таком случае расширяет описательные возможности языка. Наиболее естественным является внедрение логики Знания в рамки временной логики. Таким образом, получим много-модальную систему, сочетающую временные операторы и операторы знания. Хорошо известно, что такие системы образуют богатый, выразительный и интуитивно понятный язык.
Модели, порожденные сочетанием операторов, представляющих время и знание агентов, эффективно зарекомендовали себя в описании взаимодействия между различными агентами в потоке времени. Они получены добавлением к классической пропозициональной системе двух видов модальностей: для моделирования потока времени и для описания знания агентов. Полученный язык позволяет описывать ситуации, в которых агенты, обладающие определенными знаниями, оперируют ими в процессах рассуждений и вычислений, использующих пошаговые стратегии, имитирующие время. Изучение подобных систем активно развивается с середины 90-х годов. Например, Р. ван дер Мэйден и Н.В. Шилов исследовали линейную модальную логику Знания и Времени с модальными
операторами until и common knowledge в работе 1. В серии статей 2' 3' 4 Э. Калардо и В.В. Рыбаков рассмотрели линейную много-модальную логику Знания и Времени LTK с операторами знания агентов Кі, оператором common knowledge CL и оператором времени true from now on От. В статье В.В. Рыбакова и СВ. Бабёнышева 5 рассматривается много-модальная логика с оператором knowledge by interaction with agents 0<^. В книге 6 (Глава 4.3, Knowledge and Multi-Agent Systems: Incorporating time) предложено сочетание логики LTL (Linear Time Logic) и оператора knowledge base Ккв. Полная аксиоматизация целого ряда различных логик с условиями на знание и время (с операторами next, until, и операторами знания агентов) представлена в работе И. Халперна и др. 7.
С развитием компьютерных наук возрос интерес к изучению допустимых правил вывода для неклассических логик. Изучение искусственного интеллекта нуждается в языке, приспособленном для описания различных динамических систем, и язык многомодальных логик успешно справляется с этим. Изначально, факты и утверждения описываются с помощью формул, которые не способны выразить изменяющиеся условия и предпосылки. На помощь приходит применение правил вывода или секвентов, которые выражают логическое следование от условий (посылок) к заключениям, представляющим собой выводы или факты, которые можно получить из имеющихся предпосылок. Тем самым, правила вывода предоставляют нам более тонкий и выразительный аппарат для моделирования процессов мышления и вычислений.
Правило вывода - это схема, регламентирующая допустимые способы перехода от некоторой совокупности формул а\,... ,ап, называемых посылками, к некоторой определенной формуле /3, называемой заключением. Непосредственным изучением правил вывода впервые занялись Е. Лось (1955), А. Тарский (1956) и Р. Сушко (1958). Правило вывода называется истинным в логике Л, если из того, что а\,..., ап Є Л следует /З Є Л. Правило выводимо (доказуемо) в Л, если заключение /3 выводится из посылок а\,..., ап с помощью аксиом и постулированных правил логики Л. Понятие допустимого правила вывода было впервые введено П. Лоренценем в 1955 г. Для произвольной логики допустимыми являются те правила, которые не изменяют множество доказуемых теорем данной логики (т.е. правила, относительно которых логика замкнута). Формально, правило считается допустимым в Л, если при любой подстановке є, из а\,..., аєп Є Л следует, что /3є Є Л. Понятно,
^^Van der Meyden R., Shilov N.V. Model checking knowledge and time in systems with perfect recall // Lecture Notes in Computer Science, Springer, 1999, V. 1738, P. 432-445.
2Calardo E., Rybakov V.V. Combining time and knowledge, semantic approach // Bulletin of the Section of Logic, 2005, V. 34, № 1, P. 13-21.
3Calardo E., Admissible inference rules in the linear logic of knowledge and time LTK // Logic Journal of the IGPL, 2006, V. 14, № 1, P. 15-34.
4Calardo E., Rybakov V.V. An axiomatisation for the multi-modal logic of knowledge and linear time LTK// Logic Journal of the IGPL, 2007, V. 15, № 3, P. 239-254.
5Rybakov V.V., Babenyshev S.V. A Hybrid of Tencse Logic SAt and Multi-Agent Logic with Interacting Agents // Journal of Siberian Federal University. Mathematics & Physics, 2008, V. 1, № 4, P. 399-409.
6Fagin R., Halpern J.Y., Moses Y., Vardi M.Y. Reasoning About Knowledge // Massachussets, Cambridge, MIT Press. 1995, 491 p.
7Halpern J.Y., Shore R., Vardi M.Y. Complete Axiomatization for Reasoning About Knowledge and Time// SIAM Journal on Computing, 2004, V. 33, № 3, P. 674-703.
что любое доказуемое правило является допустимым в заданной логике. Таким образом, множество всех допустимых в логике Л правил образует наибольший класс правил вывода, которыми мы можем расширить аксиоматическую систему Л, не изменяя множества доказуемых теорем.
Начало истории изучения допустимых правил может быть датировано 1975 г. с появления проблемы X. Фридмана о существовании алгоритмического критерия допустимости правил в интуиционистской логике Int. В классической логике вопрос допустимости решался тривиально - допустимы только доказуемые правила. Однако, в логиках первого порядка, модальных и суперинтуиционистских логиках существуют допустимые, но не доказуемые правила вывода. В 1960 г. П. Харроп в работе 8 показал, что в логике Int допустимо, но не доказуемо -їх —> (у V z)/(->x —> у) V (->ж —> z). Г. Е. Минц в 9 доказал, что если правило г допустимо в Int и не содержит связок —> или V, то г выводимо в Int, и показал, что правило ((х —> у) —> (х V у))/(((х —> у) —> х) V ((х —> у) —> z)) допустимо, но не доказуемо в Int. В модальных логиках SA, 5*4.1, Grz допустимо, но не доказуемо правило Леммона-Скотта П(П(ПОПр —> Dp) —> (Dp V D^Dp)) /DODp V O-iOp. Таким образом, возникли вопросы алгоритмической разрешимости задачи распознавания допустимых правил вывода.
Положительное решение проблемы Фридмана о существовании алгоритма, распознающего допустимость правил вывода интуиционистской логики Int, было получено В.В. Рыбаковым в 1984 г. При развитии теории допустимых правил вывода для неклассических логик В.В. Рыбаков положительно решил проблему допустимости в широком классе модальных логик, в частности для К4, SA, Grz, GL и многих других.
В работе 10 В.В. Рыбаковым был использован специальный метод для разрешения проблемы допустимости правил вывода, который нашел свое применение во многих последующих исследованиях. Суть его заключается в том, что для всякого правила вывода существует конечное, с точностью до изоморфизма, множество конечных моделей Крипке специального вида, на элементах которого можно проверять истинность правила, для выяснения его допустимости. Несмотря на успехи в решении проблем допустимости правил вывода в различных логиках, данный метод имеет свои ограничения: он применим только для финитно-аппроксимируемых и транзитивных логик.
Одним из условий существования алгоритмов разрешимости допустимых правил вывода логики является ее разрешимость относительно доказуемости формул (обычно используют термин разрешимость). Напомним, что логика разрешима, если существует процедура, позволяющая по произвольной формуле определить, принадлежит ли она логике. Во многих случаях доказательство разрешимости логики сводится к доказательству того, что она обладает свойством конечных моделей (так называемым свойством финитной
8Harrop R. Concerning Formulas of the Types A —> В VC7, A —> 3xB(x) // Journal of Symbolic Logic, 1960, V. 25, № 1, P. 27-32.
9Минц Г.Е. Производность допустимых правил // Записки научного семинара ЛОМИ АН СССР, 1972, № 32, С. 85-99.
10Rybakov V.V. A criterion for admissibility of rules in the modal system 54 and the intuitionistic logic // Algebra and Logic (Eng. Ed.), 1984, V. 23, № 5, P. 369-384.
аппроксимируемости), т.е. что она полна относительно некоторого класса конечных фреймов Крипке (Теорема Харропа).
Несмотря на активные исследования допустимых правил вывода, большая часть результатов получена для транзитивных логик. При этом особый интерес представляют нетранзитивные логики, так как они более востребованы в computer science. Выяснилось, что для нетранзитивных логик не удается напрямую применять основные результаты и техники, используемые при исследовании допустимых правил вывода логик с транзитивными отношениями достижимости. Как было отмечено в работе 10, при исследовании допустимых правил вывода центральную роль играют так называемые гг-характеристические модели Крипке. Однако, построение таких моделей является достаточно ясным только для расширений модальной логики КА и интуиционистской логики. В нетранзитивном случае модели описаны только для очень малого списка логик. В работе п была представлена п-характеристическая модель для минимальной логики К. В 12 описана схема построения п-характеристической модели временной логики с нетранзитивным оператором времени завтра, и найден критерий допустимости правил вывода рассматриваемой логики. Также проблема допустимости правил вывода была решена для нетранзитивной временной логики конечных интервалов и логики LTLpastl которая сочетает в себе операторы знания агентов и нетранзитивный временной оператор since.
Результаты, представленные в диссертации, продолжают серию работ В.В. Рыбакова и Э. Калардо по исследованию свойств мульти-агентной логики Знания и Времени LTK. Ими была исследована логика LTK с транзитивным и рефлексивным отношением времени. Было доказано, что данная логика обладает свойством финитной аппроксимируемости и является разрешимой относительно доказуемости формул и допустимости правил вывода. Также представлена конечная аксиоматизация LTK. Однако, если предположить, что отношение времени не является транзитивным, то полученные результаты исследования нельзя перенести на данный случай, а используемые методы оказываются явным образом не применимы.
В диссертационной работе представлена мульти-агентная логика Знания и Времени LTKr с интранзитивным и рефлексивным отношением времени. Язык LTKr содержит временной оператор сегодня и завтра 0Tj оператор всеобщего знания (common knowledge) CL и несколько операторов знания агентов Dj. Интранзитивность времени в данном случае понимается следующим образом: на информационном узле актуальна только та информация, которая доступна либо в данный момент, либо будет доступна в следующий. Данная логика подходит для описании моделей, в которых время рассматривается как линейная дискретная последовательность состояний, содержащих в себе набор информационных узлов. Такие модели применимы в программном обеспечении, в области Интернет и в алгоритмах поиска.
11Chagrov А.V., Zakharyaschev M.V. Modal Logic // London, Cambridge Press, 1997, 589 p. 12Golovanov M.I., Rybakov V.V., Yurasova E.M. A necessary condition for rules to be admissible in temporal tomorrow-logic II Bulletin of the section of Logic, 2003, V. 32, № 4, P. 213-220.
Цель диссертации
Семантически определить линейную много-модальную логику Знания и Времени LTKr с интранзитивным и рефлексивным отношением времени и выяснить:
-
является ли логика LTKr финитно-аппроксимируемой и разрешимой;
-
разрешима ли проблема допустимости правил вывода LTKr. Предоставить алгоритм, который по заданному правилу г определяет, допустимо ли г в LTKr.
Методика исследования
Используются языки модальных и много-модальных логик, в том числе язык временных логик. В качестве основного инструмента исследования применяется семантика Крипке, расширенная на много-модальный и временной случаи. Также применяются общие методы теоретико-модельной семантики для пропозициональных нестандартных логик. Например, метод фильтрации, метод редуцирования правил вывода, семантический критерий допустимости правил вывода с помощью гг-характеристических моделей.
Научная новизна
Все результаты, представленные в диссертации, являются новыми и снабжены подробными доказательствами. Результаты совместных работ получены в нераздельном соавторстве.
Теоретическая и практическая ценность
Результаты, представленные в диссертации, носят теоретический характер и могут быть использованы в дальнейших исследованиях свойств много-модальных интранзитив-ных логик, а также в таких областях, как теория моделей, теория графов и computer science.
Практическое применение полученных результатов состоит в их внедрении в учебный процесс в виде материала для проведения специальных курсов кафедры алгебры и математической логики Института математики и фундаментальной информатики Сибирского федерального университета.
Степень достоверности и апробация работы
Достоверность научных результатов обеспечена опорой на современные методы исследования много-модальных неклассических логик: р-морфизмы и подмодели, метод канонических моделей, метод фильтрации для перехода от бесконечных моделей к конечным, критерий Рыбакова допустимости правил вывода.
Основные результаты диссертации обсуждались и докладывались на следующих конференциях: VIII всероссийской научно-технической конференции студентов, аспирантов и молодых ученых, посвященной 155-летию со дня рождения К.Э. Циолковского (Красноярск, 2012); VII всесибирском конгрессе женщин-математиков (Красноярск, 2012); меж-
дународной конференции серии "Мальцевские чтения"(Новосибирск, 2012, 2013, 2015); международной конференции, посвященной памяти В.П. Шункова "Алгебра и Логика: Теория и Приложения "(Красноярск, 2013); международной конференции "Алгебра и математическая логика: теория и приложения" (Казань, 2014).
Публикации
Основные результаты диссертации опубликованы в работах [1] - [9], из них 2 работы [1], [2] в ведущих рецензируемых изданиях, рекомендованных ВАК.
В нераздельном соавторстве выполнены четыре работы [2], [5], [6], [9].
Структура и объем работы
Допустимые правила вывода
Основным инструментом диссертационного исследования является семантика возможных миров. Первоначально идею возможных миров использовал Лейбниц для толкования "необходимо истинного "как того, что имеет место во всех возможных мирах, а "случайно истинного "как того, что имеет место в некоторых из них. Впоследствии Р. Карнап (1946), исходя из идей Лейбница, строит первую содержательную семантику для модального языка. Начиная с конца 1950-х годов, в модальной логике получила широкое распространение реляционная семантика Крипке, в которой вводится отношение достижимости (relation of accesibility) между мирами.
Основной структурой семантики является фрейм Крипке, который представляет собой пару (W, R): где W - множество (непустое) возможных миров, a R - бинарное отношение на W между мирами. Отношение R называют отношением достижимости: запись wRz означает, что мир z достижим из мира w способом, зафиксированным в свойствах отношения R. Модель определяется как упорядоченная тройка (W,R,V): где V есть функция означивания, приписывающая значения переменным множества миров V(р) С W: где они истинны. Модальный язык содержит:
В модальной логике также рассматривается унарный оператор 0 , определяемый как: ()А = -іП-іА Для любой формулы А модального языка выражение ПА интерпретируется как «необходимо А»: а выражение ()А - как «возможно А».
Отношение истинности \= на модели (W, R} V) для модальных формул определяется следующим образом:
В диссертационной работе используется семантика Крипке расширенная на много-модальный случай, где количество модальностей фиксировано, но потенциально не ограничено. Поэтому основные формальные определения и обозначения семантики Крипке будем давать именно для случая с множеством модальностей.
Пропозициональный /с-модальный язык С содержит все элементы одно-модального языка, однако, вместо одного модального оператора имеем к операторов Пі,..., П&. Понятие /с-модальной формулы языка С также определяется индуктивно стандартным образом, и множество всех таких формул обозначим как For {С).
/с-модальная логика А есть подмножество множества For, замкнутое относительно постулированных правил вывода {modus ponens, подстановки и т.д.).
По определению, нормальной к-модальной логикой называется расширение минимальной /с-модальной логики Kk, аксиомами которой являются:
Определение 1.2. п-модальный фрейм Т = (W , R\,... , Rn) называется открытым подфреймом т-модального фрейма S = (Ws} S\,..., Sm), если п = т, Wjr С Ws, для любого отношения Ri выполняется Si П W\ = Ri, а также \/а Є Wj, \/b Є Ws(aRtb = b Є W ). Определение 1.3. Фрейм Т = (W , R\,..., Rk) называется связным no отношению Ri, если Ух, y,z Є Wj {xR,by A xRiZ = yRiZ V zR,by). Определение 1.4. Дан к-модальный фрейм Крипке Т = (Wjr, R\,..., Rk); для любого Ri, Ri-сгусток - это подмножество С множества Wj такое, что \/w\/z Є C(wRiZ к zRtw) u\/z Є WjNw Є C(((wRtz к zRtw) = z Є С. Другими словами, Л -сгустком называется множество элементов, достижимых друг из друга по отношению Щ.
Говорим, что Л -сгусток С порожден элементом w (обозначаем C(w)), если w принадлежит С.
Рассмотрим некоторое множество пропозициональных переменных Р и некоторый /с-модальный фрейм Крипке Т = (Wj-, Ri, , Rk) Определение 1.5. Означиванием переменных из множества Р на фрейме Т называется функция V, которая каждой переменной р Є Р ставит в соответствие множество V(p) С Wj, т.е. V : Р і— 2Wj:.
Иначе говоря, функция означивания V определяет, на каких элементах основного множества Wj фрейма J- истинна та или иная пропозициональная переменная. Через Dom(V) := Р обозначаем множество переменных, для которых определено V.
р-морфные образы ЬТКг-фреймов
Так как уЩх, то из (1) и (2) следует (В А Л В В Л 0т(-" Л П„В)) Є г;, то есть на элементе v истинна посылка аксиомы AL. По построению п-канонической модели известно, что AL Є г , по правилу MP выполняется ПтВ Є v. Тогда из (3) следует, что - (vRrk). Таким образом, если C(v)RcTC(z) и C(z)RcTC(k), то (C(v)RcTC(k)). (f) Рассмотрим два Л -сгустка С\ и Сі п-канонической модели Л4 : при чем существуют х Є С\ и и Є С 2 такие, что xRcTu. 1) Предположим, что найдется элемент у Є Сі такой, что -i(xR y). Так как - (xR y): то по определению п-канонической модели, существует формула а такая, что П а Є х и a . у. Обозначим А = - а.
Из того, что теории и и у принадлежат одному Л -сгустку ( следует uRZy- Следовательно, () А є и. Так как хЩи, то ()т() А є ж, то есть посылка Tr.C.l принадлежит теории х. Однако, Пуск Є ж, тогда по определению истинности оператора Пу на n-канонической модели, выполняется ()тА ф Х- Следовательно, заключение Tr.C.l не принадлежит ж, что противоречит определению Л4сп. Таким образом, если существуют х Є С\ и и Є G i такие, что xRjU, то \/у Є Сі выполняется xRjy.
2) Пусть теперь найдется элемент у Є С\ и - (yRjii). По определению n-канонической модели, существует формула [5 такая, что Пт/3 Є у и [5 . и. Обозначим В = -і/З.
Из того, что xRj u, имеем ()тВ Є х. Так как теории х и у принадлежат одному Л -сгустку Сі, то xRcju и 0 0т-В Є у, то есть посылка Тг.С.2 принадлежит теории v. Однако, имеет место Пу/3 Є у, а также выполняется От-1-В Є у по определению истинности оператора Пу на n-канонической модели. Таким образом, заключение аксиомы Тг.С.2 не принадлежит теории у, что противоречит определению ЛЛсп. Следовательно, если существуют х Є Сі и и Є С 2 такие, что xRjU, то Vy Є Сі выполняется yRjU.
Из вышесказанного следует выполнение пункта (f) Леммы 2.4. (g) Для доказательства дискретности отношения RT требуется показать, что УС(а),С(Ь) Є W таких, что C(a)RjC(b) и С{а) Ф С(Ь), не существует элемента с Є Wcn, для которого выполняется C{a)RcTC{c) и С(с)ЩС(Ь), причем С(с) 7 С(а) т С(&)- Выполнение данного условия напрямую следует из пункта (е) Леммы 2.4. Таким образом, модель ]\Лсп является дискретной по отношению Rj. юбой логики является её разрешимость, т.е. возможность за конечное количество шагов проверить доказуемость в ней произвольной формулы в заданном языке. В качестве вспомогательного средства для доказательства разрешимости используется свойство финитной аппроксимируемости логики. В нашем случае удалось показать, что LTKr обладает более сильным свойством эффективной финитной аппроксимируемости.
Доказательство. Возьмем формулу А такую, что A . LTKr и пусть временная модальная степень td(A) равна п. Тогда существует LTKr—фрейм Т = (И ,Ят,Я ,Яі,...,і4), где W = {\JtejG} (J = [0,L],L Є TV или J = N), означивание V и элемент х Є Сг такие, что (J7, х) \/=у А.
Уменьшим количество элементов, принадлежащих каждому из RT сгустков С множества Wj с помощью стандартной техники фильтрации. Обозначим Sub(A) как множество всех подформул формулы А. Отношение эквивалентности на фрейме J- зададим следующим образом:
АЛ получена из модели Mi путем "отбрасывания"из IJ/j[ ] ФРагментов цепи ниже сгустка [Сг] и выше сгустка [Сг+П]. Таким образом, фрейм модели АЛ состоит не более чем из п + 1 Лу-сгустков, где п - временная модальная степень формулы А. Докажем, что если А опровергается на модели Мі, то она также опровергается на модели АЛ. Сначала покажем, что на АЛ сохраняется истинность формул, не содержащих модальных оператор Пу.
Лемма 3.2. Для любой формулы а такой, что td(a) = 0 и для любого элемента [у] Є {[Cr] U [Cr+i] U [Cr+2] U ... U [Cj]} справедливо: (Tu[y])\=Vla = (M,[y])\= x, (3-1) т.е. на модели АЛ истинность невременных формул сохраняется. Доказательство. Доказательство будем проводить индукцией по модальной невременной степени т(а) формулы а. Если т(а) = 0, то формула а состоит только из пропозициональных переменных и стандартных булевых операций. В этом случае истинность формулы на элементе [у] Є {[Cr] U [Cr+i] U [Cr+2] U ... U [Cj]} определяется только означиванием пропозициональных переменных, входящих в формулу а, только на элементе [у]. Таким образом, по построению модели АЛ, справедливо №, Ы) Ы " (М, [у]) = а.
Свойства n-канонической модели LTKr
Из вышесказанного следует, что на модели A4SP= выполняются условия 1), 2), 3) и 4) Леммы 4.3, при этом размер і?р-сгустков [С{]= ограничен размером правила гп/: мощность каждого сгустка не превышает s, где s количество ДИЗЪЮНКТОВ ПОСЫЛКИ Vnf.
Теперь ограничим длину цепи [[Со]=,... , [С ]=, Щ в соответствии размеру rnf. Для этого применим стандартную технику прореживания сгустков (drop-point). Для удобства переобозначим элемент @ через [Ср+і]=. Для каждого [СІ]= рассмотрим структуру (пару) M(i) := (pi U e (Mj) ГДе О і р + 1. Если Л4(і\) = М. 2)-, это значит, что Сіх и Сі2 изоморфны как модели, то есть существует взаимооднозначное отображение д такое, что V[a]s Є [СЧ] Щ= Є [C\U : (в(Ш = в([а]=)) к [Ь]= = 9ІШ Возьмем ЛуР-минимальный сгусток [Со]=. Он образует структуру (пару) .М(О) := ( [Со]=, U[al-fc0l_ ([a]=) ) Выберем наибольший номер индекса jo Є {1,...,р+1} такой, что JM(0) = Ai(jo), если таковой имеет ся. Удалим все і?р-сгустки из интервала [[Сі]=,..., [С,0]=], получим цепь [[Со]=, [C,-0+i] = ,..., [Ср]=, [Cp+i]=] с прежним означиванием V переменных Х{. Очевидно, что при таком прореживании истинность формул на элементах сгустка [Со]= не изменилась. Предположим, что на элементе [а]= Є [Со]= истинна формула ()T%J- Тогда либо
Если выполнялось 1., то процедура прореживания не изменила истинности формулы ()TXJ на элементе [а}= Є [Со]= и (.FSTL, [&]) =у ()T%J- Если же 1. и 3. не выполнялись, то ( 5Р=5 И=) Н OT J В силу 4.
Далее продолжаем описанную процедуру для всех последующих сгустков из рассматриваемой цепи, переобозначив при этом сгустки [С,0+ ]= через [С]=, где і Є {1,... ,р—j o + 2}. В конечном итоге получим цепь і?,р-сгустков, длина которой равна некоторому числу d + 2 и ограничена размером правила rnf. Для простоты, обозначим і?р-сгустки [С]= (0 і d), обратно, через СІ, а элемент [Cd+i]= через @.
Так как на каждом сгустке СІ Є [Со,... , С , Щ истинен единственный набор дизъюнктов lJrai_eC- #([a]=) посылки rn/, то сгусток СІ не изоморфен как модель сгустку Cj+i (0 і d—1). В том числе, сгусток Cd не изоморфен как модель элементу @, и на модели (J sp=,V) верно условие 5) Леммы 4.3.
Напомним, что Лр-сгустки C{w%-) = w%- являются одноэлементными. Обозначим через вг- формулу, которая истинна на элементе W1A. При этом имеем в\ = Q\ для всех г є {0,..., d} по 4.3.
Поэтому мы можем удалить все элементы из интервала [w w], и на полученной модели также будут выполнятся условия Леммы 4.3.
Повторим Этап 2 для остальных цепей ( [H=i w)i RT, R , - ъ 5 - ), где 1 і d. Длина каждой г-ой цепи станет равна J\ где 0 і d: при этом J ограничено размером правила гп/.
В конечном счете мы получим модель Aisp = (J SP-, У), на которой также выполняются условия 1)-5) Леммы 4.3, при этом мощность ее ограничена размером rnf.
Из Леммы 1.6 следует, что правило вывода не допустимо в логике, если оно опровергается на некоторой п-характеристической модели данной логики при некотором формульном означивании. В Лемме 4.2 установлено, что элементы n-характеристической модели логики LTKr не являются формульными. Поэтому для установления недопустимости правила вывода, следует ввести набор формул, определяющий формульное означивание переменных правила гп/ на элементах модели Скьткг(п), при котором данное правило опровергается.
Для начала рассмотрим правило вывода гп/ в редуцированной нормальной форме такое, что Var(rnf) = {х\,... ,хп}. Пусть гп/ опровергается на модели Aisp = {J sPiV), ограниченной размером гп/, где
Далее построим формулы, которые будут давать аналог формульности элементов модели Aisp- То есть каждому элементу Aisp сопоставим формулу, истинную на этом элементе. С помощью этого набора формул и будем определять формульное означивание переменных правила гп/ на элементах n-характеристической модели С1гьткг(п), при котором гп/ будет опровергаться на ChLTKr(n). (FSP,w)V=vPM(Oa) Доказательство. Пусть существует элемент w Є Wj sp глубины k 1 такой, что {FsPiW) \=v ЛІ=О — т — а- По определению истинности оператора Пу имеем Vz Є {и ДуР} : {Tsp z) \=v /\І=О ПуП_6 а. Так как отношение Щр является рефлексивным и интранзитивным, то либо z Є С (if), либо z Є C+i : C(w)Rj,pC+i. Аналогично, Ух Є { zi?yP } : (J SP X) \=v ДІ О ПуП_#а, при этом либо х Є С (if), либо ж Є С+і, либо ж Є С+2 : C+\R pC+2. Продолжая данные рассуждения и принимая во внимание, что k J, получим Vz Є if- : (FSPTZ) \=V CL#a. В том числе, Vz Є Cd выполнено (FsPiZ) \=v П- а и {FSP, Щ \=v П а- По определению истинности оператора CL имеем Vz Є ( справедливо (TSP Z) \=v 0а. Тогда в силу пункта 4) Леммы 4.3, сгусток Cd является вырожденным. Тогда Cd изоморфен как модель элементу @, что противоречит пункту 5) Леммы 4.3. Следовательно, Vif Є Wj sp : (if = @) верно {TSp,w) y=v fid+l{0a) П
(FSP,W) =i/ Pd-i+i Заметим, что в строении fii(Ok) в качестве подформулы присутствует формула вида /Зі+і(9т), поэтому для начала рассмотрим элементы сгустка Cd, на который истинна формула /3d(0k) Для любого элемента w Є Cd выполняется (wR p@), следовательно, {TSP,W) \=v От(П Ай-і(0а)) и {TSP,W) \=v РТ- При этом {TSp,w) \=V Ok для некоторого Ok Є Ai(d). Тогда (FsPiW) \=v Ok A pt A p\ A pT, т.е. {TSP,W) \=v fid{0k) Пусть теперь w Є Cd-i- Так как Cd-i является непосредственным -предшественником сгустка Cd, и Vz Є Cd верно [Tsp z] \=v fid{Om) для некоторого 0m Є A4(d), то по определению истинности оператора От имеем
Доказательство. По определению Aisp элементы w = Wj являются вырожденными і?,р-сгустками, и выполняется (J- SP W) \=v 0k для некоторого 0k Є Ai(i,j). Следовательно, по определению истинности оператора CL имеем {FSP, w) \=v 0k Л \3 0k.
По построению модели AiSp ровно через J — j + 1 по отношению R p из w = W%A достижимы элементы сгустка С{. При этом, по Утверждению 4.3 и определению истинности оператора CL, для любого Є СІ выполняется {FsPiX) \=v П_ УотЄлі(і) Рі{От)- По определению истинности оператора От получаем
Разрешимость по допустимости правил вывода LTKr
Возьмем произвольный элемент w глубины k модели СІіьткг{п): т-е-w Є /С = {K\(W)RTK2RT -RrKk} С CfiLTKr(n). Предположим, что w является формульным, то есть существует формула (3(w) временной модальной степени к такая, что (Ch(n),w) \=v /3(w) и Vz Є Wch{n) выполняется ((Ch(n),z) v P(w) w = z).
Рассмотрим элемент z глубины I к и открытую подмодель ЛГ = {NI(Z)RTN2RT RTNI} С СНЬТКГ(П), порожденную этим элементом, такие, что /С П ЛГ = 0, и К І изоморфен Ni для всех 1 і к. Так как истинность формул временной модальной степени к на элементе z зависит только от означивания переменных на модели {NI(Z)RTN2RT }, ТО индукцией по длине формулы легко показать, что на z также будет истинна формула /3(w), при этом z = w. Таким образом, элементы модели Скьткг(п) не являются формульными.
Лемма 4.3. [Необходимое условие допустимости правил вывода в логике LTKr[ Если правило вывода rnf в редуцированной нормальной форме не допустимо в логике LTKr, то существует конечная SP-модель Aisp = {Tsp}V), размер которой ограничен размером гnf, такая, что где Var(rnf) = {х\,... ,хт}. Пусть rn/ не допустимо в логике LTKr. Тогда существует подстановка CKJ, при которой каждая переменная Х{ Є Var(rnf) заменяется формулой а,и зависящей от некоторого набора пропозициональных переменных pi,...,pn. Причем посылка правила \J1 j sY1(9j) является теоремой LTKr, а заключение (жі) = OL\ не является теоремой LTKr. Положим max{td(\J\ j s S( -))} = f и i(ai) = p.
Теперь ограничим длину цепи [[Со]=,... , [С ]=, Щ в соответствии размеру rnf. Для этого применим стандартную технику прореживания сгустков (drop-point). Для удобства переобозначим элемент @ через [Ср+і]=. Для каждого [СІ]= рассмотрим структуру (пару) M(i) := (pi U e (Mj) ГДе О і р + 1. Если Л4(і\) = М. 2)-, это значит, что Сіх и Сі2 изоморфны как модели, то есть существует взаимооднозначное отображение д такое, что V[a]s Є [СЧ] Щ= Є [C\U : (в(Ш = в([а]=)) к [Ь]= = 9ІШ Возьмем ЛуР-минимальный сгусток [Со]=. Он образует структуру (пару) .М(О) := ( [Со]=, U[al-fc0l_ ([a]=) ) Выберем наибольший номер индекса jo Є {1,...,р+1} такой, что JM(0) = Ai(jo), если таковой имеет ся. Удалим все і?р-сгустки из интервала [[Сі]=,..., [С,0]=], получим цепь [[Со]=, [C,-0+i] = ,..., [Ср]=, [Cp+i]=] с прежним означиванием V переменных Х{. Очевидно, что при таком прореживании истинность формул на элементах сгустка [Со]= не изменилась. Предположим, что на элементе [а]= Є [Со]= истинна формула ()T%J- Тогда либо
Далее продолжаем описанную процедуру для всех последующих сгустков из рассматриваемой цепи, переобозначив при этом сгустки [С,0+ ]= через [С]=, где і Є {1,... ,р—j o + 2}. В конечном итоге получим цепь і?,р-сгустков, длина которой равна некоторому числу d + 2 и ограничена размером правила rnf. Для простоты, обозначим і?р-сгустки [С]= (0 і d), обратно, через СІ, а элемент [Cd+i]= через @.
Так как на каждом сгустке СІ Є [Со,... , С , Щ истинен единственный набор дизъюнктов lJrai_eC- #([a]=) посылки rn/, то сгусток СІ не изоморфен как модель сгустку Cj+i (0 і d—1). В том числе, сгусток Cd не изоморфен как модель элементу @, и на модели (J sp=,V) верно условие 5) Леммы 4.3.
Из Леммы 1.6 следует, что правило вывода не допустимо в логике, если оно опровергается на некоторой п-характеристической модели данной логики при некотором формульном означивании. В Лемме 4.2 установлено, что элементы n-характеристической модели логики LTKr не являются формульными. Поэтому для установления недопустимости правила вывода, следует ввести набор формул, определяющий формульное означивание переменных правила гп/ на элементах модели Скьткг(п), при котором данное правило опровергается.
Далее построим формулы, которые будут давать аналог формульности элементов модели Aisp- То есть каждому элементу Aisp сопоставим формулу, истинную на этом элементе. С помощью этого набора формул и будем определять формульное означивание переменных правила гп/ на элементах n-характеристической модели С1гьткг(п), при котором гп/ будет опровергаться на ChLTKr(n). (FSP,w)V=vPM(Oa) Доказательство. Пусть существует элемент w Є Wj sp глубины k 1 такой, что {FsPiW) \=v ЛІ=О — т — а- По определению истинности оператора Пу имеем Vz Є {и ДуР} : {Tsp z) \=v /\І=О ПуП_6 а. Так как отношение Щр является рефлексивным и интранзитивным, то либо z Є С (if), либо z Є C+i : C(w)Rj,pC+i. Аналогично, Ух Є { zi?yP } : (J SP X) \=v ДІ О ПуП_#а, при этом либо х Є С (if), либо ж Є С+і, либо ж Є С+2 : C+\R pC+2. Продолжая данные рассуждения и принимая во внимание, что k J, получим Vz Є if- : (FSPTZ) \=V CL#a. В том числе, Vz Є Cd выполнено (FsPiZ) \=v П- а и {FSP, Щ \=v П а- По определению истинности оператора CL имеем Vz Є ( справедливо (TSP Z) \=v 0а. Тогда в силу пункта 4) Леммы 4.3, сгусток Cd является вырожденным. Тогда Cd изоморфен как модель элементу @, что противоречит пункту 5) Леммы 4.3. Следовательно, Vif Є Wj sp : (if = @) верно {TSp,w) y=v fid+l{0a) П