4. Общая картина

Интуиционистское исчисление высказываний изначально появилось как синтаксическая теория. Подобрав ей подходящую семантику, удалось (ну… практически …) показать, что она разрешима. Тоже полезное знание . Синтаксис и семантика – равноправные партнёры.

Глава 2. Предикаты и выразимость §6. Формулы языка логики предикатов. Интерпретации

1. Обсуждение

Изучение исчисления высказываний было небесполезно, но не предоставило ни одного по-настоящему нетривиального примера. Все рассмотренные теории оказались разрешимы и синтаксическая теория всюду совпала с семантической. Трудно поверить в то, что так бывает всегда (особенно – в первое). Возможно, для получения нетривиальных примеров следует усложнить рассматриваемый язык? Наверное, можно и по-другому: создать какую-нибудь безумную пропозициональную семантику… Впрочем, семантика усложнится вместе с языком .

Вспомним также, что имеется в виду обсуждать настоящую математику, описывающую реальный мир, то есть некоторые множества и их элементы. Поэтому следует ввести в рассмотрение функции, отношения и кванторы . Иначе на программе Лейбница можно ставить крест.

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

2. Алфавит языка логики предикатов

В языке, о котором пойдёт речь, имеются четыре типа букв:

а) уже использованные символы логических связок: С, D, J, N, O, I и новые буквы А и Е, обозначающие кванторы (теперь буква А есть перевёрнутый квантор всеобщности );

б) множество V всевозможных предметных переменных (принимающих значения из некоторых множеств); элементы множества V записываются строчными латинскими буквами, возможно – с индексами;

в) множество F всевозможных функциональных символов;

г) множество R всевозможных символов отношений.

Символы функций и отношений естественно разбиваются на подмножества. Функции бывают одного переменного, двух переменных, трёх… Отношения тоже бывают унарные, бинарные, тернарные и т.д. Стоит рассмотреть так же функции от нуля переменных (то есть – предметные константы) и нульарные отношения (то есть – булевы константы, примерно то же, что раньше называлось пропозициональными переменными). Обозначая символом множество всевозможных символов функций k аргументов, а – множество всевозможных символов m-арных отношений, получаем , .

3. Термы

Необходимо рассмотреть два уровня обсуждения: на нижнем уровне при помощи функций проводятся манипуляции с элементами множеств, из полученных «сложных вещей» при помощи отношений и кванторов изготавливаются простые высказывания, из которых, в свою очередь, на верхнем уровне (при помощи логических связок) создаются высказывания сложные (или лучше сказать – составные?).

Следует сознаться, что без функций (и, следовательно, без первого уровня) можно обойтись. Например, функцию сложения (от двух переменных) можно заменить трёхместным отношением Add, определённым правилом: . Однако использование этого приёма делает запись довольно замысловатой и превращает даже довольно простые вещи в очень сложные формулы, поэтому мы так делать не будем (в качестве упражнения желающие могут подвергнуть некоторые рассматриваемые вопросы такого рода переработке).

Определение 6.1. Множество Т называется множеством термов, если удовлетворяет условиям:

(1) (всякая переменная есть терм);

(2) , ; в частности, если , то , так что ;

(3) для любого множества W, удовлетворяющего условиям (1) и (2), .

Замечания. (1) Приведённое определение очень похоже на определение множества пропозициональных формул. Напомним, что определения такого вида называются индуктивными.

(2) Выражение заменяет собой более привычное .

(3) Как и в случае формул, можно говорить не только о множестве, но и об алгебре термов (только зачем?).

(4) Совершенно так же, как и для формул, доказывается, что множество Т существует и единственно (упражнение).

(5) Конечно плохо, что на функциональном символе нигде не написано количество аргументов функций, которые он может обозначать. Поэтому не может быть полной уверенности в том, что есть терм, это так только в том случае, если . Будем считать, что это подразумевается. Однако ясно, что термом не является выражение , поскольку функция g не может быть одновременно от двух и от трёх аргументов.