<< Пред. стр.

стр. 4
(общее количество: 9)

ОГЛАВЛЕНИЕ

След. стр. >>

В предыдущей главе мы отложили вопрос о том, как проверять, является ли
данная формула P ? L? логическим следствием заданного множества формул
? ? L? . Очевидно, что осуществить такую проверку в соответствии с определе-
нием не представляется возможным. Действительно, нельзя просто перебрать
всевозможные модели всех одновременно формул множества ?, чтобы прове-
рить, являются ли они моделями формулы P, т.к. число таких моделей может
быть бесконечно, за исключением разве что некоторых тривиальных случаев.
Математики заменяют такую проверку поиском доказательства формулы P из
набора формул ?, т.е. поиском способа ”свести” формулы ? и, возможно, ещё
некоторые дополнительные формулы, к формуле P, при помощи конечного чис-
ла логических заключений (иногда говорят логических переходов) являющихся
общепризнанно элементарными. В этой главе мы формализуем процесс доказыва-
ния таким образом, чтобы полученная формализация была применима к языкам
логики предикатов первого порядка.
Будем различать семантические и формальные истины, определяемые для
формул ?. Семантические истины это те формулы, которые семантически сле-
дуют из ?, формальные – те, которые выводятся из данного набора при помощи
принятых правил доказывания. Важно отметить, что истина, полученная при по-
мощи формального вывода (доказательства) существенно зависит от того, какие
правила доказывания мы считаем допустимыми. В любом случае хотелось бы,
чтобы формулы выводимые (доказуемые) были истинны семантически. Иначе
правила вывода получаются некорректны (они существуют для вывода семанти-
ческих истин, а не всякой ерунды). Но, конечно, желательно, чтобы наши пра-
вила были в определенном смысле полны, то есть формально выводились бы все
семантические истины.
Рассмотрим формальный язык L ? V ? над алфавитом V . Будем называть
секвенцией выражение вида
V1 , V2 , . . . , Vn V,
где Vi ? L, i = 1, . . . , n и V ? L, либо выражение вида
V,
где V ? L. В первом случае будем читать секвенцию V1 , V2 , . . . , Vn V как
“V1 , V2 , . . . , Vn выводит (или доказывает, если L – какой-либо логическийязык)
V ”, или “из V1 , V2 , . . . , Vn следует V ”. Во втором случае секвенцию V будем чи-
тать как “V выводима”, или выводима из пустого множества посылок (доказуема,
если L – какой-либо язык логики). Теперь введем следующее определение.
6.1 Формальные cистемы 31


Определение 6.1 Будем говорить, что задана формальная система ?, если
заданы

(i) набор секвенций вида V , где V ? L, называемых аксиомами формальной
системы;

(ii) набор секвенций вида V1 , V2 , . . . , Vn V где V ? L и Vi ? L, i = 1, . . . , n,
называемых простыми правилами вывода;

(iii) набор условных правил вывода вида “из ?0 V 0 и ?1 V 1 следует ? V ”,
где ?0 , ?1 , ? конечные подмножества L, и {V 0 , V 1 , V } ? L.

Определение 6.2 Слово (формула) V ? L называется непосредственным след-
ствием слов (формул) {V1 , V2 , . . . , Vn } ? L, если либо V1 , V2 , . . . , Vn V , где
V1 , V2 , . . . , Vn V – одно из простых правил вывода в формальной системе ?,
либо если найдутся такие конечные множества ?0 ? L, ?1 ? L и такие сло-
ва (формулы) V 0 ? L и V 1 ? L, что правило “из ?0 V 0 и ?1 V 1 следует
V1 , V2 , . . . Vn V ” является одним из условных правил вывода формальной си-
стемы ?.

Определение 6.3 Слово (формула) V ? L выводимо (доказуемо) из
{V1 , V2 , . . . , Vn } ? L, если найдется такая последовательность формул {Wi }k ,
i=1
где k ? N, где Wk = V и каждое из слов Wi ? L, где i = 1, . . . , k является

(i) либо аксиомой формальной системы ?;

(ii) либо одной из формул V1 , V2 , . . . , Vn ;

(iii) либо непосредственным следствием некоторого подмножества слов (фор-
мул) ? ? {W1 , W2 , . . . , Wi?1 }.

В этом случае будем писать

V1 , V2 , . . . , Vn V,
?


