Спирина, М.С. Дискретная математика

Известно, что в исчислении высказываний теоремами являют­ ся общезначимые формулы, поэтому автоматизация доказатель­ ства осуществляется в виде проверки общезначимости формул с помощью таблиц истинности. Проверка истинности формул про­ изводится для любого конечного набора значений переменных. Таким образом можно алгоритмизировать процесс доказательства теорем, но не процесс вывода теорем из аксиом. 5.3. Логика предикатов Результат считается красивым, если из малого числа условий удается полу­ чить общие заключения, относящиеся к широкому кругу объектов. Б. Гнеденко С помощью формальных теорий можно описать обширный класс высказываний, называемых предикатами. Сначала дадим опреде­ ление исчисления предикатов как формальной теории, а затем подробно остановимся на интерпретации. Сразу отметим, что те­ ория будет дана в значительно упрощенном виде: многие момен­ ты мы опустим. Формальная теория S = (A, F, Р, R) называется исчислением предикатов первого порядка, если заданы алфавит, формулы, ак ­ сиомы и правила вывода. 1. Алфавит А : • х, у, z... — предметные переменные, принимающие конкрет­ ные значения из некоего множества D. Тогда хь, Уо> z0... — значе­ ния предметных переменных, т.е. предметные постоянные (кон­ станты); • р, q, г... — переменные высказывания, принимающие два значения: 1 (истина) и 0 (ложь). Тогда р0, q0, г0... — фиксирован­ ные значения; • Р, Q, F — переменные, символизирующие само высказыва­ ние; Р0, Qo — постоянные предикаты; • — символы логических операций; дополнительно ис­ пользуются символы д, v; • V, 3 — кванторы общности и существования; • служебные символы ) , ( — нужны для установления порядка выполнения связок и области действия кванторов; • можно использовать также знаки ! — единственность,: — «та­ кой, что...» и другие символы метаязыка. Например, Vx е {3, 4, ..., 25} 3! у € (0, +°°): х = у2. 2. Формулы: F: • переменные есть формулы; 224