У математичній логіці замкнений терм формальної системи є термом, який не містить жодної вільної змінної.
Аналогічним чином, замкнена формула — це формула, яка не містить жодної вільної змінної. У логіці першого порядку формула є замкненою фомулою.
Замкнений вираз — це замкнений терм, чи замкнена формула.
Приклади
Розглянемо такі вирази з логіки першого порядку над сигнатурою, що містить постійний символ 0 для числа 0, унарну функцію s та бінарну функцію + для суми.
s(0), s(s(0)), s(s(s(0))) ... замкнені терми; 0+1, 0+1+1, ... замкнені терми. x+s(1) і s(x) є термами, але не замкненими; s(0)=1 і 0+0=0 замкнені формули; s(1) і ∀x: (s(x)+1=s(s(x))) замкнені вирази.
Формальне визначення
Нижче наводиться формальне визначення для мов першого порядку. Нехай є мова першого порядку з множиною константних символів, з множиною змінних, з множиною функціональних операторів та множиною предікатних символів.
Замкнений терм Замкнені терми це терми, які не містять змінних.Вони можуть бути визначені за допомогою рекурсії. елемент з C є замкненим термом; Якщо f∈F є n-арною функцією і α1, α2, ..., αn є замкненими термами, тоді f(α1, α2, ..., αn) є замкненим термом. Кожен замкнений терм може бути представлений за допомогою застосування зазначених вище двох правил (немає ніяких інших замкнених термів; предікати не можуть бути замкненими термами).
Грубо кажучи, це сукупність всіх замкнених термів.
Замкнений атом Замкнений предікат, або замкнений атом, — це атом, всі терми якого, є замкненими.
Якщо p∈P є n-арним предікатом і α1, α2, ..., αn є замкненими термами, тоді p(α1, α2, ..., αn) є замкненим предікатом, або замкненим термом.
Грубо кажучи, база Ербрана — це множина усіх замкнених атомів, доки інтерпретація Ербрана приймає істинне значення для кожного замкненого атому у базі.
Замкнена формула Замкнена формула це формула без вільних змінних. Формули з вільними змінними можуть бути визначені за допомогою рекурсії наступним чином: Вільні змінні незамкненого атому — це всі змінні, що входять в нього. Вільні змінні — p такі самі як для p. Вільні p∨q, p∧q, p→q це вільні змінні p, чи вільні змінні q. Вільні змінні p і p - це всі вільнні змінні p окрім x.
Посилання
First-Order Logic: Syntax and Semantics