Примеры теорем формальной арифметики

Приведём ещё пример неформального доказательства в формальной ариф­метике, использующий правила вывода и аксиому индукции. Докажем, формулу" x ((x = 1) Ú ($ y ((x = 2×y) Ú (x = 2×y + 1)))), выражающую тот факт, что любое натуральное число либо чётно, либо нечётно.

Пусть А(x) = (x = 1) Ú ($ y (x = 2×y) Ú (x = 2×y + 1)). Тогда ясно, что А(1) доказуемо, т.к. А(1) = ((1 = 1) Ú ($ y (1 = 2×y) Ú (1 = 2×y + 1))) , и первый аргумент этой дизъюнкции является аксиомой (?!). Теперь, чтобы воспользоваться схемой индукции, нужно доказать (" z (А(z) ® А(z + 1))).

Если доказано А(z) = ($ y ((z = 2×y) Ú (z = 2×y + 1))), то А(z+1) означает, что ($ t ((z + 1 = 2×t) Ú (z + 1 = 2×t + 1))). В том случае, когда z = 2×y, имеем z + 1 = 2×y + 1, и в качестве искомого t можно взять t = y. В случае z = 2×y + 1 получаем z + 1 = (2×y + 1) + 1 = 2×y + 2 = 2×(y+1), и в качестве искомого t можно взять t = y + 1.

Таким образом, неформально доказана формула (" z (А(z) ® А(z + 1))) и по схеме индукции, можно заключить, что доказана и формула (" x А(x)).

Упражнения: 1. Что в этом доказательстве неформального ?

2. Формализуйте доказательство.

Как видно из приведённых примеров, доказательство даже простейших теорем в формальной аксиоматической теории довольно громоздко. Для того чтобы дать возможность при доказательствах теорем рассуждать менее формально и не повторять многократно одни и те же куски похожих доказательств удобно в любой специальной теории (как и в теориях формального исчисления высказываний и формального исчисления предикатов) ввести понятие выводимости формулы из конечной совокупности формул Г.

Пусть Г = {Ф₁ , … , Ф_k } – конечное множество формул (возможно пустое). Говорят, что формула В выводима из множества формул Г, если существует конечная цепочка формул В₁ , … , В_n , где В_n совпадает с В, а каждая формула B_i (1 £ i £ n) либо является аксиомой, либо принадлежит Г, либо получена из некоторых предыдущих формул В_j и В_k (1 £ j < i, 1 £ k < i) по правилам вывода теории. Факт выводимости формулы В из совокупности Г обозначается через Г В.

Ясно, что формула В доказуема тогда и только тогда, когда она выводима из пустого множества формул: В. С другой стороны, если все формулы, входящие в Г = {Ф₁ , … , Ф_k }, доказуемы, а В выводима из Г, то В доказуема. Действительно, чтобы получить доказательство формулы В, достаточно к её выводу В₁ , … , В_n из формул Г присоединить доказательства формул Ф₁ , … , Ф_k :

<доказательство Ф₁ >, … , <доказательство Ф_k >, В₁ , … , В_n –

это доказательство формулы В.Таким образом, для доказательства формулы достаточно вывести её из уже доказанных ранее формул.

Понятие выводимости аналогично понятию логического следования. В дальнейшем эта аналогия будет прослежена более подробно. Так, в § 3 будет доказана эквивалентность этих понятий для формальной теории исчисления высказываний. То же справедливо и для формальной теории исчисления предикатов. Таким образом, можно пользоваться при доказательствах формул изученными ранее правилами вывода, применяя их к выводимости формул.