язык исчисления высказываний

язык исчисления высказываний Элементы теории алгоритмов 1. Интуитивное понятие алгоритма, вычислимой функции. Ансамбли  конструктивных объектов. Область возможных исходных данных. Область  применимости алгоритма. Примеры алгоритмов. Вычислимая функция. 2. Модели вычислений. Машины Тьюринга. Машины с неограниченными  регистрами (МНР). Тезис Чёрча. 3. Разрешимость, перечислимость подмножества ансамбля конструктивных  объектов. Критерий разрешимости перечислимого множества (теорема Поста).  Свойства перечислимых, разрешимых множеств. Теорема о графике вычислимой функции. Теорема о проекции. 4. Универсальная вычислимая функция. Невозможность вычислимой функции,  универсальной для класса всех всюду определённых вычислимых функций.  Главная универсальная вычислимая функция. Теорема о трансляторе (s­m­n­ теорема). Примеры неразрешимых проблем. Неразрешимость проблемы остановки.  Примеры неразрешимых перечислимых множеств. Многозначная (m­сводимость). Свойства m­сводимости. Теорема Райса о  неразрешимости нетривиальных классов в.ф. Примеры применения теоремы  Райса. Диофантовы множества. Десятая проблема Гильберта и ее отрицательное  решение. Логика высказываний 1. Язык логики высказываний. Логические связки и таблицы истинности.  Приведение формул к дизъюнктивной и конъюнктивной нормальным формам.  Булевы функции. Полные системы булевых функций. Теорема Поста. Полиномы Жегалкина. 2. Гильбертовский вариант исчисления для логики высказываний. Алфавит,  формулы, схемы аксиом и правила вывода исчисления высказываний. Вывод,  выводимая формула. Семантическая корректность исчисления высказываний. Вывод из гипотез. Теорема о дедукции для исчисления высказываний. Теорема о  семантической полноте исчисления высказываний. 3. Генценовский вариант исчисления для логики высказываний. Понятие  секвенциального вывода. Эквивалентность гильбертовского и генценовского  вариантов исчисления высказываний. Теорема об устранении сечения. Алгоритм  поиска вывода в исчислении высказываний.Логика первого порядка 1. Язык первого порядка. Понятие переменной, предиката, квантора. Сигнатура  языка первого порядка, терм, формула. Применение языков первого порядка для описания фрагментов естественных языков. Примеры языков первого порядка: языки теории полей, групп, частичного  упорядочения, язык арифметики. 2. Семантика языков первого порядка. Интерпретация языка первого порядка.  Выполнимые формулы, общезначимые формулы. Равносильность формул языка  первого порядка. Основные равносильности. Предваренные формулы.  Приведение формулы к предваренной форме. 3. Исчисление предикатов. Схемы аксиом и правила вывода исчисления  предикатов. Вывод из гипотез в исчислении предикатов. Теорема о дедукции для исчисления предикатов. Теорема о корректности исчисления предикатов. Теорема Гёделя о полноте исчисления предикатов. Невозможность  аксиоматизации предиката равенства в языке первого порядка. Нормальные  модели. Исчисление предикатов с равенством, его корректность и полнота  относительно нормальных моделей. Неразрешимость исчисления предикатов. 4. Теории первого порядка. Примеры теорий первого порядка: теория равенства, теория плотного линейного порядка, теория групп, теория полей, арифметика  Пеано. Теорема Гёделя о полноте для теорий первого порядка. Теорема Лёвенгейма­ Скулема. Теорема компактности для языков первого порядка. Невозможность аксиоматизации свойства конечности в языке первого порядка.  Существование счётных нестандартных моделей арифметики. Логика второго порядка 1. Логика 2­го порядка, основные отличия ее от логики 1­го порядка.  Определение предиката равенства. Формула, выражающая конечность.  Аксиоматизация арифметики. Неперечислимость логики второго порядка. Неклассические логики 1. Интуиционистская логика высказываний. Конструктивное понимание  логических связок, семантика Крипке. Аксиомы интуиционистского исчисления высказываний. Теорема о корректности и полноте интуиционистского исчисления высказываний относительно  семантики Крипке. Доказательство невыводимости законов исключенного третьего и снятия  двойного отрицания в интуиционистском исчислении высказываний. Свойстводизъюнктивности для интуиционистской логики. Невозможность задания  интуиционистских связок истинностными таблицами с конечным числом  значений. 2. Многозначная логика. 3. Модальная логика. Язык модальной логики. Примеры модальностей в  естественном языке. Системы аксиом для логик K, K4, S4, S5, GL, Grz.  Семантика Крипке для модального языка. Классы шкал Крипке,  соответствующие основным аксиомам логик K, K4, S4, S5, Grz. Полнота K, K4,  S4, S5, Grz относительно семантики Крипке. Вложение интуиционистской  логики высказываний в S4. 4. Временные операторы, языки временных логик. Логика данной шкалы  времени. Примеры временных логик: логики линейного времени, логики  ветвящегося времени. Перевод формул языка пропозициональной временной  логики на языки классической логики I­го и II­го порядка. Пример  неэлементарной временной логики. Разрешимость линейных временных логик.  Временные логики и верификация программ. Язык формализованного исчисления предикатов. ,  , функциональных букв   и  , кванторов   и   и скобок  , предикатных  , а также знаков логических  . При этом верхние индексы предикатных и  Алфавит исчисления предикатов состоит из предметных переменных  предметных констант (символы выделенных элементов)  букв  связок  функциональных букв указывают число аргументов соответственно предиката или функции, которые могут быть подставлены вместо этих букв. Понятие формулы определяется в два этапа. Сначала определяются термы. Ими являются  отдельно взятые предметные переменные и константы, а также выражения  вида  Наконец, определяются формулы: а) если   — предикатная буква,  все вхождения переменных в эту формулу называются свободными; б) если  переменных, свободные в  , являются свободными и в формулах указанных видов;   — n­местный функциональный символ;   — формулы, то формулами являются   — термы, то   — формула; при этом  , где   — термы.  ; причем все вхождениянет предметных переменных, которые связаны в   — формула, содержащая свободные вхождения переменной  кроме того, можно считать, что в   и  одной формуле и свободны в другой; в) если  и  вхождения же всех остальных предметных переменных в эти формулы остаются  свободными (связанными), если они были свободными (связанными) в формуле  (формула   называется областью действия квантора);  — формулы; при этом вхождения переменной   в них называются связанными;  , то      г) никаких других формул, кроме тех, которые строятся по правилам а, б, в, нет. Из этого определения ясно, что вхождения переменных в формулу обладают следующими  свойствами: свободные и связанные переменные обозначены разными буквами (если это не  так, то ясно, что, не нарушая смысла формулы, можно переобозначить в ней связанные  переменные); если какой­либо квантор находится в области действия другого квантора, то  переменные, связанные этими кванторами, обозначены разными буквами (если это не так, то  ясно, что, не нарушая смысла формулы, можно переобозначить в ней соответствующие  переменные). Нарушения этих свойств называются коллизией переменных. Определенные  формулы называются формулами первой ступени, так как в них разрешается навешивать  кванторы только по предметным переменным, а по функциональным и предикатным — не  разрешается. Возникающее исчисление предикатов называют исчислением предикатов  первой ступени или узким исчислением предикатов (в отличие от расширенного  исчисления предикатов), сокращенно — УИП.  называется сигнатурой  Совокупность  рассматриваемого исчисления предикатов. Если в сигнатуре отсутствуют функциональные  символы, (а значит, функциональные термы), то возникающее исчисление предикатов  называется чистым исчислением предикатов. Оно строится для произвольной предметной  области и не зависит от взаимосвязи между предметами в этой области. Это чисто  логическая теория. Именно о таком чистом исчислении предикатов и пойдет речь. Если же  такие связи имеются и они описываются функциями на этой предметной области, то логика  проникает в эту область и в эти связи и возникает логическая теория соответствующей  математической Дисциплины, или, как говорят, некая формальная математическая теория. Система аксиом исчисления предикатов Указанная система состоит из двух групп из которых первая — это аксиомы  формализованного исчисления высказываний:где под   понимаются уже любые формулы исчисления предикатов. Вторая группа аксиом (схем аксиом) — это собственно предикатные аксиомы (схемы  аксиом), т.е. аксиомы с кванторами. Выберем в качестве них следующие (называемые  аксиомами Бернайса):  — любая формула, содержащая свободные вхождения  где  находится в области действия квантора по   (если таковой имеется); формула  получена из   заменой всех свободных вхождений   на  . , причем ни одно из них не     формулу  Существенность последнего требования можно пояснить следующим примером. Рассмотрим в качестве формулы  вхождение  аксиому  общезначимой. В самом деле, предикат  превращает ее в ложное высказывание: , где это требование нарушено: свободное   находится в области действия квантора   на множестве вещественных чисел  . Подставив эту формулу в  , получим формулу   которая не будет  Правила вывода в формальном исчислении высказываний К правилу вывода modus ponens из исчисления высказываний добавляются еще два правила  вывода: ∀­правило, или правило обобщения:  ; ∃­правило, или правило конкретизации:  при условии, что   содержит свободное вхождение  , a   не содержит.и  Последнее требование также весьма существенно. Его нарушение может привести по этим  правилам к ложным выводам из истинных посылок. Так, например, взяв  предикаты  предикат  опровержимый предикат:  тех  условия) ∃­правило, то получим также опровержимый предикат  Применив же к последнему предикату уже на корректных основаниях ∀­правило, придем к  ложному высказыванию   над  . Но применив к нему правило обобщения, получим уже  (он превращается в ложное высказывание при  , которые делятся на 6). Если к предикату  , получим тождественно истинный   применить (в нарушение  .  . Теория формального вывода Определения формального доказательства (формального вывода из аксиом и из гипотез)  доказуемой формулы (теоремы) в формализованном исчислении предикатов даются так же,  как и в формализованном исчислении высказываний (см. определение 15.1), с точностью до  добавления двух новых аксиомных схем  правила и ∃­правила.  и двух новых правил вывода: ∀­  и   с фиксированными   называется выводимой из гипотез  Уточним все же понятие формальной выводимости формулы из гипотез в исчислении  предикатов. Формула  вхождениями (в гипотезы) свободных переменных, если существует такая конечная  последовательность формул  , каждая формула которой является  либо аксиомой, либо гипотезой, либо получена из предыдущих формул последовательности  по одному из правил вывода. (Сама эта последовательность называется выводом   из  гипотез  дальше в этом выводе не могут быть использованы ∀­ и ∃­правила вывода по любой  переменной  используется то же, что и в исчислении высказываний:  отсутствуют, то говорят, что  теоремой формализованного исчисления предикатов и пишут  , которая входит свободно хотя бы в одну из гипотез. Обозначение   выводима из аксиом (или просто выводима), и называют   есть первая гипотеза, встречающаяся в выводе, то  ). При этом, если  . Если гипотезы    . Отметим сначала, что так как все формулы, выводимые в исчислении высказываний,  являются также выводимыми в исчислении предикатов, то, совершая подстановки в  выводимые формулы исчисления высказываний, мы будем получать выводимые формулы  исчисления предикатов. (Тем не менее всякую выводимую формулу исчисления предикатов  таким способом получить нельзя.) Следовательно, все производные правила вывода,  установленные для исчисления высказываний, остаются справедливыми и для исчисления  предикатов, и мы будем в логике предикатов широко пользоваться этим.Дальнейшее изучение формализованного исчисления предикатов строится в форме  систематизированной подборки задач на доказательство теорем ФИП. Подборка начинается  с построения выводов из аксиом. Затем рассматривается построение выводов из гипотез.  Наконец — теорема о дедукции и ее применение к доказательству теорем ФИП. Теорема о  дедукции в ФИП формулируется так же, как и в ФИВ: если  , то  ), то  (в частности, если  . Ничем особо не отличается и идея доказательства, с  той лишь разницей, что появятся случаи, связанные с получением формулы в  последовательности­выводе не только по правилу modus ponens, но и по ∀­правилу и по ∃­ правилу.