Термы и их унификация

Теории первого порядка

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

Теории первого порядка возникли с целью формализации и строгого обоснования математики. В 1901 году Дедекинд предложил первое обоснование арифметики, известное теперь под названием системы аксиом Пеано. В 1908 году Цермело сформулировал аксиомы теории множеств. Так было установлено, что множество натуральных чисел и класс всех множеств тоже являются моделями теорий первого порядка. Это стимулировало развитие теории моделей, основные теоремы которой были доказаны Лёвенгеймом (1915 г.), Скулемом (1920 г.), Гёделем (1930 г.), Мальцевым (1936 г.).

Главное внимание в данной главе будет уделено доказательствам теоремы Мальцева о компактности, теорем Гёделя о непротиворечивости исчисления предикатов и о полноте теории первого порядка. Отметим теоремы Лёвенгейма-Скулема, из которых следует существование счётной модели теории множеств и несчётной модели теории натуральных чисел. Рассмотрим метод резолюций Робинсона (1965 г.) автоматического доказательства предложений исчисления предикатов.

Термы и предикаты

Термы и их унификация

Упрощённо можно сказать, что термы – это алгебраические выражения, определяющие функции, значения которых вычисляются с помощью операций. Например, в булевой алгебре А определены операции: , , , и из этих операций можно составлять термы, например, , , . Перейдём к точным определениям.

Пусть – счётное множество, элементы которого будут называться переменными, F – произвольное множество, элементы которого будут называться функциональными символами, – произвольная функция. Элементы f Î F, для которых , называются n-арными операциями. Например, для булевой алгебры множество функциональных символов будет равно: F = {Ç, È, Ø}, значения функции # равны #(Ç) = 2, #(È) = 2, #(Ø) = 1, поэтому все элементы из F – операции. Символы c Î F, для которых #(с) = 0, называются символами констант. Термы определим по индукции:

1) переменные и символы констант являются термами;

2) если – термы и f – n-арная операция, то – терм;

3) кроме построенных с помощью правил 1 – 2, других термов нет.

В определении терма участвует префиксная форма операции. Заметим, что бинарные операции записываются обычно в инфиксной форме. Например, вместо применяется запись: . Учитывая приоритеты операций, скобки часто опускают, в частности, приведённая запись равносильна выражению: , ибо приоритет операции Ç выше приоритета È.

Согласно определению терма, множество всех термов T(F) содержит множество переменных X. Подстановкой называется отображение такое, что для всех x Î X, за исключением элементов некоторого конечного подмножества из X, имеет место v(x) = x. Распространим подстановку v до некоторой функции , полагая

1) если t Î X, то v¢(t) = v(t);

2) если t – символ константы, то v¢(t) = t;

3) если для некоторой n-арной операции f и термов , то .

Терм v¢(t) называется результатом применения подстановки v к терму t. Например, результатом подстановки

, ,

в терм будет терм: . Если значения не указаны, то по умолчанию . Подстановку записывают как множество пар , например: .

Пусть заданы два терма s и t, и пусть надо найти подстановку, делающую эти термы равными. Эта задача решается следующим образом.

Подстановка v называется унификатором термов s и t, если v¢ (s) = v¢ (t). Унификатор v называется наибольшим общим унификатором термов s и t и обозначается: m.g.u.(s, t) = v, если для любого другого унификатора w термов s и t существует такая подстановка a, что a¢ _° v¢ = w¢. Если для термов s и t существует хотя бы один унификатор, то среди унификаторов существует наибольший общий. Для его нахождения предлагается следующий алгоритм.