причем индекс ?, указывающий на используемую формальную систему, будем
опускать, если это не ведет к неясности.

Определение 6.4 Формальная система ? называется корректной, если для
любого множества ? ? L и для любого P ? L из ? ? P следует ? |= P,
то есть все формальные истины, получаемые при помощи данной формальной
системы, являются семантическими истинами.
32 Элементы теории доказательств


Определение 6.5 Формальная система ? называется полной, если для любого
множества ? ? L и для любого P ? L из ? |= P следует ? ? P, то есть все
семантические истины можно получить формально.
Таким образом определенное понятие формальной системы применимо вовсе
не только к языкам логики. Это просто инструмент для операций с цепочками
символов заданного формального языка.
Приведем простейший пример формальной системы.
Пример 6.1 Рассмотрим язык L, совпадающий со множеством всех слов над
алфавитом {a, b}, и формальную систему, содержащую
две аксиомы
• a,
• b,
и бесконечное количество правил вывода, объединенных в две группы
•A aAa,
•A bAb,
где A – любое непустое слово языка. Для этой формальной системы, например,
можно получить aaa, bab, babab. В частности, из пустого множества
выводимы любые палиндромы нечетной длины (цепочки символов, которые чи-
таются одинаково слева направо и справа налево). Этот же пример показы-
вает и различие семантической и формальной истин. К примеру, условимся
считать “осмысленными” (семантически истинными) все палиндромы, а фор-
мальными истинами – всё, что выводимо из пустого множества. Тогда не
все семантические истины оказываются формальными (то есть формальная
система неполна), но формальные истины всегда являются семантическими,
иначе говоря, формальная система корректна.
Другой пример формальной системы, не имеющей отношения к логике: фор-
мальная система для языка записи шахматных позиций. У неё одна аксиома – это
начальная позиция, а правила вывода – правила ходов. Стоит отметить, что в по-
нятие позиции входит не только положение фигур на доске, но также и признаки
того, делал ли игрок ход королем и кто из игроков сделал последний ход.
В следующем разделе мы будем изучать формальную систему, применимую к
языку логики предикатов первого порядка, правила вывода которой моделируют
те элементарные логические заключения, которые используют математики при
доказательстве формул.

6.2 Естественная дедукция
Логические заключения, которые используют люди в своих рассуждениях, опре-
деляется рядом элементарных правил, которые сформулированы ещё Аристоте-
лем. Формализация этих правил приводит к различным формальным системам
6.2 Естественная дедукция 33


для логических языков. Впредь мы будем рассматривать одну из таких фор-
мальных систем для языка логики предикатов первого порядка, называемую
естественной дедукцией (Natural deduction). Аксиом в ней нет, а правила вы-
вода можно разделить на две группы: правила введения (обозначаются буквой i
– "introduce", слева соответствующий значок отсутствует, справа присутствует),
и правила исключения (обозначаются буквой e – "eliminate", справа соответству-
ющий значок отсутствует, слева присутствует) для каждого логического значка
и квантора (?, ?, >, ¬, ?, ?). При формулировке этих правил мы покажем их за-
пись в строчной форме и в форме столбца (дерева), а именно, строчную запись
A
A B можно заменить записью в столбец (в виде дерева) .
B




правило A?B
(?e1 ) A?B A
исключения “и” A
правило A?B
(?e2 ) A?B B
исключения “и” B
правило AB
(?i) A, B A?B
введения “и” A?B
правило введения A
(?i1 ) A A?B
“или” слева A?B


правило введения A
(?i2 ) A B?A
“или” справа B?A
[A]1 [B]1
Если A C
правило
C C A?B
и B C,
(?e)
исключения “или” 1
то A ? B C C
Иначе говоря, последнее правило можно “прочесть” так: если C доказано с
использование допущения A, и C доказано с использованием допущения B, и при
этом мы знаем, что верно A ? B, то можно считать доказанным C (уже без пред-
положений о верности A и B). В последнем правиле использовалось следующее
обозначение: посылка в квадратных скобках означает, что её можно исключить
из рассмотрения. Можно представить себе это как “обрывание” листьев дере-
ва доказательства, соответствующих тем посылкам, которые можно исключить.
Индексом около квадратных скобок показывается то место в дереве, где “обо-
рванный лист” был использован (то есть посылки, заключенные в квадратные
скобки, стали ненужными). Дерево доказательства можно читать так: необорван-
ные листья доказывают корень. Читателю предоставляется возможность самому
34 Элементы теории доказательств


