- •Раздел 4. Математическая логика и формальные системы.
- •4.1. Введение в формальные системы
- •4.2. Принципы построения формальных теорий.
- •4.3. Исчисление высказываний. Аксиомы и правила вывода.
- •2) Правило заключения (Modus Ponens). Если u и u β – выводимые формулы, то β выводима:
- •4.4. Исчисления предикатов и теории первого порядка.
- •3. Аксиомы исчисления предикатов делятся на две группы:
- •1) Аксиомы исчисления высказываний ( можно взять любую из систем или );
- •2) Две следующие предикатные аксиомы:
- •4.Правила вывода:
- •3) Правило - введения:
- •4.5.Предмет математической логики
- •4.6. Аксиоматический метод
- •1.4 Такое число m единственно.
- •1.20 Если k ј m и m ј n, то k ј n.
- •4.7. Логика высказываний
- •2.1 Укажите два примера множества строк: одно замкнутое, другое не замкнутое относительно правил построения.
- •2.2 Множество формул замкнуто относительно правил построения.
- •2.3 Является ли формулой ¬(p & q)?
- •2.4 Является ли формулой (p)?
- •2.10 Найдите формулу f такую, что (3) – единственная интерпретация, при которой f истинна.
- •2.11 Для любых формул f1,...,Fn (n і 1) и любой интерпретации I
- •2.12 Сформулируйте и докажите подобный факт для дизъюнкции f1 ъ ··· ъ Fn.
- •2.13 Для любой интерпретации I существует формула f такая, что I – единственная интерпретация, при которой f истинна.
- •2.15 Покажите, что для атомов p и q
- •2.22 Предполагая, что p и q – атомы, определите
- •2.23 G влечёт f тогда и только тогда, когда g и { ¬f } не выполнимо.
- •2.24 Определить, какие из следующих формул являются тавтологиями: (p й q) ъ (q й p), ((p й q) й p) й p, ((p є q) є r) є (p є (q є r)).
- •2.25 Для любых формул f, g1,...,Gn (n і 1) : f следует из { g1,..., Gn } тогда и только тогда, когда (g1 & ··· & Gn) й f – тавтология.
- •2.26 Найдите вывод q & p из p & q.
- •2.29 Найдите вывод p й r из p й q и q й r.
- •2.43 Правило удаления отрицания корректно.
- •2.44 Правило введения отрицания корректно.
- •2.45 Правило противоречия корректно.
- •2.52 Оба правила введения дизъюнкции корректны.
- •2.53 Правило удаления дизъюнкции корректно.
- •3.1 Является ли " X формулой?
- •3.2 Если формула содержит квантор, тогда она содержит переменную. Верно или нет ?
- •3.3 Если формула содержит квантор, тогда она содержит скобки. Верно или нет ?
- •3.4 Найдите свободные переменные и связанные переменные формулы
- •3.5 Все простые числа больше чем X.
- •3.10 Найдите результат подстановки константы a вместо X в формулу из задачи 3.4.
- •3.11 Если V не является свободной переменной f(V), тогда f(t) равно f(V).
- •V не является свободной переменной формулы Kw f.
- •3.12 Терм, не содержащий ни одной связанной переменной формулы f, является подстановочным в f для любой переменной.
- •3.23 Каждый терм содержит объектную константу или объектную переменную. Верно или нет ?
- •3.38 Модель арифметики первого порядка (7) стандартна.
- •3.39 G непротиворечива.
- •3.40 Арифметика первого порядка имеет нестандартную модель.
Раздел 4. Математическая логика и формальные системы.
4.1. Введение в формальные системы
Формальные системы – это системы операций над объектами, понимаемыми как последовательность символов (т.е. как слова в зафиксированном алфавите); сами операции также являются операциями над символами. Термин "формальный" подчеркивает, что объекты и операции над ними рассматриваются чисто формально, без каких бы то ни было содержательных интерпретаций символов. Предполагается, что между символами не существует никаких связей и отношений кроме тех, которые явно описаны средствами самой формальной системы.
Если предложить читателю упорядочить объекты 53, 109, 3, то, скорее всего, он без всяких дополнительных вопросов расположит их в порядке 3, 53,109. Иначе говоря, этой задаче будет дана обычная арифметическая интерпретация: последовательности цифр рассматриваются как изображение чисел в обычной десятичной системе, упорядочение этих последовательностей есть расположение изображаемых ими чисел по возрастанию, а правило сравнения таких изображений чисел известно настолько хорошо, что обычно о них никто не задумывается.
В действительности такое упорядочение не очевидно. Возможность неоднозначного извлечения задач из текста ограничений означает, что текст не содержит формального определения задачи. Для такого определения необходимо четко описать класс объектов, для которых задача решается и явно ввести для них понятие упорядочения, описав его как систему локальных операций над символами, из которых эти объекты состоят.
По существу при таком понимании формальное описание системы означает ее точное, явное описание – все, что существенно для решения задачи, описано явно. Такое уточнение задачи принято называть ее формализацией.
Сходные соображения по поводу того, что такое точное описание можно проследить на примере понятий “алгоритм”, “данные” и т.п. В определенном смысле проблему точного описания некоторого множества можно рассматривать, как проблему построения алгоритма, перечисляющего или порождающего это множество.
Так, к примеру, определение с помощью формулы – это описание перечисляемого множества, в котором использованы все существенные составные части понятия алгоритм, кроме одного – детерминированности. Отбрасывая несущественный здесь порядок перечисления элементов множества, мы выигрываем в компактности описания, которое при этом не становится менее открытым. Такое описание, не являясь алгоритмом, представляет собой формальную систему, однозначно описывающую множество формул.
Исторически теория формальных систем возникла в рамках оснований математики при исследовании построения аксиоматических теорий и методов доказательств в таких теориях. С их изучения и начинается знакомство с формальными системами.