- •Министерство образования и науки Российской Федерации
- •Глава I. Алгебра высказываний
- •§ 1. Понятие высказывания
- •§ 2. Язык исчисления высказываний
- •Примеры формул и не формул
- •§ 3. Истинностные значения формул
- •§ 4. Законы логики, противоречия, выполнимые и равносильные формулы
- •§ 5. Совершенные дизъюнктивная и конъюнктивная нормальные формы
- •§ 6. Булевы функции
- •§ 7. Логическое следование
- •§ 8. Некоторые применения алгебры высказываний
- •Глава II. Алгебра предикатов
- •§ 1. Предикаты и кванторы
- •Логические операции над предикатами
- •§ 2. Равносильные и тождественно истинные предикаты
- •§ 3. Язык исчисления предикатов
- •§ 4. Интерпретации формул исчисления предикатов
- •§ 5. Приведённая и предварённая нормальные формы
- •§ 6. О структуре современных математических теорий
- •§ 7. Виды математических утверждений
- •§ 8. Некоторые методы доказательства теорем
- •Глава III. Формальные аксиоматические теории
- •§ 1. Формальные и неформальные аксиоматические теории
- •Примеры формальных аксиоматических теорий
- •Примеры доказательств в формальном исчислении высказываний
- •(В): (введение квантора ), (в): (введение квантора ),
- •Примеры доказательств в формальном исчислении предикатов
- •Аксиомы равенства:
- •Аксиомы операций сложения и умножения:
- •Примеры теорем формальной арифметики
- •§ 2. Непротиворечивость аксиоматических теорий
- •§ 3. Полнота аксиоматических теорий
- •§ 4. Разрешимость аксиоматических теорий
- •§ 5. Независимость системы аксиом теории
- •§ 6. Формальное исчисление высказываний
- •Приложение: формальная теория множеств
- •§ 1. Азы наивной теории множеств
- •Основные операции над множествами
- •§ 2. Аксиоматика Цермело-Френкеля теории множеств
- •40. Аксиома существования булеана (множества всех подмножеств) :
- •50. Аксиома (неупорядоченной) пары :
- •§ 3. Формальная теория множеств: райские кущи или адские дебри ?
- •А) основная литература:
- •Б) дополнительная литература:
- •Список основных обозначений
- •Предметный указатель
- •Алексей Игоревич Валицкас
Аксиомы равенства:
Рефлексивность: ( x (x = x))
Симметричность: ( x ( y ((x = y) (y = x)))
Транзитивность: ( x ( y ( z (((x = y) (y = z)) (x = z))))
Схема подстановки: для любых арифметических выражений А, В, С с выделенным вхождением выражения В в А (символически А = А(В)) следующая формула является аксиомой ((В = С ) (А(В) = А(С))), где А(С) – результат замены выделенного вхождения подвыражения В в А на С .
Это – очень сильная форма подстановки, её можно значительно ослабить.
Условимся для арифметических выражений А(x1 , … , xn) и В(y1 , … , ym) использовать краткую запись А(x1 , … , xn) В(y1 , … , ym) вместо отрицания .
Аксиомы операций сложения и умножения:
Существование и единственность следующего: ( x ( ! y (y = x + 1)))
Единица – наименьший элемент: ( x ((x + 1) 1))
Равенство следующих: ( x ( y ((x + 1) = (y + 1)) (x = y)))
Ассоциативность прибавления 1: ( x ( y ((x + (y + 1)) = ((x + y) + 1))))
Единица – нейтральна по умножению: ( x ((x1) = x))
Связь сложения и умножения: ( x ( y ((x(y + 1) = ((xy) + x)))))
Схема формальной индукции
Для любой формулы арифметики А(x) со свободной переменной x следующая формула является аксиомой: ((А(1) ( y (А(y) А(y + 1)))) ( x А(x))).
Правила вывода формальной арифметики, понятия доказательства формулы и доказуемой формулы в формальной арифметике такие же, как в формальном исчислении предикатов.
Примеры теорем формальной арифметики
Введём обычные обозначения: 2 = (1 + 1), 3 = (2 + 1) = ((1 + 1) + 1), 4 = (3 + 1) = (((1 + 1) + 1) + 1) , и.т.д.
1. (4 = (2 + 2))
( x ( y ((x + (y + 1)) = ((x + y) + 1)))) (аксиома ассоциативности +)
( y (((1 + 1) + (y + 1)) = (((1 + 1) + y) + 1))) (аксиома (x = 1+1))
(((1 + 1) + (1 + 1)) = (((1 + 1) + 1) + 1)) (аксиома (y = 1))
(((1 + 1) + 1) + 1) = ((1 + 1) + (1 + 1))) (аксиома симметричности)
((1 + 1) = 2) (определение)
((1 + 1) = 2) (((1 + 1) + 1) + 1) = (2 + 2)) (подстановка)
(((1 + 1) + 1) + 1) = (2 + 2)) МР(5, 6)
((((1 + 1) + 1) + 1) = 4) (определение)
((((1 + 1) + 1) + 1) = 4) (4 = (2 + 2))) (подстановка)
(4 = (2 + 2)) МР(8, 9)
2. (22 = 4)
( x ( y ((x(y + 1)) = ((xy) + x)))) (аксиома связи + и )
( y ((2(y + 1)) = ((2y) + 2)))) (аксиома (x = 2))
((2(1 + 1)) = ((21) + 2))) (аксиома (y = 1))
( x ((x1) = x)) (аксиома о нейтральности 1)
21 = 2 (аксиома (5))
((21 = 2) ((21) + 2) = (2 + 2))) (подстановка)
(((21) + 2) = (2 + 2)) МР(5, 6)
((2 + 2) = 4) доказано
(((2 + 2) = 4) (((21) + 2) = 4)) (подстановка)
(((21) + 2) = 4) МР(8, 9)
(2 = (1+ 1)) (определение)
(2 = (1+ 1)) ((22) = ((21) + 2))) (подстановка в 3)
((22) = ((21) + 2)) MP(11, 12)
((22) = ((21) + 2)) (22 = 4) (подстановка 10 в 13)
(22 = 4) MP(13, 14)
Приведём ещё пример неформального доказательства в формальной арифметике, использующий правила вывода и аксиому индукции. Докажем, формулу x ((x = 1) ( y ((x = 2y) (x = 2y + 1)))), выражающую тот факт, что любое натуральное число либо чётно, либо нечётно.
Пусть А(x) = (x = 1) ( y (x = 2y) (x = 2y + 1)). Тогда ясно, что А(1) доказуемо, т.к. А(1) = ((1 = 1) ( y (1 = 2y) (1 = 2y + 1))) , и первый аргумент этой дизъюнкции является аксиомой (?!). Теперь, чтобы воспользоваться схемой индукции, нужно доказать ( z (А(z) А(z + 1))).
Если доказано А(z) = ( y ((z = 2y) (z = 2y + 1))), то А(z+1) означает, что ( t ((z + 1 = 2t) (z + 1 = 2t + 1))). В том случае, когда z = 2y, имеем z + 1 = 2y + 1, и в качестве искомого t можно взять t = y. В случае z = 2y + 1 получаем z + 1 = (2y + 1) + 1 = 2y + 2 = 2(y+1), и в качестве искомого t можно взять t = y + 1.
Таким образом, неформально доказана формула ( z (А(z) А(z + 1))) и по схеме индукции, можно заключить, что доказана и формула ( x А(x)).
Упражнения: 1. Что в этом доказательстве неформального ?
2. Формализуйте доказательство.
Как видно из приведённых примеров, доказательство даже простейших теорем в формальной аксиоматической теории довольно громоздко. Для того чтобы дать возможность при доказательствах теорем рассуждать менее формально и не повторять многократно одни и те же куски похожих доказательств удобно в любой специальной теории (как и в теориях формального исчисления высказываний и формального исчисления предикатов) ввести понятие выводимости формулы из конечной совокупности формул Г.
Пусть Г = {Ф1 , … , Фk } – конечное множество формул (возможно пустое). Говорят, что формула В выводима из множества формул Г, если существует конечная цепочка формул В1 , … , Вn , где Вn совпадает с В, а каждая формула Bi (1 i n) либо является аксиомой, либо принадлежит Г, либо получена из некоторых предыдущих формул Вj и Вk (1 j < i, 1 k < i) по правилам вывода теории. Факт выводимости формулы В из совокупности Г обозначается через Г В.
Ясно, что формула В доказуема тогда и только тогда, когда она выводима из пустого множества формул: В. С другой стороны, если все формулы, входящие в Г = {Ф1 , … , Фk }, доказуемы, а В выводима из Г, то В доказуема. Действительно, чтобы получить доказательство формулы В, достаточно к её выводу В1 , … , Вn из формул Г присоединить доказательства формул Ф1 , … , Фk :
<доказательство Ф1 >, … , <доказательство Фk >, В1 , … , Вn –
это доказательство формулы В. Таким образом, для доказательства формулы достаточно вывести её из уже доказанных ранее формул.
Понятие выводимости аналогично понятию логического следования. В дальнейшем эта аналогия будет прослежена более подробно. Так, в § 3 будет доказана эквивалентность этих понятий для формальной теории исчисления высказываний. То же справедливо и для формальной теории исчисления предикатов. Таким образом, можно пользоваться при доказательствах формул изученными ранее правилами вывода, применяя их к выводимости формул.
Для простоты изложения в дальнейшем все рассматриваемые формальные теории, кроме исчислений высказываний и предикатов, предполагаются специальными.