- •Математическая логика
- •Раздел I. Алгебра высказываний
- •1. Высказывания и операции над ними. Формулы
- •2. Следование, эквивалентность и преобразование формул
- •3. Использование законов логики в доказательстве теорем и построении схем
- •Преобразуем эту формулу, используя соответствующие эквивалентности u
- •4. Булевы функции
- •5. Нормальные формы
- •5. Полные системы операций. Алгебра Жегалкина
- •6. Выводимость
- •Раздел II. Алгебра предикатов
- •1. Предикат. Операции над предикатами.
- •2. Модель. Формула алгебры предикатов сигнатуры .
- •3. Формулы алгебры предикатов
- •Основные общезначимости алгебры предикатов
- •Раздел 3. Логические исчисления
- •1. Определение формального исчисления
- •2. Исчисление высказываний ив.
- •3. Отношение эквивалентности в ив
- •4. Исчисление секвенций ис.
- •Исчисления предикатов ип (ипс).
- •Прикладные исчисления предикатов.
- •Автоматическое доказательство теорем
- •Теория алгоритмов
- •Машины Тьюринга
- •2. Рекурсивные функции
- •3. Временная сложность алгоритма. Классы p и np.
- •4. Полиномиальная сводимость. Np-полные языки и задачи.
Раздел 3. Логические исчисления
Широкое использование аксиоматического метода в построении математических теорий стало одной из важных причин появления и развития математической логики. При таком подходе выбирается система основных неопределяемых понятий и отношений между ними, далее, постулируется система свойств основных понятий и отношений, называемых аксиомами. Новые понятия теории вводятся через основные или ранее определенные, а утверждения выводятся из аксиом или из ранее доказанных утверждений.
Всякую математическую теорему можно записать в виде импликации, выделив условие и заключение. При доказательстве теоремы из ее условия по определенным правилам получают заключение, при этом говорят, что заключение является логическим следствием условия или что оно выводимо из условия.
1. Определение формального исчисления
Логическим исчислением принято называть синтаксическую (т.е. формализованную аксиоматическую) теорию математической логики. Описание всякого исчисления I включает:
описание алфавита A(I), т.е. множества используемых символов, последовательности которых называются словами исчисления, множество всех слов обозначим W(I);
описание языка E(I), т.е. правил построения допустимых последовательностей символов (слов) алфавита, называемых формулами и секвенциями, из W(I) (E(I)W(I));
задание системы аксиом Ax(I) – некоторого множества истинных формул, называемых аксиомами (Ax(I)E(I));
определение правил вывода R(I), позволяющих из одних истинных формул получать другие формулы рассматриваемой синтаксической теории.
Для записи правил вывода используют сокращенную схему, которая имеет вид
,
и читаются следующим образом. “Если формулы U1, U2, . . . ,Um истинны, то в соответствии с правилом вывода Ri формула U также истинна”.
Таким образом, I = < A(I), E(I), Ax(I), R(I) >.
Указанием аксиом и правил вывода мы полностью определили понятие истинной, или выводимой в формальном исчислении, формулы. Пользуясь правилами вывода, мы можем, исходя из аксиом, конструировать новые истинные формулы и получать, таким образом, каждую истинную формулу. Формула B называется доказуемой (теоремой формального исчисления), что обозначается | B, если существует конечная последовательность формул
B1, B2, . . . , Bt , (1)
в которой каждая из формул Bi является либо аксиомой, либо, получена по правилам вывода из некоторых предыдущих формул последовательности (1). Эта последовательность называется доказательством формулы (теоремы).
Формула B выводима из формул U1, U2, . . . ,Un, называемых исходными посылками, что записывается символически как
U1, U2, . . . ,Un | B,
если существует такая конечная последовательность формул (1), что Bt есть B и для каждой формулы Bi выполнено одно из условий:
Bi есть посылка или теорема формального исчисления;
Bi получена из некоторых предыдущих формул последовательности (1) по правилам вывода.
Последовательность (1) называется в этом случае выводом формулы B из системы посылок U1, U2, . . . ,Un.
Заметим, что если посылки являются аксиомами или теоремами формального исчисления, то класс выводимых из них формул совпадает с классом всех истинных формул, выводимых из любой системы посылок.
Существует два типа формальных исчислений, в основе которых лежат формулы алгебры логики, это исчисления генценовского и гильбертовского типа.