matlogta

Министерство образования и науки Российской Федерации

НОВОСИБИРСКИЙ ГОСУДАРСТВЕННЫЙ ТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ

С. В. СУДОПЛАТОВ, Е. В. ОВЧИННИКОВА

МАТЕМАТИЧЕСКАЯ ЛОГИКА И ТЕОРИЯ АЛГОРИТМОВ

УЧЕБНИК

для дистанционного образования

НОВОСИБИРСК

2006

Рецензенты: А. Г. Пинус д-р физ.-мат. наук, проф.; В. М. Зыбарев канд. техн.наук, доц.

Сергей Владимирович Судоплатов Елена Викторовна Овчинникова

Математическая логика и теория алгоритмов

В книге излагаются основные классические исчисления математи- ческой логики: исчисления высказываний и исчисления предикатов, а также элементы теории алгоритмов и неклассических логик.

Книга предназначена для студентов технических вузов, изучающих математическую логику и теорию алгоритмов в рамках дистанционного образования.

°c Судоплатов С.В., Овчинникова Е.В., 2006.

Оглавление

3

à ë à â à 1

ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ

Ÿ 1.1. Определение формального исчисления

Введем общее понятие формального исчисления. Будем говорить, что формальное исчисление I определено, если выполняются следую-

щие четыре условия:

1. Имеется некоторое множество A(I) алфавит исчисления I. Элементы алфавита A(I) называются символами. Конечные последовательности символов называются словами исчисления I. Обозначим через W (I) множество всех слов алфавита исчисления I.

2. Задано подмножество E(I) µ W (I), называемое множеством выражений исчисления I. Элементы множества E(I) называются фор-

мулами или секвенциями.

3. Выделено множество Ax(I) µ E(I) выражений исчисления I, называемых аксиомами исчисления I.

4. Имеется конечное множество R(I) частичных операций R1, R2,

: : :, Rn на множестве E(I), называемых правилами вывода исчисления I.

Итак, исчисление I есть четверка hA(I); E(I); Ax(I); R(I)i.

Если набор выражений (Φ1; : : : ; Φm; Φ) принадлежит правилу Ri, то выражения Φ1; : : : ; Φm называются посылками, а выражение Φ

непосредственным следствием выражений Φ1, : : :, Φm по правилу Ri,

Иногда в этой записи символ i будет опускаться, если из контекста ясно, о каком правиле идет речь:

Φ1; : : : ; Φm :

Φ

5

Выводом в исчислении I называется последовательность выражений Φ1, Φ2, : : :, Φn такая, что для любого i (1 6 i 6 n) выражение

Φi есть либо аксиома исчисления I, либо непосредственное следствие каких-либо предыдущих выражений.

Выражение Φ называется теоремой исчисления I, выводимым в I

или доказуемым в I, если существует вывод Φ1, : : :, Φn, Φ, который называется выводом выражения Φ или доказательством теоремы Φ.

П р и м е р 1.1.1. 1. Пусть E(I) множество повествовательных предложений русского языка, Ax(I) множество истинных в данный

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

2. Пусть E(I) множество программ Pf , производящих вычисле- ния значений одноместных числовых функций f, Ax(I) множество

простых программ. Для программ Pf ; Pg 2 E(I) обозначим через

Pf ± Pg программу, составленную из программ Pf è Pg òàê, ÷òî ïî ëþ- бым начальным данным производятся вычисления значений функции f, а затем полученные значения используются как начальные данные,

по которым вычисляется значение функции g. Правило вывода

Pf ; Pg

Pf ± Pg

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

Вообще говоря, может не существовать алгоритма, с помощью которого для произвольного выражения Φ формального исчисления I çà

конечное число шагов можно определить, является ли Φ выводимым в I или нет. Если такой алгоритм существует, то исчисление называется

разрешимым, а если такого алгоритма нет неразрешимым. Исчисление называется непротиворечивым, если не все его выра-

жения доказуемы.

Ниже мы проведем построение двух формальных исчислений исчислений высказываний, в основе которых лежат формулы алгебры логики. Первое из этих исчислений исчисление высказываний генценовского типа, предложенное Генценом, в качестве выражений использует секвенции, построенные из формул алгебры логики. Это исчисление будет обозначаться через ИС. Второе исчисление исчис- ление высказываний гильбертовского типа, создано Гильбертом, и в

6

нем выражениями являются непосредственно формулы алгебры логики. Исчисление высказываний гильбертовского типа будет обозначаться через ИВ.

Мы покажем, что оба исчисления эквивалентны в том смысле, что доказуемыми в них будут являться в точности тождественно истинные формулы. Из последнего факта будут вытекать разрешимость и непротиворечивость исчислений высказываний.

Строящиеся в дальнейшем исчисления ИПС и ИП, являющиеся расширениями исчислений ИС и ИВ соответственно, послужат примерами неразрешимых непротиворечивых исчислений.

Ÿ1.2. Исчисление высказываний генценовского типа