разобраться, какой формой записи пользоваться удобно, а именно, запись в виде
дерева весьма компактна, но не всегда легко читаема. Зато запись в строчку (с
подробными комментариями), как правило, легко читается, но редко получается
компактной.


A A>B
правило исключения импликации
(> e) A, A > B B
или modus ponens (m.p.) B

[A]1
B
Если A B
(> i) правило введения импликации 1
то A > B A>B


Обратимся к правилам, имеющим дело с логическим значком отрицания. Вве-
дем псевдоформулу ? “ложь”, истинностное значение которой во всех интерпре-
тациях будем считать нулем. С помощью такой псевдоформулы можно, напри-
мер, весьма легко записать противоречивость множества формул ? следующим
образом:
? |= ?.
Теперь можно сформулировать правила для значка отрицания и константы
"ложь":

?
правило исключения константы ложь.
(?e) ? A
A
Данное правило допускает простую интерпретацию: из лжи следует все что угод-
но (ex falsum sequitor quodlibet). Даже несведущим в формальной логике людям
это правило хорошо известно; например, оно применяется в житейском споре
в виде восклицания “если это (очевидно ложное для собеседника утверждение)
верно, то я Папа Римский”.

¬A A
(?i) правило введения константы “ложь” ¬A, A ?
?
[A]1
?
Если A ?
(¬i) правило введения отрицания 1
то ¬A ¬A
[¬A]1
?
правило сведения к противоречию Если ¬A ?
(RAA) 1
(reductio ad absurdum) то A A
6.2 Естественная дедукция 35



Наиболее “нетривиальное” правило – последнее. При использовании этого пра-
вила непонятно, как конструктивно выписать A, что породило два крупных
направления в логике – классическая и интуиционистская (не принимает послед-
него правила). Чтобы доказать какое-либо утверждение, в интуиционистской ло-
гике необходимо предъявить цепочку доказательства.

Теорема 6.1 Правило сведения к противоречию (RAA) эквивалентно закону
исключенного третьего (tertium non datur)

(A ? ¬A) (T N D)

Доказательство:
1. Докажем, что из правила сведения к противоречию (RAA) следует закон
исключенного третьего (TND). Доказательство удобно записать в виде следую-
щего дерева.

[A]1
[A ? ¬A]2
¬A ? ¬A
?
¬A1
A ? ¬A [¬(A ? ¬A)]2
?2
A ? ¬A

2. Докажем, что из закона исключенного третьего (TND) следует правило сведе-
ния к противоречию (RAA).
Пусть ¬A ?, тогда
[¬A]1
[A]1
?
A ? ¬A A A
1
A
Таким образом нами была доказана эквивалентность закона исключенного тре-
тьего и правила сведения к противоречию.
Подход интуиционистов нельзя отметать сразу, поскольку уверенными можно
быть в истинности только проверяемых утверждений. Рассмотрим в качестве
примера утверждение о бесконечной последовательности бит, например

(i) данная последовательность состоит только из единиц;

(ii) в данной последовательности есть хотя бы один нуль.
36 Элементы теории доказательств


Очевидно, что ни одно из этих утверждений не может быть проверено (для про-
верки их понадобилось бы бесконечное время). Классическая логика тем не ме-
нее утверждает, что ровно одно из утверждений (i) и (ii) является истинным
(в силу закона исключенного третьего (TND)). Интуиционистский же подход в
данном случае является более осторожным: поскольку ни одно из рассматривае-
мых утверждений практически проверено быть не может, то нельзя утверждать
истинность того, что “верно либо (i), либо (ii)”.

6.3 Подстановки в термах и формулах
Для того, чтобы сформулировать правила введения кванторов всеобщности и
существования, будем считать неразличимыми формулы, которые отличаются
только именами связанных переменных. Например, ?yP (x, y) и ?zP (x, z) будем
считать одной и той же формулой.
Нам также понадобится ввести операцию замены переменных в формуле. В
дальнейшем будем понимать под обозначением P[t/x], где P ? L? , x ? Var, и
I
?
t ? TER(LI ) замену всех вхождений переменной x на терм t. Мы определим
замену переменных для языка логики первого порядка следующим образом.

