Т. А. Сливина математическая логика и теория алгоритмов

Определение терма.
1. Предметная переменная и предметная константа – термы.
2.Если r₁, r₂, ..., r_п – термы и А – символ n-местной операции, то (r₁, r₂, …, r_n) терм.
3. Никаких других термов, кроме определенных в п. 1 и п. 2, в Т нет.
Согласно естественной интерпретации, терм – это имя некоторого предмета. Кроме переменных и предметных констант, термами являются цепочки, образованные из переменных и предметных констант посредством символов операций, так как в подразумеваемой интерпретации он истолковывается как значение некоторой функции.
Определение формулы.
1. Если А – символ n-местного отношения (предикат или функция), а r₁, r₂, ..., r_п – термы, то A(r₁, r₂, ..., r_п) – формула. В частности, если А – предикатная буква , то (r₁, r₂, ..., r_п) называется элементарной формулой.
2. Если А и В формулы, то АВ, AВ, АВ , – формулы.
3. Если А – формула, а у – предметная переменная, которая входит в А свободно или не содержится в А, то выражения yA, уА – формулы. При этом А называется областью действия квантора.
4. Никаких других формул, кроме определенных в п. 1 – 3, нет.
Логические и специальные аксиомы. Правила вывода.
Аксиомы теории первого порядка Т разбиваются на два класса: логические аксиомы и специальные (нелогические или собственные аксиомы).
Логические аксиомы. Каковы бы ни были формулы А, В и С теории Т следующие формулы являются логическими аксиомами теории Т:
1. А(ВА);
2. (А(ВС))((АВ)(АС));
3. ;
4. , где есть формула теории Т и t есть терм теории Т, свободный в А(x_i). Отметим, что t может совпадать с х_i, и тогда мы приходим к аксиоме ;

1. 
   5. , если x_i не входит свободно в формулу А.