Определим элементы исчисления высказываний ИС.

Алфавит ИС состоит из букв A, B, Q, P , R и других, возмож-

но, с индексами (которые называются пропозициональными переменными), логических символов (связок) отрицания :, конъюнкции ^,

дизъюнкции _, импликации !, следования `, а также вспомогатель-

íûõ символов: левой скобки (, правой скобки ), запятой ,. Множество формул ИС определяется индуктивно:

а) все пропозициональные переменные являются формулами ИС (такие формулы называются элементарными или атомарными);

á) åñëè ', Ã формулы ИС, то :', (' ^ Ã), (' _ Ã), (' ! Ã)

формулы ИС; в) выражение является формулой ИС тогда и только тогда, когда

это может быть установлено с помощью пунктов а и б .

Таким образом, любая формула ИС строится из пропозициональных переменных с помощью связок :, ^, _, !.

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

Секвенциями называются конечные выражения следующих двух видов, где '1; : : : ; 'n; Ã формулы ИС:

'1; : : : ; 'n ` Ã ( из истинности '1; : : : ; 'n следует Ã ),

'1; : : : ; 'n ` ( система формул '1; : : : ; 'n противоречива ). Последовательности формул '1; : : : ; 'n в секвенциях будут часто

обозначаться через (возможно, с индексами): ` Ã, `. При этом последовательность считается пустой при n = 0. Значит, записи ` Ã è ` также являются секвенциями, первая из которых может читать-

ся как утверждение о доказуемости формулы Ã. Смысл секвенции ` будет указан в Ÿ 1.5.

7

Таким образом, наряду с формулами, символизирующими простые или сложные высказывания, секвенции являются записями утверждений, в которых выделяются посылки и заключение.

Множество аксиом ИС определяется следующей схемой секвенций: ' ` ', ãäå ' произвольная формула ИС.

Аксиомами являются, например, секвенции A ^ :B ` A ^ :B è

A ! :A1 ! B _ C ^ :D ` A ! :A1 ! B _ C ^ :D.

Правила вывода ИС задаются следующими записями, где , 1 произвольные (возможно пустые) конечные последовательности формул ИС, '; Ã; Â произвольные формулы ИС.

` '; ` Ã

1.` (' ^ Ã) (введение ^).

` (' ^ Ã)

2.` ' (удаление ^).

` (' ^ Ã)

3.` Ã (удаление ^).

` '

4.` (' _ Ã) (введение _).

` Ã

5.` (' _ Ã) (введение _).

8

Вывод S0; : : : ; Sn в ИС называется линейным доказательством. Секвенция S называется доказуемой в ИС, или теоремой ИС, если су-

ществует линейное доказательство S0; : : : ; Sn в ИС, заканчивающееся секвенцией S: Sn = S. Формула ' называется доказуемой в ИС, если в ИС доказуема секвенция ` '.

Определим по индукции понятие дерева секвенций: 1) любая секвенция является деревом секвенций;

2) åñëè D0; : : : ; Dn деревья секвенций и S секвенция, то запись

D0; : : : ; Dn

S

также является деревом секвенций; 3) любое дерево секвенций строится в соответствии с пп. 1 и 2.

Вхождением секвенции в дерево D называется место, которое се-

квенция занимает в дереве. Каждая секвенция может иметь несколько вхождений в дерево секвенций. Вхождение секвенции в дерево D, íàä

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

Из определения дерева секвенций ясно, что начальных секвенций в дереве может быть несколько, а заключительная секвенция единственна.

Часть дерева, состоящая из секвенций, находящихся непосредственно над некоторой чертой, под той же чертой, а также самой черты, называется переходом.

Дерево D называется доказательством в ИС в виде дерева, если

все его начальные секвенции суть аксиомы ИС, а переходы осуществляются по правилам 1 12. Дерево D называется доказательством се-

квенции S в виде дерева в ИС, или деревом вывода S â ÈÑ, åñëè D

доказательство в ИС и S его заключительная секвенция.

Наличие линейного доказательства секвенции равносильно существованию доказательства секвенции в виде дерева:

Предложение 1.2.1. Секвенция S имеет доказательство в ИС в виде дерева тогда и только тогда, когда S теорема ИС. ¤

Очевидно, что представление доказательства в виде дерева более наглядно и позволяет проследить все переходы по правилам вывода.

9

П р и м е р 1.2.1. 1. Следующее дерево демонстрирует доказуемость формулы ' _ :' для любой формулы ':

`'_:' 9

2. Приведем доказательство секвенций ' ^ Ã ` Ã ^ ' в виде дерева для любых формул ' è Ã:

S0; : : : ; Sn

Правило S называется допустимым в ИС, если из выводимости в ИС секвенций S0; : : : ; Sn следует выводимость в ИС секвенции

S.

Заметим, что допустимость правила равносильна тому, что его добавление в исчисление ИС не расширяет множество доказуемых секвенций.

` ' ^ :'

(æ)` (выведение противоречия);

10