Аннотация 2
Введение 4
1 Язык L1, семантика и теория доказательства 6
1.1 Язык L1 6
1.2 Семантика языка L1 7
1.3 Теория доказательства 9
2 Корректность и полнота K 12
2.1 Корректность K 12
2.2 Полнота K 17
3 Перевод с языка L1 на язык L2 26
3.1 Язык L, 26
3.2 Семантика языка L2 26
3.3 Сравнение выразительных возможностей языков L1 и L2 28
Заключение 36
Список использованной литературы 37
Средств языка первопорядковой модальной логики, не содержащего Л-оператора или поссибилистских кванторов, не достаточно для формализации прочтений de re таких предло жений как, например, «число планет необходимо больше семи». Формализация предложения «число планет необходимо больше семи» как □ (n > 7), где n - число планет, □ - оператор необходимости и > понимается как в арифметике, отражает только прочтение de dicto. Для формализации, отражающей прочтение de re, требуется язык, обладающий большей вырази тельной силой.
Решение данной проблемы можно найти в книге М. Фиттинга и Р.Л. Мендельсона «First- ordermodal logic» (Fitting M., 1998, С.187-202). Авторы используют язык первопорядковой мо дальной логики с Л-оператором . Однако в данном решении есть некоторые недостатки:
1. Теория доказательства М. Фиттинга и Р.Л. Мендельсона позволяет доказывать только замкнутые формулы.
2. Не представлено доказательство корректности и полноты построенной логики.
Исследовательская проблема заключается в том, что в литературе не найдена логика, позволяющая решить проблему формализации прочтений de re, доказывать открытые формулы и для которой при этом была бы доказана корректность и полнота.
Актуальность темы исследования. Первопорядковые модальные логики используют ся как инструмент формализации рассуждений в философии языка, лингвистике, основаниях математики и т.д. Актуальность темы исследования обусловлена тем, что многообразие иссле дуемых рассуждений требует логик с большой выразительной силой.
В соответствии с этим, перед дипломной работой стоит две цели:
1. доказать корректность и полноту первопорядковой модальной логики K, построенной на языке с Л-оператором;
2. показать, что есть язык обладающий большими выразительными способностями.
Объект исследования - логика, построенная на языке с Л-оператором.
Предмет исследования - выразительные возможности логики, построенной на языке с Л-оператором.
Реализация поставленной цели предполагает решение следующих исследовательских задач:
1. Описать язык L1, на котором строится первопорядковая модальная логика K;
2. Построить семантику для языка С1;
3. Представить правила табличного построения деревьев K и определить логику K;
4. Изложить доказательство корректности и доказательство полноты K относительно се мантики для языка L1;
5. Описать язык L2;
6. Построить семантику для языка L2;
7. Определить перевод с языка L1 на язык L2;
8. Сравнить выразительные способности языков L1 и L2.
Используемые методы. Поскольку основная часть работы посвящена доказательству теорем о корректности, полноте и соотношении двух языков, используются такие методы как метод доказательства индукцией по структуре формулы и доказательство от противного.
Описание используемых источников и структуры работы. Первопорядковая модаль
ная логика с Л-оператором изложенав книге «First-Order Modal Logic» М. Фиттинга и Р.Л. Мендельсон Также в этой книге представлен метод доказательства корректности и полноты первопорядко вой модальной логики (без Л-оператора). Другие варианты доказательства полноты первопо рядковых модальных логик (без Л-оператора) представлены в книгах за авторством Д.Э. Хьюза и М.Д. Крессвелла «A companion to modal logic»(1984) и «A new introduction to modal logic» (1996).
Необходимые теоретико-множественные понятия осваивались по источникам: «A set theory workbook» И.Т. Адамсона, Л. Сиглера «Exercises in set theory», Э. Шиммерлинга «A course on set theory».
Тезисы работы:
1. Первопорядковая модальная логика, построенная на языке с Л-оператором, корректна и полна относительно семантики для этого языка.
2. Язык первопорядковой модальной логики, содержащий два вида кванторов (поссибилистские и актуалистские) и равенство, обладает большей выразительной силой, чем язык с Л-оператором и равенством.
В первом разделе дипломной работы были изложены язык L1, семантика для языка L1, теория доказательства, позволяющая доказывать открытые формулы, и определена логика K.
Во втором разделе представлено доказательство корректности и полноты логики K от носительно семантики для языка L1.
В третьем разделе представлено решение проблемы формализации прочтений de re без использования A-оператора. Для этого был описан язык L2, отличие которого от языка L1 за ключается в наличии двух видов кванторов (актуалистских и поссибилистских) и отсутствии A-оператора. Далее был определен перевод с языка L1 на язык L2 и показано, что перевод со храняет истинностное значение формул. В завершение было показано преимущество языка С2 перед языком L1, а именно было показано, что обратного перевода не существует, из чего сле дует, что язык L2 обладает большей выразительной силой, чем язык L1.
Перспективы дальнейшего исследования заключаются в построении теории доказательства для логики, построенной на языке С2, и доказательстве ее корректности и полноты.
