Замкнений вираз
У математичній логіці замкнений терм формальної системи є термом, який не містить жодної вільної змінної.
Аналогічним чином, замкнена формула - це формула, яка не містить жодної вільної змінної. У логіці першого порядку формула є замкненою фомулою.
Замкнений вираз - це замкнений терм, чи замкнена формула.
Приклади
Розглянемо такі вирази з логіки першого порядку над сигнатурою, що містить постійний символ 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.
Посилання
- Dalal, M. (2000). Logic-based computer programming paradigms. У Rosen, K.H.; Michaels, J.G. Handbook of discrete and combinatorial mathematics. с. 68.
- Hodges, Wilfrid (1997). A shorter model theory. Cambridge University Press. ISBN 978-0-521-58713-6.
- First-Order Logic: Syntax and Semantics