Определение 6.6 (Замена переменных для термов). Пусть s, t ? TER,
x ? Var. Определим замену s[t/x] следующим образом.
(i) Если s = c ? Const, то s[t/x] := c.

(ii) Если s = y ? Var, причем y отлично от x, то s[t/x] := y.

(iii) Если s = x ? Var, то s[t/x] := t.

(iv) Если s = f k (t1 , . . . , tk ), где f k k-арный функциональный символ, и
t1 , . . . , tk ? TER(L? ), то s[t/x] := f k (t1 [t/x], ..., tk [t/x].
I

Пример 6.2 Пусть c символ константы, x, y символы предметных пере-
менных, а f тернарный функциональный символ. Тогда

f (s(x, c), c, y) f (x, s(x, y), y)/x = f (s(f (x, s(x, y), y), c), c, y)

Определение 6.7 (замена переменных для правильных формул). Пусть
t ? TER(L? ), x ? Var, P, Q ? ?, Ak k-арный предикатный символ. Определим
I
замену так:
(i) Если P атомная формула, т. е. P = Ak (t1 , ..., tk ), то

P[t/x] = Ak (t1 , ..., tk )[t/x] := Ak (t1 [t/x], ..., tk [t/x]).
6.3 Подстановки в термах и формулах 37


(ii) Если P = (¬Q), то
P[t/x] := (¬Q[t/x]).

(iii) Если P = (R ? Q), то

(P)[t/x] = (R[t/x] ? Q[t/x]),

где ? это один из символов ?, ? или >.
(iv) Если P = (?yQ), где ? один из кванторов ? или ?, то

1. Если y = x и y ? V AR(t), то (?yQ)[t/x] = (?yQ[t/x])., где V AR(t) –
множество всех символов предметных переменных в терме t.
2. Если y = x, но y ? V AR(t), то (?yQ)[t/x] = (?rQ[r/y][t/x]), где r ?
V AR(t) (см. пример).
3. Если y = x, то замена не делается, т. е. (?xQ)[t/x] = (?xQ).

Пример 6.3 Пусть < – бинарный предикатный символ (вместо < (x, y) будем
писать x < y), f – унарный функциональный символ, x и y – символы предмет-
ных переменных. Тогда

?y (x < y) f (y)/x = ?z (f (y) < z)

(а не ?y (f (y) < y)).

Теперь мы можем сформулировать правила введения и исключения для кван-
торов всеобщности и существования:
?xA
правило исключения ?xA A [y/x]
(?e)
где y ? T ER(L? )
квантора всеобщности A [y/x]
I


Если ? A [y/x] то ? ?xA
A [y/x]
правило введения
(?i) если y ?
/ free(Q)
квантора всеобщности ?xA
Q??

Заметим, что в последнем правиле весьма важно предположение о том, что y
не входит свободно ни в одну из формул множества ? (иначе говоря, y – “произ-
вольная” переменная). Это правило иногда формулируют так: если ? A [y/x]
для произвольного y, то ? A для любого x. Опустить “предположение” о произ-
вольности y здесь нельзя. Например, введем в арифметике Пеано две формулы
с одной свободной переменной: Odd(x) и Even(x), означающие по смыслу, что x
соответственно “нечетное” или “четное” число. Запишем их следующим образом

Even(x) := ?y(2 · y = x),
38 Элементы теории доказательств


где 2 := s(s(0)),

Odd(x) := Even(s(x))

Тогда в силу доказанного правила (id) имеем Odd(y) Even(S(y))

Однако неверно, что Odd(y) ?xEven(s(x)). То есть из нечетности некоторого
y не следует четность всех чисел! Правило введения квантора всеобщности было
применено неправильно, поскольку символ предикатной переменной y, входящий
в формулу, не являлся произвольным (он входил свободно в формулу-посылку).
Правила введения и исключения для квантора существования следующие:
правило введения
A[t/x]
A[t/x] ?xA
(?i) квантора
где t ? T ER(L? ) ?xA
I
существования

[A[y/x]]1
Если ?, A[y/x] C ?xA
правило исключения
C
то ?, ?xA C
квантора
(?e) 1

<< Пред. стр.

стр. 4
(общее количество: 9)

ОГЛАВЛЕНИЕ

След. стр. >>