Формулы. 
Дискретный анализ. 
Формальные системы и алгоритмы

Среди слов (последовательностей символов) в алфавите исчисления предикатов выделяются термы и формулы. Неформально говоря, термы описывают объекты, а формулы — утверждения об объектах (предикаты от объектов). Формальные определения термов (и формул) даются рекурсивно с использованием определений терма (или формулы) меньшей длины.

Вначале определим термы.

Определение 3.6. Слово t в алфавите ИП является термом тогда и только тогда, когда оно удовлетворяет одному из двух условий.

• 1: t является переменной или константой (т. е. 0-арным функциональным символом);
• 2: t = ^гД^{е в} скобках записаны через запятую п термов, а / — символ из множества п-арных функциональных символов J-_n.

Пример 3.7. Пусть а;, у — символы переменных, а / — бинарной функции. Тогда f (f{x, y), y), f (x, f (x, y)) — термы, а /(/,?) — нет.

Рассмотрим последний пример более подробно. Чтобы слово /(/, х) являлось термом, символ / должен иметь арность 2, а слова /их должны быть термами. Но / термом не является: он не может удовлетворять первому условию, так как / не является переменной или 0-арным символом, однако и второму условию он удовлетворять не может хотя бы потому, что в слове / нет ни одной скобки.

Определение 3.8. Слово в алфавите ИП является эл&мептарной формулой тогда и только тогда, когда оно имеет вид A (t,… ,?_п), где в скобках записаны через запятую п термов, а А — символ из множества n-арных предикатных символов V_n.

Пример 3.9. Слово A (f (f (x, y), y), f (xif (x, y))) является элементарной формулой тогда и только тогда, когда гг, у €.

*, / € А € Р₂.

А вот слова.

не являются формулами. В первом случае А, а во втором / должны одновременно быть бинарным предикатным символом и бинарным функциональным символом, что невозможно по нашему определению алфавита ИП. (Проверьте это утверждение, следуя данным выше определениям!).

Теперь мы, наконец, дадим определение формулы исчисления предикатов.

Определение 3.10. Слово А в алфавите ИП является формулой тогда и только тогда, когда выполняется одно из четырёх условий.

• 1: А является элементарной формулой;
• 2: А = (15), где В — формула;
• 3: А = (В—>С), где В, С — формулы;
• 4: А = (f xB), где В — формула, х — переменная.

При записи формул удобно применять и другие связки Л, V, которые обозначают такие же сокращения, как и в случае исчисления высказываний:

• (А А В) это сокращение формулы (1(Л—"(15))),
• (А V В) это сокращение формулы ((1Л)—>5),
• (Л В) это сокращение формулы ((Л—"В) Л (В—>А)).

Для сокращения записи формул используется также квантор существования 3 по следующему соглашению:

(ЗхА) сокращенно обозначает формулу (1(/#(1Л))).

Аналогично исчислению высказываний, для сокращённой записи формул используются правила опускания скобок. Кванторы, но старшинству сильнее —" и слабее V, Л, 1. Кроме того, принято опускать скобки, в которые заключается кванторная формула (/уА).

Задача 3.1. Докажите, что по сокращённой записи формулы в соответствии со сформулированными выше правилами однозначно восстанавливается её полная запись.

Как и формулы исчисления высказываний, формулы исчисления предикатов можно представлять в виде помеченных корневых плоских деревьев (см. с. 19). Вершины дерева, которое соответствует формуле, помечены переменными, символами пропозициональных связок —1, предикатными и функциональными символами и кванторными блоками х. При этом выполняются следующие условия: переменными помечены только листья дерева; у каждой вершины, помеченной символами 1 или / х, есть один потомок; у вершины, помеченной символом —", — два потомка; у вершины, помеченной функциональным или предикатным символом, столько потомков, какова арность этого символа; потомками вершины, помеченной предикатным символом, являются вершины, помеченные переменными или функциональными символами.

Задача 3.2. Докажите, что по формуле ИП можно определить вид каждого входящего в неё символа (предикатный, функциональный, переменная), а также арность предикатных и функциональных символов.